src/HOL/Tools/recfun_codegen.ML
changeset 42411 ff997038e8eb
parent 41448 72ba43b47c7f
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Apr 19 22:32:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Apr 19 23:57:28 2011 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    if member (op =) xs x then xs
     1.5    else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
     1.6  
     1.7 -fun add_rec_funs thy defs dep module eqs gr =
     1.8 +fun add_rec_funs thy mode defs dep module eqs gr =
     1.9    let
    1.10      fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    1.11        Logic.dest_equals (Codegen.rename_term t));
    1.12 @@ -81,10 +81,10 @@
    1.13      fun mk_fundef module fname first [] gr = ([], gr)
    1.14        | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
    1.15        let
    1.16 -        val (pl, gr1) = Codegen.invoke_codegen thy defs dname module false lhs gr;
    1.17 -        val (pr, gr2) = Codegen.invoke_codegen thy defs dname module false rhs gr1;
    1.18 +        val (pl, gr1) = Codegen.invoke_codegen thy mode defs dname module false lhs gr;
    1.19 +        val (pr, gr2) = Codegen.invoke_codegen thy mode defs dname module false rhs gr1;
    1.20          val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
    1.21 -        val (ty, gr4) = Codegen.invoke_tycodegen thy defs dname module false T gr3;
    1.22 +        val (ty, gr4) = Codegen.invoke_tycodegen thy mode defs dname module false T gr3;
    1.23          val num_args = (length o snd o strip_comb) lhs;
    1.24          val prfx = if fname = fname' then "  |"
    1.25            else if not first then "and"
    1.26 @@ -121,7 +121,7 @@
    1.27               if not (member (op =) xs dep) then
    1.28                 let
    1.29                   val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
    1.30 -                 val module' = Codegen.if_library thyname module;
    1.31 +                 val module' = Codegen.if_library mode thyname module;
    1.32                   val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
    1.33                   val (fundef', gr3) = mk_fundef module' "" true eqs''
    1.34                     (Codegen.add_edge (dname, dep)
    1.35 @@ -137,7 +137,7 @@
    1.36            else if s = dep then gr else Codegen.add_edge (s, dep) gr))
    1.37    end;
    1.38  
    1.39 -fun recfun_codegen thy defs dep module brack t gr =
    1.40 +fun recfun_codegen thy mode defs dep module brack t gr =
    1.41    (case strip_comb t of
    1.42      (Const (p as (s, T)), ts) =>
    1.43       (case (get_equations thy defs p, Codegen.get_assoc_code thy (s, T)) of
    1.44 @@ -145,12 +145,12 @@
    1.45       | (_, SOME _) => NONE
    1.46       | ((eqns, thyname), NONE) =>
    1.47          let
    1.48 -          val module' = Codegen.if_library thyname module;
    1.49 +          val module' = Codegen.if_library mode thyname module;
    1.50            val (ps, gr') = fold_map
    1.51 -            (Codegen.invoke_codegen thy defs dep module true) ts gr;
    1.52 +            (Codegen.invoke_codegen thy mode defs dep module true) ts gr;
    1.53            val suffix = mk_suffix thy defs p;
    1.54            val (module'', gr'') =
    1.55 -            add_rec_funs thy defs dep module' (map prop_of eqns) gr';
    1.56 +            add_rec_funs thy mode defs dep module' (map prop_of eqns) gr';
    1.57            val (fname, gr''') = Codegen.mk_const_id module'' (s ^ suffix) gr''
    1.58          in
    1.59            SOME (Codegen.mk_app brack (Codegen.str (Codegen.mk_qual_id module fname)) ps, gr''')