src/Pure/Isar/code.ML
changeset 31998 2c7a24f74db9
parent 31971 8c1b845ed105
child 32070 c670a31c964c
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4    val print_codesetup: theory -> unit
     1.5  
     1.6    (*infrastructure*)
     1.7 -  val add_attribute: string * attribute parser -> theory -> theory
     1.8 +  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
     1.9    val purge_data: theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -235,31 +235,6 @@
    1.13    end;
    1.14  
    1.15  
    1.16 -(** code attributes **)
    1.17 -
    1.18 -structure Code_Attr = TheoryDataFun (
    1.19 -  type T = (string * attribute parser) list;
    1.20 -  val empty = [];
    1.21 -  val copy = I;
    1.22 -  val extend = I;
    1.23 -  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
    1.24 -);
    1.25 -
    1.26 -fun add_attribute (attr as (name, _)) =
    1.27 -  let
    1.28 -    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
    1.29 -      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
    1.30 -  in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
    1.31 -    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
    1.32 -  end;
    1.33 -
    1.34 -val _ = Context.>> (Context.map_theory
    1.35 -  (Attrib.setup (Binding.name "code")
    1.36 -    (Scan.peek (fn context =>
    1.37 -      List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
    1.38 -    "declare theorems for code generation"));
    1.39 -
    1.40 -
    1.41  (** data store **)
    1.42  
    1.43  (* code equations *)
    1.44 @@ -543,7 +518,7 @@
    1.45        in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
    1.46      fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
    1.47        let
    1.48 -        val _ = if tyco' <> tyco
    1.49 +        val _ = if (tyco' : string) <> tyco
    1.50            then error "Different type constructors in constructor set"
    1.51            else ();
    1.52          val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
    1.53 @@ -911,18 +886,32 @@
    1.54   of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
    1.55    | NONE => thy;
    1.56  
    1.57 +structure Code_Attr = TheoryDataFun (
    1.58 +  type T = (string -> thm -> theory -> theory) option;
    1.59 +  val empty = NONE;
    1.60 +  val copy = I;
    1.61 +  val extend = I;
    1.62 +  fun merge _ (NONE, f2) = f2
    1.63 +    | merge _ (f1, _) = f1;
    1.64 +);
    1.65 +
    1.66 +fun set_code_target_attr f = Code_Attr.map (K (SOME f));
    1.67 +
    1.68  val _ = Context.>> (Context.map_theory
    1.69    (let
    1.70      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    1.71 -    fun add_simple_attribute (name, f) =
    1.72 -      add_attribute (name, Scan.succeed (mk_attribute f));
    1.73 -    fun add_del_attribute (name, (add, del)) =
    1.74 -      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
    1.75 -        || Scan.succeed (mk_attribute add))
    1.76 +    val code_attribute_parser =
    1.77 +      Args.del |-- Scan.succeed (mk_attribute del_eqn)
    1.78 +      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
    1.79 +      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
    1.80 +           (fn prefix => mk_attribute (fn thm => fn thy => thy
    1.81 +             |> add_warning_eqn thm
    1.82 +             |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
    1.83 +      || Scan.succeed (mk_attribute add_warning_eqn);
    1.84    in
    1.85      Type_Interpretation.init
    1.86 -    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
    1.87 -    #> add_simple_attribute ("nbe", add_nbe_eqn)
    1.88 +    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
    1.89 +        "declare theorems for code generation"
    1.90    end));
    1.91  
    1.92