Fixed problem with "code ind" attribute that caused code generator to
authorberghofe
Thu Aug 21 16:20:45 2003 +0200 (2003-08-21)
changeset 14162f05f299512e9
parent 14161 73ad4884441f
child 14163 5ffa75ce4919
Fixed problem with "code ind" attribute that caused code generator to
fail for mutually recursive predicates.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Aug 21 16:18:43 2003 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Aug 21 16:20:45 2003 +0200
     1.3 @@ -22,11 +22,13 @@
     1.4  structure CodegenArgs =
     1.5  struct
     1.6    val name = "HOL/inductive_codegen";
     1.7 -  type T = thm list Symtab.table;
     1.8 -  val empty = Symtab.empty;
     1.9 +  type T = thm list Symtab.table * unit Graph.T;
    1.10 +  val empty = (Symtab.empty, Graph.empty);
    1.11    val copy = I;
    1.12    val prep_ext = I;
    1.13 -  val merge = Symtab.merge_multi Drule.eq_thm_prop;
    1.14 +  fun merge ((tab1, graph1), (tab2, graph2)) =
    1.15 +    (Symtab.merge_multi Drule.eq_thm_prop (tab1, tab2),
    1.16 +     Graph.merge (K true) (graph1, graph2));
    1.17    fun print _ _ = ();
    1.18  end;
    1.19  
    1.20 @@ -35,22 +37,37 @@
    1.21  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    1.22    string_of_thm thm);
    1.23  
    1.24 +fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
    1.25 +
    1.26  fun add (p as (thy, thm)) =
    1.27 -  let val tab = CodegenData.get thy;
    1.28 +  let val (tab, graph) = CodegenData.get thy;
    1.29    in (case concl_of thm of
    1.30        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    1.31 -        Const (s, _) => (CodegenData.put (Symtab.update ((s,
    1.32 -          if_none (Symtab.lookup (tab, s)) [] @ [thm]), tab)) thy, thm)
    1.33 +        Const (s, _) =>
    1.34 +          let val cs = foldr add_term_consts (prems_of thm, [])
    1.35 +          in (CodegenData.put
    1.36 +            (Symtab.update ((s,
    1.37 +               if_none (Symtab.lookup (tab, s)) [] @ [thm]), tab),
    1.38 +             foldr (uncurry (Graph.add_edge o pair s))
    1.39 +               (cs, foldl add_node (graph, s :: cs))) thy, thm)
    1.40 +          end
    1.41        | _ => (warn thm; p))
    1.42      | _ => (warn thm; p))
    1.43    end;
    1.44  
    1.45  fun get_clauses thy s =
    1.46 -  (case Symtab.lookup (CodegenData.get thy, s) of
    1.47 -     None => (case InductivePackage.get_inductive thy s of
    1.48 -       None => None
    1.49 -     | Some ({names, ...}, {intrs, ...}) => Some (names, intrs))
    1.50 -   | Some thms => Some ([s], thms));
    1.51 +  let val (tab, graph) = CodegenData.get thy
    1.52 +  in case Symtab.lookup (tab, s) of
    1.53 +      None => (case InductivePackage.get_inductive thy s of
    1.54 +        None => None
    1.55 +      | Some ({names, ...}, {intrs, ...}) => Some (names, intrs))
    1.56 +    | Some _ =>
    1.57 +        let val Some names = find_first
    1.58 +          (fn xs => s mem xs) (Graph.strong_conn graph)
    1.59 +        in Some (names,
    1.60 +          flat (map (fn s => the (Symtab.lookup (tab, s))) names))
    1.61 +        end
    1.62 +  end;
    1.63  
    1.64  
    1.65  (**** improper tuples ****)