1.1 --- a/src/Pure/codegen.ML Thu Dec 20 14:55:28 2001 +0100
1.2 +++ b/src/Pure/codegen.ML Thu Dec 20 14:57:15 2001 +0100
1.3 @@ -21,6 +21,7 @@
1.4
1.5 val add_codegen: string -> term codegen -> theory -> theory
1.6 val add_tycodegen: string -> typ codegen -> theory -> theory
1.7 + val add_attribute: string -> theory attribute -> theory -> theory
1.8 val print_codegens: theory -> unit
1.9 val generate_code: theory -> (string * string) list -> string
1.10 val generate_code_i: theory -> (string * term) list -> string
1.11 @@ -90,18 +91,24 @@
1.12 {codegens : (string * term codegen) list,
1.13 tycodegens : (string * typ codegen) list,
1.14 consts : ((string * typ) * term mixfix list) list,
1.15 - types : (string * typ mixfix list) list};
1.16 + types : (string * typ mixfix list) list,
1.17 + attrs: (string * theory attribute) list};
1.18
1.19 - val empty = {codegens = [], tycodegens = [], consts = [], types = []};
1.20 + val empty =
1.21 + {codegens = [], tycodegens = [], consts = [], types = [], attrs = []};
1.22 val copy = I;
1.23 val prep_ext = I;
1.24
1.25 - fun merge ({codegens = codegens1, tycodegens = tycodegens1, consts = consts1, types = types1},
1.26 - {codegens = codegens2, tycodegens = tycodegens2, consts = consts2, types = types2}) =
1.27 + fun merge
1.28 + ({codegens = codegens1, tycodegens = tycodegens1,
1.29 + consts = consts1, types = types1, attrs = attrs1},
1.30 + {codegens = codegens2, tycodegens = tycodegens2,
1.31 + consts = consts2, types = types2, attrs = attrs2}) =
1.32 {codegens = rev (merge_alists (rev codegens1) (rev codegens2)),
1.33 tycodegens = rev (merge_alists (rev tycodegens1) (rev tycodegens2)),
1.34 - consts = merge_alists consts1 consts2,
1.35 - types = merge_alists types1 types2};
1.36 + consts = merge_alists consts1 consts2,
1.37 + types = merge_alists types1 types2,
1.38 + attrs = merge_alists attrs1 attrs2};
1.39
1.40 fun print sg ({codegens, tycodegens, ...} : T) =
1.41 Pretty.writeln (Pretty.chunks
1.42 @@ -116,28 +123,48 @@
1.43 (**** add new code generators to theory ****)
1.44
1.45 fun add_codegen name f thy =
1.46 - let val {codegens, tycodegens, consts, types} = CodegenData.get thy
1.47 + let val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy
1.48 in (case assoc (codegens, name) of
1.49 None => CodegenData.put {codegens = (name, f) :: codegens,
1.50 - tycodegens = tycodegens, consts = consts, types = types} thy
1.51 + tycodegens = tycodegens, consts = consts, types = types,
1.52 + attrs = attrs} thy
1.53 | Some _ => error ("Code generator " ^ name ^ " already declared"))
1.54 end;
1.55
1.56 fun add_tycodegen name f thy =
1.57 - let val {codegens, tycodegens, consts, types} = CodegenData.get thy
1.58 + let val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy
1.59 in (case assoc (tycodegens, name) of
1.60 None => CodegenData.put {tycodegens = (name, f) :: tycodegens,
1.61 - codegens = codegens, consts = consts, types = types} thy
1.62 + codegens = codegens, consts = consts, types = types,
1.63 + attrs = attrs} thy
1.64 | Some _ => error ("Code generator " ^ name ^ " already declared"))
1.65 end;
1.66
1.67
1.68 +(**** code attribute ****)
1.69 +
1.70 +fun add_attribute name att thy =
1.71 + let val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy
1.72 + in (case assoc (attrs, name) of
1.73 + None => CodegenData.put {tycodegens = tycodegens,
1.74 + codegens = codegens, consts = consts, types = types,
1.75 + attrs = (name, att) :: attrs} thy
1.76 + | Some _ => error ("Code attribute " ^ name ^ " already declared"))
1.77 + end;
1.78 +
1.79 +val code_attr =
1.80 + Attrib.syntax (Scan.depend (fn thy => Scan.optional Args.name "" >>
1.81 + (fn name => (thy, case assoc (#attrs (CodegenData.get thy), name) of
1.82 + None => error ("Unknown code attribute: " ^ quote name)
1.83 + | Some att => att))));
1.84 +
1.85 +
1.86 (**** associate constants with target language code ****)
1.87
1.88 fun gen_assoc_consts prep_type xs thy = foldl (fn (thy, (s, tyopt, syn)) =>
1.89 let
1.90 val sg = sign_of thy;
1.91 - val {codegens, tycodegens, consts, types} = CodegenData.get thy;
1.92 + val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy;
1.93 val cname = Sign.intern_const sg s;
1.94 in
1.95 (case Sign.const_type sg cname of
1.96 @@ -152,7 +179,8 @@
1.97 in (case assoc (consts, (cname, T')) of
1.98 None => CodegenData.put {codegens = codegens,
1.99 tycodegens = tycodegens,
1.100 - consts = ((cname, T'), syn) :: consts, types = types} thy
1.101 + consts = ((cname, T'), syn) :: consts,
1.102 + types = types, attrs = attrs} thy
1.103 | Some _ => error ("Constant " ^ cname ^ " already associated with code"))
1.104 end
1.105 | _ => error ("Not a constant: " ^ s))
1.106 @@ -165,13 +193,13 @@
1.107
1.108 fun assoc_types xs thy = foldl (fn (thy, (s, syn)) =>
1.109 let
1.110 - val {codegens, tycodegens, consts, types} = CodegenData.get thy;
1.111 + val {codegens, tycodegens, consts, types, attrs} = CodegenData.get thy;
1.112 val tc = Sign.intern_tycon (sign_of thy) s
1.113 in
1.114 (case assoc (types, tc) of
1.115 None => CodegenData.put {codegens = codegens,
1.116 tycodegens = tycodegens, consts = consts,
1.117 - types = (tc, syn) :: types} thy
1.118 + types = (tc, syn) :: types, attrs = attrs} thy
1.119 | Some _ => error ("Type " ^ tc ^ " already associated with code"))
1.120 end) (thy, xs);
1.121
1.122 @@ -212,7 +240,8 @@
1.123 val (xs as x::_) = explode (rename (space_implode "_"
1.124 (NameSpace.unpack (Sign.cond_extern sg kind s))));
1.125 fun check_str [] = ""
1.126 - | check_str (x::xs) =
1.127 + | check_str (" " :: xs) = "_" ^ check_str xs
1.128 + | check_str (x :: xs) =
1.129 (if Symbol.is_letter x orelse Symbol.is_digit x orelse x="_" then x
1.130 else "_" ^ string_of_int (ord x)) ^ check_str xs
1.131 in
1.132 @@ -462,7 +491,10 @@
1.133 [CodegenData.init,
1.134 add_codegen "default" default_codegen,
1.135 add_tycodegen "default" default_tycodegen,
1.136 - assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]];
1.137 + assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")],
1.138 + Attrib.add_attributes [("code",
1.139 + (code_attr, K Attrib.undef_local_attribute),
1.140 + "declare theorems for code generation")]];
1.141
1.142 end;
1.143