src/HOL/Tools/recfun_codegen.ML
changeset 15531 08c8dad8e399
parent 15321 694f9d3ce90d
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -53,8 +53,8 @@
     1.4      val tab = CodegenData.get thy;
     1.5      val (s, _) = const_of (prop_of thm);
     1.6    in case Symtab.lookup (tab, s) of
     1.7 -      None => p
     1.8 -    | Some thms => (CodegenData.put (Symtab.update ((s,
     1.9 +      NONE => p
    1.10 +    | SOME thms => (CodegenData.put (Symtab.update ((s,
    1.11          gen_rem eq_thm (thms, thm)), tab)) thy, thm)
    1.12    end handle TERM _ => (warn thm; p);
    1.13  
    1.14 @@ -68,14 +68,14 @@
    1.15  
    1.16  fun get_equations thy (s, T) =
    1.17    (case Symtab.lookup (CodegenData.get thy, s) of
    1.18 -     None => []
    1.19 -   | Some thms => preprocess thy (del_redundant thy []
    1.20 +     NONE => []
    1.21 +   | SOME thms => preprocess thy (del_redundant thy []
    1.22         (filter (fn thm => is_instance thy T
    1.23           (snd (const_of (prop_of thm)))) thms)));
    1.24  
    1.25  fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
    1.26    (case get_defn thy s T of
    1.27 -     Some (_, Some i) => "_def" ^ string_of_int i
    1.28 +     SOME (_, SOME i) => "_def" ^ string_of_int i
    1.29     | _ => "");
    1.30  
    1.31  exception EQN of string * typ * string;
    1.32 @@ -104,19 +104,19 @@
    1.33        end;
    1.34  
    1.35      fun put_code fundef = Graph.map_node dname
    1.36 -      (K (Some (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0,
    1.37 +      (K (SOME (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0,
    1.38        separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
    1.39  
    1.40    in
    1.41      (case try (Graph.get_node gr) dname of
    1.42 -       None =>
    1.43 +       NONE =>
    1.44           let
    1.45             val gr1 = Graph.add_edge (dname, dep)
    1.46 -             (Graph.new_node (dname, (Some (EQN (s, T, "")), "")) gr);
    1.47 +             (Graph.new_node (dname, (SOME (EQN (s, T, "")), "")) gr);
    1.48             val (gr2, fundef) = mk_fundef "" "fun " gr1 eqs';
    1.49             val xs = cycle gr2 ([], dname);
    1.50             val cs = map (fn x => case Graph.get_node gr2 x of
    1.51 -               (Some (EQN (s, T, _)), _) => (s, T)
    1.52 +               (SOME (EQN (s, T, _)), _) => (s, T)
    1.53               | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
    1.54                  implode (separate ", " xs))) xs
    1.55           in (case xs of
    1.56 @@ -129,12 +129,12 @@
    1.57                   val (gr3, fundef') = mk_fundef "" "fun "
    1.58                     (Graph.add_edge (dname, dep)
    1.59                       (foldr (uncurry Graph.new_node) (map (fn k =>
    1.60 -                       (k, (Some (EQN ("", dummyT, dname)), ""))) xs,
    1.61 +                       (k, (SOME (EQN ("", dummyT, dname)), ""))) xs,
    1.62                           Graph.del_nodes xs gr2))) eqs''
    1.63                 in put_code fundef' gr3 end
    1.64               else gr2)
    1.65           end
    1.66 -     | Some (Some (EQN (_, _, s)), _) =>
    1.67 +     | SOME (SOME (EQN (_, _, s)), _) =>
    1.68           if s = "" then
    1.69             if dname = dep then gr else Graph.add_edge (dname, dep) gr
    1.70           else if s = dep then gr else Graph.add_edge (s, dep) gr)
    1.71 @@ -142,15 +142,15 @@
    1.72  
    1.73  fun recfun_codegen thy gr dep brack t = (case strip_comb t of
    1.74      (Const (p as (s, T)), ts) => (case (get_equations thy p, get_assoc_code thy s T) of
    1.75 -       ([], _) => None
    1.76 -     | (_, Some _) => None
    1.77 -     | (eqns, None) =>
    1.78 +       ([], _) => NONE
    1.79 +     | (_, SOME _) => NONE
    1.80 +     | (eqns, NONE) =>
    1.81          let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)
    1.82          in
    1.83 -          Some (add_rec_funs thy gr' dep (map prop_of eqns),
    1.84 +          SOME (add_rec_funs thy gr' dep (map prop_of eqns),
    1.85              mk_app brack (Pretty.str (mk_poly_id thy p)) ps)
    1.86          end)
    1.87 -  | _ => None);
    1.88 +  | _ => NONE);
    1.89  
    1.90  
    1.91  val setup =