- Added cycle test to function mk_ind_def to avoid non-termination
authorberghofe
Thu Aug 02 17:29:40 2007 +0200 (2007-08-02)
changeset 24129591394d9ee66
parent 24128 654b3a988f6a
child 24130 5ab8044b6d46
- Added cycle test to function mk_ind_def to avoid non-termination
of code generator.
- Functions generated from inductive predicates having neither
parameters nor input arguments now take a unit element as an
argument, otherwise the generated code would be ill-formed.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Aug 02 16:12:02 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Aug 02 17:29:40 2007 +0200
     1.3 @@ -325,8 +325,10 @@
     1.4                 val (gr', (ps, mode_id)) = foldl_map
     1.5                     (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
     1.6                   modename module name mode;
     1.7 -               val (gr'', ps') = foldl_map
     1.8 -                 (invoke_codegen thy defs dep module true) (gr', args2)
     1.9 +               val (gr'', ps') = (case mode of
    1.10 +                   ([], []) => (gr', [Pretty.str "()"])
    1.11 +                 | _ => foldl_map
    1.12 +                     (invoke_codegen thy defs dep module true) (gr', args2))
    1.13               in (gr', (if brack andalso not (null ps andalso null ps') then
    1.14                 single o parens o Pretty.block else I)
    1.15                   (List.concat (separate [Pretty.brk 1]
    1.16 @@ -398,7 +400,8 @@
    1.17                     val (gr2, in_ps) = foldl_map
    1.18                       (invoke_codegen thy defs dep module true) (gr1, in_ts);
    1.19                     val (gr3, ps) = if is_ind t then
    1.20 -                       apsnd (fn ps => ps @ Pretty.brk 1 ::
    1.21 +                       apsnd (fn ps => ps @
    1.22 +                           (if null in_ps then [] else [Pretty.brk 1]) @
    1.23                             separate (Pretty.brk 1) in_ps)
    1.24                           (compile_expr thy defs dep module false modes
    1.25                             (gr2, (mode, t)))
    1.26 @@ -442,7 +445,8 @@
    1.27      ((gr', "and "), Pretty.block
    1.28        ([Pretty.block (separate (Pretty.brk 1)
    1.29           (Pretty.str (prfx ^ mode_id) ::
    1.30 -           map Pretty.str arg_vs @ xs) @
    1.31 +           map Pretty.str arg_vs @
    1.32 +           (case mode of ([], []) => [Pretty.str "()"] | _ => xs)) @
    1.33           [Pretty.str " ="]),
    1.34          Pretty.brk 1] @
    1.35         List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
    1.36 @@ -491,7 +495,10 @@
    1.37              (gr, foldr add_term_consts [] ts)
    1.38  
    1.39  and mk_ind_def thy defs gr dep names module modecs intrs nparms =
    1.40 -  add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
    1.41 +  add_edge_acyclic (hd names, dep) gr handle
    1.42 +    Graph.CYCLES (xs :: _) =>
    1.43 +      error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs)
    1.44 +  | Graph.UNDEF _ =>
    1.45      let
    1.46        val _ $ u = Logic.strip_imp_concl (hd intrs);
    1.47        val args = List.take (snd (strip_comb u), nparms);