src/Pure/codegen.ML
changeset 23178 07ba6b58b3d2
parent 22921 475ff421a6a3
child 23655 d2d1138e0ddc
     1.1 --- a/src/Pure/codegen.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -359,7 +359,7 @@
     1.4  fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
     1.5  
     1.6  val code_attr =
     1.7 -  Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
     1.8 +  Attrib.syntax (Scan.peek (fn context => List.foldr op || Scan.fail (map mk_parser
     1.9      (#attrs (CodegenData.get (Context.theory_of context))))));
    1.10  
    1.11  val _ = Context.add_setup
    1.12 @@ -542,7 +542,7 @@
    1.13  
    1.14  fun rename_terms ts =
    1.15    let
    1.16 -    val names = foldr add_term_names
    1.17 +    val names = List.foldr add_term_names
    1.18        (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
    1.19      val reserved = filter ML_Syntax.is_reserved names;
    1.20      val (illegal, alt_names) = split_list (map_filter (fn s =>
    1.21 @@ -684,7 +684,7 @@
    1.22      val (Ts, _) = strip_type (fastype_of t);
    1.23      val j = i - length ts
    1.24    in
    1.25 -    foldr (fn (T, t) => Abs ("x", T, t))
    1.26 +    List.foldr (fn (T, t) => Abs ("x", T, t))
    1.27        (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
    1.28    end;
    1.29  
    1.30 @@ -862,15 +862,15 @@
    1.31      if module = "" then
    1.32        let
    1.33          val modules = distinct (op =) (map (#2 o snd) code);
    1.34 -        val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
    1.35 -          (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
    1.36 +        val mod_gr = fold_rev Graph.add_edge_acyclic
    1.37            (maps (fn (s, (_, module, _)) => map (pair module)
    1.38              (filter_out (equal module) (map (#2 o Graph.get_node gr)
    1.39 -              (Graph.imm_succs gr s)))) code);
    1.40 +              (Graph.imm_succs gr s)))) code)
    1.41 +          (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
    1.42          val modules' =
    1.43            rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
    1.44        in
    1.45 -        foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
    1.46 +        List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
    1.47            (map (rpair "") modules') code
    1.48        end handle Graph.CYCLES (cs :: _) =>
    1.49          error ("Cyclic dependency of modules:\n" ^ commas cs ^
    1.50 @@ -887,7 +887,7 @@
    1.51      val graphs = get_modules thy;
    1.52      val defs = mk_deftab thy;
    1.53      val gr = new_node ("<Top>", (NONE, module, ""))
    1.54 -      (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
    1.55 +      (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
    1.56          (Graph.merge (fn ((_, module, _), (_, module', _)) =>
    1.57             module = module') (gr, gr'),
    1.58           (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr