some experiements towards user interface for predicate compiler
authorhaftmann
Fri Apr 24 17:45:16 2009 +0200 (2009-04-24)
changeset 309725b65835ccc92
parent 30971 7fbebf75b3ef
child 30973 304ab57afa6e
some experiements towards user interface for predicate compiler
src/HOL/ex/Predicate_Compile.thy
src/HOL/ex/predicate_compile.ML
     1.1 --- a/src/HOL/ex/Predicate_Compile.thy	Fri Apr 24 17:45:15 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Fri Apr 24 17:45:16 2009 +0200
     1.3 @@ -1,20 +1,17 @@
     1.4  theory Predicate_Compile
     1.5 -imports Complex_Main Code_Index Lattice_Syntax
     1.6 +imports Complex_Main Lattice_Syntax Code_Eval
     1.7  uses "predicate_compile.ML"
     1.8  begin
     1.9  
    1.10 +text {* Package setup *}
    1.11 +
    1.12  setup {* Predicate_Compile.setup *}
    1.13  
    1.14 -primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
    1.15 -  \<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where
    1.16 -    "next yield Predicate.Empty = None"
    1.17 -  | "next yield (Predicate.Insert x P) = Some (x, P)"
    1.18 -  | "next yield (Predicate.Join P xq) = (case yield P
    1.19 -   of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
    1.20 +
    1.21 +text {* Experimental code *}
    1.22  
    1.23 -fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
    1.24 -  "anamorph f k x = (if k = 0 then ([], x)
    1.25 -    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> let (vs, z) = anamorph f (k - 1) y in (v # vs, z))"
    1.26 +definition pred_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'b Predicate.pred" where
    1.27 +  "pred_map f P = Predicate.bind P (Predicate.single o f)"
    1.28  
    1.29  ML {*
    1.30  structure Predicate =
    1.31 @@ -22,11 +19,68 @@
    1.32  
    1.33  open Predicate;
    1.34  
    1.35 -fun yield (Predicate.Seq f) = @{code next} yield (f ());
    1.36 +val pred_ref = ref (NONE : (unit -> term Predicate.pred) option);
    1.37 +
    1.38 +fun eval_pred thy t =
    1.39 +  t 
    1.40 +  |> Eval.mk_term_of (fastype_of t)
    1.41 +  |> (fn t => Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy t []);
    1.42 +
    1.43 +fun eval_pred_elems thy t T length =
    1.44 +  t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T;
    1.45  
    1.46 -fun yieldn k = @{code anamorph} yield k;
    1.47 +fun analyze_compr thy t =
    1.48 +  let
    1.49 +    val split = case t of (Const (@{const_name Collect}, _) $ t') => t'
    1.50 +      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t);
    1.51 +    val (body, Ts, fp) = HOLogic.strip_split split;
    1.52 +    val (t_pred, args) = strip_comb body;
    1.53 +    val pred = case t_pred of Const (pred, _) => pred
    1.54 +      | _ => error ("Not a constant: " ^ Syntax.string_of_term_global thy t_pred);
    1.55 +    val mode = map is_Bound args; (*FIXME what about higher-order modes?*)
    1.56 +    val args' = filter_out is_Bound args;
    1.57 +    val T = HOLogic.mk_tupleT fp Ts;
    1.58 +    val mk = HOLogic.mk_tuple' fp T;
    1.59 +  in (((pred, mode), args), (mk, T)) end;
    1.60  
    1.61  end;
    1.62  *}
    1.63  
    1.64 +
    1.65 +text {* Example(s) *}
    1.66 +
    1.67 +inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
    1.68 +    "even 0"
    1.69 +  | "even n \<Longrightarrow> odd (Suc n)"
    1.70 +  | "odd n \<Longrightarrow> even (Suc n)"
    1.71 +
    1.72 +setup {* pred_compile "even" *}
    1.73 +thm even_codegen
    1.74 +
    1.75 +
    1.76 +inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.77 +    append_Nil: "append [] xs xs"
    1.78 +  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    1.79 +
    1.80 +setup {* pred_compile "append" *}
    1.81 +thm append_codegen
    1.82 +
    1.83 +
    1.84 +inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.85 +  for f where
    1.86 +    "partition f [] [] []"
    1.87 +  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
    1.88 +  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
    1.89 +
    1.90 +setup {* pred_compile "partition" *}
    1.91 +thm partition_codegen
    1.92 +
    1.93 +setup {* pred_compile "tranclp" *}
    1.94 +thm tranclp_codegen
    1.95 +
    1.96 +ML_val {* Predicate_Compile.modes_of @{theory} @{const_name partition} *}
    1.97 +ML_val {* Predicate_Compile.modes_of @{theory} @{const_name tranclp} *}
    1.98 +
    1.99 +ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
   1.100 +
   1.101  end
   1.102 \ No newline at end of file
     2.1 --- a/src/HOL/ex/predicate_compile.ML	Fri Apr 24 17:45:15 2009 +0200
     2.2 +++ b/src/HOL/ex/predicate_compile.ML	Fri Apr 24 17:45:16 2009 +0200
     2.3 @@ -6,38 +6,119 @@
     2.4  
     2.5  signature PREDICATE_COMPILE =
     2.6  sig
     2.7 -  val create_def_equation': string -> (int list option list * int list) option -> theory -> theory
     2.8 +  type mode = int list option list * int list
     2.9 +  val create_def_equation': string -> mode option -> theory -> theory
    2.10    val create_def_equation: string -> theory -> theory
    2.11 -  val intro_rule: theory -> string -> (int list option list * int list) -> thm
    2.12 -  val elim_rule: theory -> string -> (int list option list * int list) -> thm
    2.13 +  val intro_rule: theory -> string -> mode -> thm
    2.14 +  val elim_rule: theory -> string -> mode -> thm
    2.15    val strip_intro_concl : term -> int -> (term * (term list * term list))
    2.16    val code_ind_intros_attrib : attribute
    2.17    val code_ind_cases_attrib : attribute
    2.18 +  val print_alternative_rules : theory -> theory
    2.19 +  val modename_of: theory -> string -> mode -> string
    2.20 +  val modes_of: theory -> string -> mode list
    2.21    val setup : theory -> theory
    2.22 -  val print_alternative_rules : theory -> theory
    2.23    val do_proofs: bool ref
    2.24  end;
    2.25  
    2.26  structure Predicate_Compile: PREDICATE_COMPILE =
    2.27  struct
    2.28  
    2.29 +(** auxiliary **)
    2.30 +
    2.31 +(* debug stuff *)
    2.32 +
    2.33 +fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
    2.34 +
    2.35 +fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
    2.36 +fun debug_tac msg = (fn st => (tracing msg; Seq.single st));
    2.37 +
    2.38 +val do_proofs = ref true;
    2.39 +
    2.40 +
    2.41 +(** fundamentals **)
    2.42 +
    2.43 +(* syntactic operations *)
    2.44 +
    2.45 +fun mk_eq (x, xs) =
    2.46 +  let fun mk_eqs _ [] = []
    2.47 +        | mk_eqs a (b::cs) =
    2.48 +            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
    2.49 +  in mk_eqs x xs end;
    2.50 +
    2.51 +fun mk_tupleT [] = HOLogic.unitT
    2.52 +  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
    2.53 +
    2.54 +fun mk_tuple [] = HOLogic.unit
    2.55 +  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
    2.56 +
    2.57 +fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
    2.58 +  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
    2.59 +  | dest_tuple t = [t]
    2.60 +
    2.61 +fun mk_pred_enumT T = Type ("Predicate.pred", [T])
    2.62 +
    2.63 +fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T
    2.64 +  | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []);
    2.65 +
    2.66 +fun mk_Enum f =
    2.67 +  let val T as Type ("fun", [T', _]) = fastype_of f
    2.68 +  in
    2.69 +    Const (@{const_name Predicate.Pred}, T --> mk_pred_enumT T') $ f    
    2.70 +  end;
    2.71 +
    2.72 +fun mk_Eval (f, x) =
    2.73 +  let val T = fastype_of x
    2.74 +  in
    2.75 +    Const (@{const_name Predicate.eval}, mk_pred_enumT T --> T --> HOLogic.boolT) $ f $ x
    2.76 +  end;
    2.77 +
    2.78 +fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T);
    2.79 +
    2.80 +fun mk_single t =
    2.81 +  let val T = fastype_of t
    2.82 +  in Const(@{const_name Predicate.single}, T --> mk_pred_enumT T) $ t end;
    2.83 +
    2.84 +fun mk_bind (x, f) =
    2.85 +  let val T as Type ("fun", [_, U]) = fastype_of f
    2.86 +  in
    2.87 +    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
    2.88 +  end;
    2.89 +
    2.90 +val mk_sup = HOLogic.mk_binop @{const_name sup};
    2.91 +
    2.92 +fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred},
    2.93 +  HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) $ cond;
    2.94 +
    2.95 +fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT
    2.96 +  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
    2.97 +
    2.98 +
    2.99 +(* data structures *)
   2.100 +
   2.101 +type mode = int list option list * int list;
   2.102 +
   2.103 +val mode_ord = prod_ord (list_ord (option_ord (list_ord int_ord))) (list_ord int_ord);
   2.104 +
   2.105  structure PredModetab = TableFun(
   2.106 -  type key = (string * (int list option list * int list))
   2.107 -  val ord = prod_ord fast_string_ord (prod_ord
   2.108 -            (list_ord (option_ord (list_ord int_ord))) (list_ord int_ord)))
   2.109 +  type key = string * mode
   2.110 +  val ord = prod_ord fast_string_ord mode_ord
   2.111 +);
   2.112  
   2.113  
   2.114 +(*FIXME scrap boilerplate*)
   2.115 +
   2.116  structure IndCodegenData = TheoryDataFun
   2.117  (
   2.118    type T = {names : string PredModetab.table,
   2.119 -            modes : ((int list option list * int list) list) Symtab.table,
   2.120 +            modes : mode list Symtab.table,
   2.121              function_defs : Thm.thm Symtab.table,
   2.122              function_intros : Thm.thm Symtab.table,
   2.123              function_elims : Thm.thm Symtab.table,
   2.124 -            intro_rules : (Thm.thm list) Symtab.table,
   2.125 +            intro_rules : Thm.thm list Symtab.table,
   2.126              elim_rules : Thm.thm Symtab.table,
   2.127              nparams : int Symtab.table
   2.128 -           };
   2.129 +           }; (*FIXME: better group tables according to key*)
   2.130        (* names: map from inductive predicate and mode to function name (string).
   2.131           modes: map from inductive predicates to modes
   2.132           function_defs: map from function name to definition
   2.133 @@ -115,26 +196,12 @@
   2.134              intro_rules = #intro_rules x, elim_rules = #elim_rules x,
   2.135              nparams = f (#nparams x)}) thy
   2.136  
   2.137 -(* Debug stuff and tactics ***********************************************************)
   2.138 -
   2.139 -fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
   2.140 -fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
   2.141 -
   2.142 -fun debug_tac msg = (fn st =>
   2.143 -     (tracing msg; Seq.single st));
   2.144 -
   2.145  (* removes first subgoal *)
   2.146  fun mycheat_tac thy i st =
   2.147    (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
   2.148  
   2.149 -val (do_proofs : bool ref) = ref true;
   2.150 -
   2.151  (* Lightweight mode analysis **********************************************)
   2.152  
   2.153 -(* Hack for message from old code generator *)
   2.154 -val message = tracing;
   2.155 -
   2.156 -
   2.157  (**************************************************************************)
   2.158  (* source code from old code generator ************************************)
   2.159  
   2.160 @@ -153,7 +220,8 @@
   2.161        | _ => false)
   2.162    in check end;
   2.163  
   2.164 -(**** check if a type is an equality type (i.e. doesn't contain fun) ****)
   2.165 +(**** check if a type is an equality type (i.e. doesn't contain fun)
   2.166 +  FIXME this is only an approximation ****)
   2.167  
   2.168  fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
   2.169    | is_eqT _ = true;
   2.170 @@ -165,7 +233,7 @@
   2.171      | SOME js => enclose "[" "]" (commas (map string_of_int js)))
   2.172         (iss @ [SOME is]));
   2.173  
   2.174 -fun print_modes modes = message ("Inferred modes:\n" ^
   2.175 +fun print_modes modes = tracing ("Inferred modes:\n" ^
   2.176    cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
   2.177      string_of_mode ms)) modes));
   2.178  
   2.179 @@ -182,6 +250,7 @@
   2.180          (get_args' is (i+1) ts)
   2.181  in get_args' is 1 ts end
   2.182  
   2.183 +(*FIXME this function should not be named merge... make it local instead*)
   2.184  fun merge xs [] = xs
   2.185    | merge [] ys = ys
   2.186    | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
   2.187 @@ -197,7 +266,8 @@
   2.188  
   2.189  fun cprods xss = foldr (map op :: o cprod) [[]] xss;
   2.190  
   2.191 -datatype mode = Mode of (int list option list * int list) * int list * mode option list;
   2.192 +datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand
   2.193 +  why there is another mode type!?*)
   2.194  
   2.195  fun modes_of modes t =
   2.196    let
   2.197 @@ -285,11 +355,11 @@
   2.198    in (p, List.filter (fn m => case find_index
   2.199      (not o check_mode_clause thy param_vs modes m) rs of
   2.200        ~1 => true
   2.201 -    | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
   2.202 +    | i => (tracing ("Clause " ^ string_of_int (i+1) ^ " of " ^
   2.203        p ^ " violates mode " ^ string_of_mode m); false)) ms)
   2.204    end;
   2.205  
   2.206 -fun fixp f (x : (string * (int list option list * int list) list) list) =
   2.207 +fun fixp f (x : (string * mode list) list) =
   2.208    let val y = f x
   2.209    in if x = y then x else fixp f y end;
   2.210  
   2.211 @@ -306,66 +376,6 @@
   2.212  (*****************************************************************************************)
   2.213  (**** term construction ****)
   2.214  
   2.215 -fun mk_eq (x, xs) =
   2.216 -  let fun mk_eqs _ [] = []
   2.217 -        | mk_eqs a (b::cs) =
   2.218 -            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
   2.219 -  in mk_eqs x xs end;
   2.220 -
   2.221 -fun mk_tuple [] = HOLogic.unit
   2.222 -  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
   2.223 -
   2.224 -fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
   2.225 -  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
   2.226 -  | dest_tuple t = [t]
   2.227 -
   2.228 -fun mk_tupleT [] = HOLogic.unitT
   2.229 -  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
   2.230 -
   2.231 -fun mk_pred_enumT T = Type ("Predicate.pred", [T])
   2.232 -
   2.233 -fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T
   2.234 -  | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []);
   2.235 -
   2.236 -fun mk_single t =
   2.237 -  let val T = fastype_of t
   2.238 -  in Const(@{const_name Predicate.single}, T --> mk_pred_enumT T) $ t end;
   2.239 -
   2.240 -fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T);
   2.241 -
   2.242 -fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred},
   2.243 -                          HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) 
   2.244 -                         $ cond
   2.245 -
   2.246 -fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT
   2.247 -  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
   2.248 -
   2.249 -fun mk_bind (x, f) =
   2.250 -  let val T as Type ("fun", [_, U]) = fastype_of f
   2.251 -  in
   2.252 -    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
   2.253 -  end;
   2.254 -
   2.255 -fun mk_Enum f =
   2.256 -  let val T as Type ("fun", [T', _]) = fastype_of f
   2.257 -  in
   2.258 -    Const (@{const_name Predicate.Pred}, T --> mk_pred_enumT T') $ f    
   2.259 -  end;
   2.260 -
   2.261 -fun mk_Eval (f, x) =
   2.262 -  let val T = fastype_of x
   2.263 -  in
   2.264 -    Const (@{const_name Predicate.eval}, mk_pred_enumT T --> T --> HOLogic.boolT) $ f $ x
   2.265 -  end;
   2.266 -
   2.267 -fun mk_Eval' f =
   2.268 -  let val T = fastype_of f
   2.269 -  in
   2.270 -    Const (@{const_name Predicate.eval}, T --> dest_pred_enumT T --> HOLogic.boolT) $ f
   2.271 -  end; 
   2.272 -
   2.273 -val mk_sup = HOLogic.mk_binop @{const_name sup};
   2.274 -
   2.275  (* for simple modes (e.g. parameters) only: better call it param_funT *)
   2.276  (* or even better: remove it and only use funT'_of - some modifications to funT'_of necessary *) 
   2.277  fun funT_of T NONE = T
   2.278 @@ -424,13 +434,16 @@
   2.279         (v', mk_empty U')]))
   2.280    end;
   2.281  
   2.282 -fun modename thy name mode = let
   2.283 +fun modename_of thy name mode = let
   2.284      val v = (PredModetab.lookup (#names (IndCodegenData.get thy)) (name, mode))
   2.285 -  in if (is_some v) then the v
   2.286 -     else error ("fun modename - definition not found: name: " ^ name ^ " mode: " ^  (makestring mode))
   2.287 +  in if (is_some v) then the v (*FIXME use case here*)
   2.288 +     else error ("fun modename_of - definition not found: name: " ^ name ^ " mode: " ^  (makestring mode))
   2.289    end
   2.290  
   2.291 -(* function can be removed *)
   2.292 +fun modes_of thy =
   2.293 +  these o Symtab.lookup ((#modes o IndCodegenData.get) thy);
   2.294 +
   2.295 +(*FIXME function can be removed*)
   2.296  fun mk_funcomp f t =
   2.297    let
   2.298      val names = Term.add_free_names t [];
   2.299 @@ -449,7 +462,7 @@
   2.300      val f' = case f of
   2.301          Const (name, T) =>
   2.302            if AList.defined op = modes name then
   2.303 -            Const (modename thy name (iss, is'), funT'_of (iss, is') T)
   2.304 +            Const (modename_of thy name (iss, is'), funT'_of (iss, is') T)
   2.305            else error "compile param: Not an inductive predicate with correct mode"
   2.306        | Free (name, T) => Free (name, funT_of T (SOME is'))
   2.307      in list_comb (f', params' @ args') end
   2.308 @@ -463,7 +476,7 @@
   2.309                 val (Ts, Us) = get_args is
   2.310                   (curry Library.drop (length ms) (fst (strip_type T)))
   2.311                 val params' = map (compile_param thy modes) (ms ~~ params)
   2.312 -               val mode_id = modename thy name mode
   2.313 +               val mode_id = modename_of thy name mode
   2.314               in list_comb (Const (mode_id, ((map fastype_of params') @ Ts) --->
   2.315                 mk_pred_enumT (mk_tupleT Us)), params')
   2.316               end
   2.317 @@ -556,7 +569,7 @@
   2.318      val cl_ts =
   2.319        map (fn cl => compile_clause thy
   2.320          all_vs param_vs modes mode cl (mk_tuple xs)) cls;
   2.321 -    val mode_id = modename thy s mode
   2.322 +    val mode_id = modename_of thy s mode
   2.323    in
   2.324      HOLogic.mk_Trueprop (HOLogic.mk_eq
   2.325        (list_comb (Const (mode_id, (Ts1' @ Us1) --->
   2.326 @@ -591,7 +604,7 @@
   2.327      fold Term.add_consts intrs [] |> map fst
   2.328      |> filter_out (member (op =) preds) |> filter (is_ind_pred thy)
   2.329  
   2.330 -fun print_arities arities = message ("Arities:\n" ^
   2.331 +fun print_arities arities = tracing ("Arities:\n" ^
   2.332    cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
   2.333      space_implode " -> " (map
   2.334        (fn NONE => "X" | SOME k' => string_of_int k')
   2.335 @@ -691,10 +704,10 @@
   2.336  (* Proving equivalence of term *)
   2.337  
   2.338  
   2.339 -fun intro_rule thy pred mode = modename thy pred mode
   2.340 +fun intro_rule thy pred mode = modename_of thy pred mode
   2.341      |> Symtab.lookup (#function_intros (IndCodegenData.get thy)) |> the
   2.342  
   2.343 -fun elim_rule thy pred mode = modename thy pred mode
   2.344 +fun elim_rule thy pred mode = modename_of thy pred mode
   2.345      |> Symtab.lookup (#function_elims (IndCodegenData.get thy)) |> the
   2.346  
   2.347  fun pred_intros thy predname = let
   2.348 @@ -711,7 +724,7 @@
   2.349    end
   2.350  
   2.351  fun function_definition thy pred mode =
   2.352 -  modename thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the
   2.353 +  modename_of thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the
   2.354  
   2.355  fun is_Type (Type _) = true
   2.356    | is_Type _ = false
   2.357 @@ -973,7 +986,7 @@
   2.358      in nth (#elims (snd ind_result)) index end)
   2.359  
   2.360  fun prove_one_direction thy all_vs param_vs modes clauses ((pred, T), mode) = let
   2.361 -  val elim_rule = the (Symtab.lookup (#function_elims (IndCodegenData.get thy)) (modename thy pred mode))
   2.362 +  val elim_rule = the (Symtab.lookup (#function_elims (IndCodegenData.get thy)) (modename_of thy pred mode))
   2.363  (*  val ind_result = InductivePackage.the_inductive (ProofContext.init thy) pred
   2.364    val index = find_index (fn s => s = pred) (#names (fst ind_result))
   2.365    val (_, T) = dest_Const (nth (#preds (snd ind_result)) index) *)
   2.366 @@ -1225,7 +1238,7 @@
   2.367  (* main function *********************************************************************)
   2.368  (*************************************************************************************)
   2.369  
   2.370 -fun create_def_equation' ind_name (mode : (int list option list * int list) option) thy =
   2.371 +fun create_def_equation' ind_name (mode : mode option) thy =
   2.372  let
   2.373    val _ = tracing ("starting create_def_equation' with " ^ ind_name)
   2.374    val (prednames, preds) = 
   2.375 @@ -1249,6 +1262,7 @@
   2.376    val _ = tracing ("calling preds: " ^ makestring name_of_calls)
   2.377    val _ = tracing "starting recursive compilations"
   2.378    fun rec_call name thy = 
   2.379 +    (*FIXME use member instead of infix mem*)
   2.380      if not (name mem (Symtab.keys (#modes (IndCodegenData.get thy)))) then
   2.381        create_def_equation name thy else thy
   2.382    val thy'' = fold rec_call name_of_calls thy'