src/HOL/Tools/recfun_codegen.ML
changeset 16645 a152d6b21c31
parent 16424 18a07ad8fea8
child 17144 6642e0f96f44
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Jul 01 14:11:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Jul 01 14:13:40 2005 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  signature RECFUN_CODEGEN =
     1.6  sig
     1.7 -  val add: theory attribute
     1.8 +  val add: string option -> theory attribute
     1.9 +  val del: theory attribute
    1.10    val setup: (theory -> theory) list
    1.11  end;
    1.12  
    1.13 @@ -19,11 +20,11 @@
    1.14  structure CodegenData = TheoryDataFun
    1.15  (struct
    1.16    val name = "HOL/recfun_codegen";
    1.17 -  type T = thm list Symtab.table;
    1.18 +  type T = (thm * string option) list Symtab.table;
    1.19    val empty = Symtab.empty;
    1.20    val copy = I;
    1.21    val extend = I;
    1.22 -  fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
    1.23 +  fun merge _ = Symtab.merge_multi' (Drule.eq_thm_prop o pairself fst);
    1.24    fun print _ _ = ();
    1.25  end);
    1.26  
    1.27 @@ -35,14 +36,14 @@
    1.28  fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    1.29    string_of_thm thm);
    1.30  
    1.31 -fun add (p as (thy, thm)) =
    1.32 +fun add optmod (p as (thy, thm)) =
    1.33    let
    1.34      val tab = CodegenData.get thy;
    1.35      val (s, _) = const_of (prop_of thm);
    1.36    in
    1.37      if Pattern.pattern (lhs_of thm) then
    1.38        (CodegenData.put (Symtab.update ((s,
    1.39 -        thm :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
    1.40 +        (thm, optmod) :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
    1.41      else (warn thm; p)
    1.42    end handle TERM _ => (warn thm; p);
    1.43  
    1.44 @@ -53,7 +54,7 @@
    1.45    in case Symtab.lookup (tab, s) of
    1.46        NONE => p
    1.47      | SOME thms => (CodegenData.put (Symtab.update ((s,
    1.48 -        gen_rem eq_thm (thms, thm)), tab)) thy, thm)
    1.49 +        gen_rem (eq_thm o apfst fst) (thms, thm)), tab)) thy, thm)
    1.50    end handle TERM _ => (warn thm; p);
    1.51  
    1.52  fun del_redundant thy eqs [] = eqs
    1.53 @@ -61,20 +62,27 @@
    1.54      let
    1.55        val tsig = Sign.tsig_of (sign_of thy);
    1.56        val matches = curry
    1.57 -        (Pattern.matches tsig o pairself lhs_of)
    1.58 +        (Pattern.matches tsig o pairself (lhs_of o fst))
    1.59      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    1.60  
    1.61 -fun get_equations thy (s, T) =
    1.62 +fun get_equations thy defs (s, T) =
    1.63    (case Symtab.lookup (CodegenData.get thy, s) of
    1.64 -     NONE => []
    1.65 -   | SOME thms => preprocess thy (del_redundant thy []
    1.66 -       (List.filter (fn thm => is_instance thy T
    1.67 -         (snd (const_of (prop_of thm)))) thms)));
    1.68 +     NONE => ([], "")
    1.69 +   | SOME thms => 
    1.70 +       let val thms' = del_redundant thy []
    1.71 +         (List.filter (fn (thm, _) => is_instance thy T
    1.72 +           (snd (const_of (prop_of thm)))) thms)
    1.73 +       in if null thms' then ([], "")
    1.74 +         else (preprocess thy (map fst thms'),
    1.75 +           case snd (snd (split_last thms')) of
    1.76 +               NONE => (case get_defn thy defs s T of
    1.77 +                   NONE => thyname_of_const s thy
    1.78 +                 | SOME ((_, (thyname, _)), _) => thyname)
    1.79 +             | SOME thyname => thyname)
    1.80 +       end);
    1.81  
    1.82 -fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
    1.83 -  (case get_defn thy s T of
    1.84 -     SOME (_, SOME i) => "_def" ^ string_of_int i
    1.85 -   | _ => "");
    1.86 +fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    1.87 +  SOME (_, SOME i) => "_def" ^ string_of_int i | _ => "");
    1.88  
    1.89  exception EQN of string * typ * string;
    1.90  
    1.91 @@ -82,27 +90,27 @@
    1.92    if x mem xs then xs
    1.93    else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths g (x, x)));
    1.94  
    1.95 -fun add_rec_funs thy gr dep eqs =
    1.96 +fun add_rec_funs thy defs gr dep eqs thyname =
    1.97    let
    1.98 -    fun dest_eq t =
    1.99 -      (mk_poly_id thy (const_of t), dest_eqn (rename_term t));
   1.100 +    fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
   1.101 +      dest_eqn (rename_term t));
   1.102      val eqs' = map dest_eq eqs;
   1.103      val (dname, _) :: _ = eqs';
   1.104      val (s, T) = const_of (hd eqs);
   1.105  
   1.106 -    fun mk_fundef fname prfx gr [] = (gr, [])
   1.107 -      | mk_fundef fname prfx gr ((fname', (lhs, rhs)) :: xs) =
   1.108 +    fun mk_fundef thyname fname prfx gr [] = (gr, [])
   1.109 +      | mk_fundef thyname fname prfx gr ((fname', (lhs, rhs)) :: xs) =
   1.110        let
   1.111 -        val (gr1, pl) = invoke_codegen thy dname false (gr, lhs);
   1.112 -        val (gr2, pr) = invoke_codegen thy dname false (gr1, rhs);
   1.113 -        val (gr3, rest) = mk_fundef fname' "and " gr2 xs
   1.114 +        val (gr1, pl) = invoke_codegen thy defs dname thyname false (gr, lhs);
   1.115 +        val (gr2, pr) = invoke_codegen thy defs dname thyname false (gr1, rhs);
   1.116 +        val (gr3, rest) = mk_fundef thyname fname' "and " gr2 xs
   1.117        in
   1.118          (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
   1.119             pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
   1.120        end;
   1.121  
   1.122 -    fun put_code fundef = Graph.map_node dname
   1.123 -      (K (SOME (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0,
   1.124 +    fun put_code thyname fundef = Graph.map_node dname
   1.125 +      (K (SOME (EQN ("", dummyT, dname)), thyname, Pretty.string_of (Pretty.blk (0,
   1.126        separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
   1.127  
   1.128    in
   1.129 @@ -110,43 +118,47 @@
   1.130         NONE =>
   1.131           let
   1.132             val gr1 = Graph.add_edge (dname, dep)
   1.133 -             (Graph.new_node (dname, (SOME (EQN (s, T, "")), "")) gr);
   1.134 -           val (gr2, fundef) = mk_fundef "" "fun " gr1 eqs';
   1.135 +             (Graph.new_node (dname, (SOME (EQN (s, T, "")), "", "")) gr);
   1.136 +           val (gr2, fundef) = mk_fundef thyname "" "fun " gr1 eqs';
   1.137             val xs = cycle gr2 ([], dname);
   1.138             val cs = map (fn x => case Graph.get_node gr2 x of
   1.139 -               (SOME (EQN (s, T, _)), _) => (s, T)
   1.140 +               (SOME (EQN (s, T, _)), _, _) => (s, T)
   1.141               | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   1.142                  implode (separate ", " xs))) xs
   1.143           in (case xs of
   1.144 -             [_] => put_code fundef gr2
   1.145 +             [_] => put_code thyname fundef gr2
   1.146             | _ =>
   1.147               if not (dep mem xs) then
   1.148                 let
   1.149 -                 val eqs'' = map (dest_eq o prop_of)
   1.150 -                   (List.concat (map (get_equations thy) cs));
   1.151 -                 val (gr3, fundef') = mk_fundef "" "fun "
   1.152 +                 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   1.153 +                 val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   1.154 +                 val (gr3, fundef') = mk_fundef thyname "" "fun "
   1.155                     (Graph.add_edge (dname, dep)
   1.156                       (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
   1.157                         (map (fn k =>
   1.158 -                         (k, (SOME (EQN ("", dummyT, dname)), ""))) xs))) eqs''
   1.159 -               in put_code fundef' gr3 end
   1.160 +                         (k, (SOME (EQN ("", dummyT, dname)), thyname, ""))) xs))) eqs''
   1.161 +               in put_code thyname fundef' gr3 end
   1.162               else gr2)
   1.163           end
   1.164 -     | SOME (SOME (EQN (_, _, s)), _) =>
   1.165 +     | SOME (SOME (EQN (_, _, s)), _, _) =>
   1.166           if s = "" then
   1.167             if dname = dep then gr else Graph.add_edge (dname, dep) gr
   1.168           else if s = dep then gr else Graph.add_edge (s, dep) gr)
   1.169    end;
   1.170  
   1.171 -fun recfun_codegen thy gr dep brack t = (case strip_comb t of
   1.172 -    (Const (p as (s, T)), ts) => (case (get_equations thy p, get_assoc_code thy s T) of
   1.173 -       ([], _) => NONE
   1.174 +fun recfun_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   1.175 +    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
   1.176 +       (([], _), _) => NONE
   1.177       | (_, SOME _) => NONE
   1.178 -     | (eqns, NONE) =>
   1.179 -        let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)
   1.180 +     | ((eqns, thyname'), NONE) =>
   1.181 +        let
   1.182 +          val (gr', ps) = foldl_map
   1.183 +            (invoke_codegen thy defs dep thyname true) (gr, ts);
   1.184 +          val suffix = mk_suffix thy defs p
   1.185          in
   1.186 -          SOME (add_rec_funs thy gr' dep (map prop_of eqns),
   1.187 -            mk_app brack (Pretty.str (mk_poly_id thy p)) ps)
   1.188 +          SOME (add_rec_funs thy defs gr' dep (map prop_of eqns) thyname',
   1.189 +            mk_app brack (Pretty.str
   1.190 +              (mk_const_id (sign_of thy) thyname thyname' s ^ suffix)) ps)
   1.191          end)
   1.192    | _ => NONE);
   1.193  
   1.194 @@ -154,6 +166,8 @@
   1.195  val setup =
   1.196    [CodegenData.init,
   1.197     add_codegen "recfun" recfun_codegen,
   1.198 -   add_attribute "" (Args.del |-- Scan.succeed del || Scan.succeed add)];
   1.199 +   add_attribute ""
   1.200 +     (   Args.del |-- Scan.succeed del
   1.201 +      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
   1.202  
   1.203  end;