src/Pure/codegen.ML
changeset 24219 e558fe311376
parent 24166 7b28dc69bdbb
child 24280 c9867bdf2424
     1.1 --- a/src/Pure/codegen.ML	Fri Aug 10 17:04:24 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Fri Aug 10 17:04:34 2007 +0200
     1.3 @@ -26,7 +26,6 @@
     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 -> (Args.T list -> attribute * Args.T list) -> theory -> theory
     1.8    val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
     1.9    val preprocess: theory -> thm list -> thm list
    1.10    val preprocess_term: theory -> term -> term
    1.11 @@ -202,8 +201,6 @@
    1.12  
    1.13  (* theory data *)
    1.14  
    1.15 -structure CodeData = CodegenData;
    1.16 -
    1.17  structure CodegenData = TheoryDataFun
    1.18  (
    1.19    type T =
    1.20 @@ -211,29 +208,27 @@
    1.21       tycodegens : (string * typ codegen) list,
    1.22       consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
    1.23       types : (string * (typ mixfix list * (string * string) list)) list,
    1.24 -     attrs: (string * (Args.T list -> attribute * Args.T list)) list,
    1.25       preprocs: (stamp * (theory -> thm list -> thm list)) list,
    1.26       modules: codegr Symtab.table,
    1.27       test_params: test_params};
    1.28  
    1.29    val empty =
    1.30 -    {codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
    1.31 +    {codegens = [], tycodegens = [], consts = [], types = [],
    1.32       preprocs = [], modules = Symtab.empty, test_params = default_test_params};
    1.33    val copy = I;
    1.34    val extend = I;
    1.35  
    1.36    fun merge _
    1.37      ({codegens = codegens1, tycodegens = tycodegens1,
    1.38 -      consts = consts1, types = types1, attrs = attrs1,
    1.39 +      consts = consts1, types = types1,
    1.40        preprocs = preprocs1, modules = modules1, test_params = test_params1},
    1.41       {codegens = codegens2, tycodegens = tycodegens2,
    1.42 -      consts = consts2, types = types2, attrs = attrs2,
    1.43 +      consts = consts2, types = types2,
    1.44        preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
    1.45      {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
    1.46       tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
    1.47       consts = AList.merge (op =) (K true) (consts1, consts2),
    1.48       types = AList.merge (op =) (K true) (types1, types2),
    1.49 -     attrs = AList.merge (op =) (K true) (attrs1, attrs2),
    1.50       preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
    1.51       modules = Symtab.merge (K true) (modules1, modules2),
    1.52       test_params = merge_test_params test_params1 test_params2};
    1.53 @@ -253,10 +248,10 @@
    1.54  fun get_test_params thy = #test_params (CodegenData.get thy);
    1.55  
    1.56  fun map_test_params f thy =
    1.57 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.58 +  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
    1.59      CodegenData.get thy;
    1.60    in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
    1.61 -    consts = consts, types = types, attrs = attrs, preprocs = preprocs,
    1.62 +    consts = consts, types = types, preprocs = preprocs,
    1.63      modules = modules, test_params = f test_params} thy
    1.64    end;
    1.65  
    1.66 @@ -266,10 +261,10 @@
    1.67  fun get_modules thy = #modules (CodegenData.get thy);
    1.68  
    1.69  fun map_modules f thy =
    1.70 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.71 +  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
    1.72      CodegenData.get thy;
    1.73    in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
    1.74 -    consts = consts, types = types, attrs = attrs, preprocs = preprocs,
    1.75 +    consts = consts, types = types, preprocs = preprocs,
    1.76      modules = f modules, test_params = test_params} thy
    1.77    end;
    1.78  
    1.79 @@ -277,23 +272,23 @@
    1.80  (**** add new code generators to theory ****)
    1.81  
    1.82  fun add_codegen name f thy =
    1.83 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.84 +  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
    1.85      CodegenData.get thy
    1.86    in (case AList.lookup (op =) codegens name of
    1.87        NONE => CodegenData.put {codegens = (name, f) :: codegens,
    1.88          tycodegens = tycodegens, consts = consts, types = types,
    1.89 -        attrs = attrs, preprocs = preprocs, modules = modules,
    1.90 +        preprocs = preprocs, modules = modules,
    1.91          test_params = test_params} thy
    1.92      | SOME _ => error ("Code generator " ^ name ^ " already declared"))
    1.93    end;
    1.94  
    1.95  fun add_tycodegen name f thy =
    1.96 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.97 +  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
    1.98      CodegenData.get thy
    1.99    in (case AList.lookup (op =) tycodegens name of
   1.100        NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
   1.101          codegens = codegens, consts = consts, types = types,
   1.102 -        attrs = attrs, preprocs = preprocs, modules = modules,
   1.103 +        preprocs = preprocs, modules = modules,
   1.104          test_params = test_params} thy
   1.105      | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   1.106    end;
   1.107 @@ -302,11 +297,11 @@
   1.108  (**** preprocessors ****)
   1.109  
   1.110  fun add_preprocessor p thy =
   1.111 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   1.112 +  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.113      CodegenData.get thy
   1.114    in CodegenData.put {tycodegens = tycodegens,
   1.115      codegens = codegens, consts = consts, types = types,
   1.116 -    attrs = attrs, preprocs = (stamp (), p) :: preprocs,
   1.117 +    preprocs = (stamp (), p) :: preprocs,
   1.118      modules = modules, test_params = test_params} thy
   1.119    end;
   1.120  
   1.121 @@ -341,53 +336,20 @@
   1.122        end)
   1.123    in add_preprocessor prep end;
   1.124  
   1.125 -
   1.126 -(**** code attribute ****)
   1.127 -
   1.128 -fun add_attribute name att thy =
   1.129 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   1.130 -    CodegenData.get thy
   1.131 -  in (case AList.lookup (op =) attrs name of
   1.132 -      NONE => CodegenData.put {tycodegens = tycodegens,
   1.133 -        codegens = codegens, consts = consts, types = types,
   1.134 -        attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
   1.135 -        preprocs = preprocs, modules = modules,
   1.136 -        test_params = test_params} thy
   1.137 -    | SOME _ => error ("Code attribute " ^ name ^ " already declared"))
   1.138 -  end;
   1.139 -
   1.140 -fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
   1.141 -
   1.142 -val code_attr =
   1.143 -  Attrib.syntax (Scan.peek (fn context => List.foldr op || Scan.fail (map mk_parser
   1.144 -    (#attrs (CodegenData.get (Context.theory_of context))))));
   1.145 -
   1.146  val _ = Context.add_setup
   1.147 -  (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
   1.148 -
   1.149 -local
   1.150 -  fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   1.151 -  fun add_simple_attribute (name, f) =
   1.152 -    add_attribute name (Scan.succeed (mk_attribute f));
   1.153 -  fun add_del_attribute (name, (add, del)) =
   1.154 -    add_attribute name (Args.del |-- Scan.succeed (mk_attribute del)
   1.155 -      || Scan.succeed (mk_attribute add))
   1.156 -in
   1.157 -  val _ = Context.add_setup (add_simple_attribute ("unfold",
   1.158 -    fn thm => add_unfold thm #> CodeData.add_inline thm));
   1.159 -  val _ = map (Context.add_setup o add_del_attribute) [
   1.160 -    ("func", (CodeData.add_func true, CodeData.del_func)),
   1.161 -    ("inline", (CodeData.add_inline, CodeData.del_inline)),
   1.162 -    ("post", (CodeData.add_post, CodeData.del_post))
   1.163 -  ];
   1.164 -end; (*local*)
   1.165 +  (let
   1.166 +    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   1.167 +  in
   1.168 +    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
   1.169 +      (fn thm => add_unfold thm #> Code.add_inline thm)))
   1.170 +  end);
   1.171  
   1.172  
   1.173  (**** associate constants with target language code ****)
   1.174  
   1.175  fun gen_assoc_const prep_const (raw_const, syn) thy =
   1.176    let
   1.177 -    val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   1.178 +    val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.179        CodegenData.get thy;
   1.180      val (cname, T) = prep_const thy raw_const;
   1.181    in
   1.182 @@ -397,20 +359,20 @@
   1.183        NONE => CodegenData.put {codegens = codegens,
   1.184          tycodegens = tycodegens,
   1.185          consts = ((cname, T), syn) :: consts,
   1.186 -        types = types, attrs = attrs, preprocs = preprocs,
   1.187 +        types = types, preprocs = preprocs,
   1.188          modules = modules, test_params = test_params} thy
   1.189      | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
   1.190    end;
   1.191  
   1.192  val assoc_const_i = gen_assoc_const (K I);
   1.193 -val assoc_const = gen_assoc_const CodegenConsts.read_bare_const;
   1.194 +val assoc_const = gen_assoc_const CodeUnit.read_bare_const;
   1.195  
   1.196  
   1.197  (**** associate types with target language types ****)
   1.198  
   1.199  fun assoc_type (s, syn) thy =
   1.200    let
   1.201 -    val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   1.202 +    val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.203        CodegenData.get thy;
   1.204      val tc = Sign.intern_type thy s;
   1.205    in
   1.206 @@ -421,7 +383,7 @@
   1.207          else (case AList.lookup (op =) types tc of
   1.208            NONE => CodegenData.put {codegens = codegens,
   1.209              tycodegens = tycodegens, consts = consts,
   1.210 -            types = (tc, syn) :: types, attrs = attrs,
   1.211 +            types = (tc, syn) :: types,
   1.212              preprocs = preprocs, modules = modules, test_params = test_params} thy
   1.213          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   1.214      | _ => error ("Not a type constructor: " ^ s)