1.1 --- a/src/Pure/Tools/codegen_package.ML Tue Jan 17 10:26:50 2006 +0100
1.2 +++ b/src/Pure/Tools/codegen_package.ML Tue Jan 17 16:36:57 2006 +0100
1.3 @@ -12,10 +12,15 @@
1.4 signature CODEGEN_PACKAGE =
1.5 sig
1.6 type auxtab;
1.7 - type appgen;
1.8 + type eqextr = theory -> auxtab
1.9 + -> (string * typ) -> (thm list * typ) option;
1.10 type defgen;
1.11 + type appgen = theory -> auxtab
1.12 + -> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
1.13 +
1.14 val add_appconst: string * ((int * int) * appgen) -> theory -> theory;
1.15 val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory;
1.16 + val add_eqextr: string * eqextr -> theory -> theory;
1.17 val add_defgen: string * defgen -> theory -> theory;
1.18 val add_prim_class: xstring -> string list -> (string * string)
1.19 -> theory -> theory;
1.20 @@ -25,49 +30,31 @@
1.21 -> theory -> theory;
1.22 val add_prim_i: string -> string list -> (string * Pretty.T)
1.23 -> theory -> theory;
1.24 - val add_syntax_tyco: xstring -> (string * (string * CodegenSerializer.fixity))
1.25 - -> theory -> theory;
1.26 - val add_syntax_tyco_i: string -> (string * (CodegenThingol.itype Codegen.mixfix list * CodegenSerializer.fixity))
1.27 - -> theory -> theory;
1.28 - val add_syntax_const: (xstring * string option) -> (string * (string * CodegenSerializer.fixity))
1.29 - -> theory -> theory;
1.30 - val add_syntax_const_i: string -> (string * (CodegenThingol.iexpr Codegen.mixfix list * CodegenSerializer.fixity))
1.31 - -> theory -> theory;
1.32 - val add_lookup_tyco: string * string -> theory -> theory;
1.33 - val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory;
1.34 val add_alias: string * string -> theory -> theory;
1.35 val set_is_datatype: (theory -> string -> bool) -> theory -> theory;
1.36 val set_get_all_datatype_cons : (theory -> (string * string) list)
1.37 -> theory -> theory;
1.38 + val set_int_tyco: string -> theory -> theory;
1.39
1.40 val exprgen_type: theory -> auxtab
1.41 -> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact;
1.42 val exprgen_term: theory -> auxtab
1.43 -> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
1.44 - val ensure_def_tyco: theory -> auxtab
1.45 - -> string -> CodegenThingol.transact -> string * CodegenThingol.transact;
1.46 - val ensure_def_const: theory -> auxtab
1.47 - -> string * typ -> CodegenThingol.transact -> string * CodegenThingol.transact;
1.48 + val appgen_default: appgen;
1.49
1.50 val appgen_let: (int -> term -> term list * term)
1.51 -> appgen;
1.52 val appgen_split: (int -> term -> term list * term)
1.53 -> appgen;
1.54 - val appgen_number_of: (term -> IntInf.int) -> (term -> term)
1.55 + val appgen_number_of: (term -> term) -> (term -> IntInf.int) -> string -> string
1.56 -> appgen;
1.57 - val appgen_datatype_case: (string * int) list
1.58 - -> appgen;
1.59 - val add_cg_case_const: (theory -> string -> (string * int) list option) -> xstring
1.60 + val add_case_const: (theory -> string -> (string * int) list option) -> xstring
1.61 -> theory -> theory;
1.62 - val add_cg_case_const_i: (theory -> string -> (string * int) list option) -> string
1.63 + val add_case_const_i: (theory -> string -> (string * int) list option) -> string
1.64 -> theory -> theory;
1.65 val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option)
1.66 -> (theory -> string * string -> typ list option)
1.67 -> defgen;
1.68 - val defgen_datacons: (theory -> string * string -> typ list option)
1.69 - -> defgen;
1.70 - val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ)
1.71 - -> defgen;
1.72
1.73 val print_codegen_generated: theory -> unit;
1.74 val rename_inconsistent: theory -> theory;
1.75 @@ -105,16 +92,13 @@
1.76
1.77 val is_number = is_some o Int.fromString;
1.78
1.79 -fun newline_correct s =
1.80 - s
1.81 - |> space_explode "\n"
1.82 - |> map (implode o (fn [] => []
1.83 - | (" "::xs) => xs
1.84 - | xs => xs) o explode)
1.85 - |> space_implode "\n";
1.86 +fun merge_opt _ (x1, NONE) = x1
1.87 + | merge_opt _ (NONE, x2) = x2
1.88 + | merge_opt eq (SOME x1, SOME x2) =
1.89 + if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
1.90
1.91
1.92 -(* shallo name spaces *)
1.93 +(* shallow name spaces *)
1.94
1.95 val nsp_class = "class";
1.96 val nsp_tyco = "tyco";
1.97 @@ -123,11 +107,9 @@
1.98 val nsp_dtcon = "dtcon";
1.99 val nsp_mem = "mem";
1.100 val nsp_inst = "inst";
1.101 -val nsp_eq_inst = "eq_inst";
1.102 -val nsp_eq_pred = "eq";
1.103
1.104
1.105 -(* code generator data types *)
1.106 +(* code generator basics *)
1.107
1.108 structure InstNameMangler = NameManglerFun (
1.109 type ctxt = theory;
1.110 @@ -171,9 +153,7 @@
1.111 type ctxt = theory;
1.112 type src = string * string;
1.113 val ord = prod_ord string_ord string_ord;
1.114 - fun mk thy (("0", "nat"), _) =
1.115 - "Nat.Zero"
1.116 - | mk thy ((co, dtco), i) =
1.117 + fun mk thy ((co, dtco), i) =
1.118 let
1.119 fun basename 0 = NameSpace.base co
1.120 | basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co
1.121 @@ -194,69 +174,55 @@
1.122 fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
1.123 );
1.124
1.125 -type auxtab = ((typ * (term list * term)) Symtab.table * string Symtab.table)
1.126 +type auxtab = ((typ * thm) list Symtab.table * string Symtab.table)
1.127 * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T);
1.128 +type eqextr = theory -> auxtab
1.129 + -> (string * typ) -> (thm list * typ) option;
1.130 +type defgen = theory -> auxtab -> gen_defgen;
1.131 +type appgen = theory -> auxtab -> (string * typ) * term list -> transact -> iexpr * transact;
1.132
1.133 -type appgen = theory -> auxtab -> ((string * typ) * term list, iexpr) gen_exprgen;
1.134 -type defgen = theory -> auxtab -> gen_defgen;
1.135 -
1.136 -
1.137 -(* serializer *)
1.138 -
1.139 -val serializer_ml =
1.140 - let
1.141 - val name_root = "Generated";
1.142 - val nsp_conn = [
1.143 - [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_eq_inst, nsp_eq_pred]
1.144 - ];
1.145 - in CodegenSerializer.ml_from_thingol nsp_conn nsp_class name_root end;
1.146 -
1.147 -val serializer_hs =
1.148 - let
1.149 - val name_root = "Generated";
1.150 - val nsp_conn = [
1.151 - [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem, nsp_eq_pred], [nsp_dtcon], [nsp_inst, nsp_eq_inst]
1.152 - ];
1.153 - in CodegenSerializer.haskell_from_thingol nsp_conn nsp_dtcon name_root end;
1.154 +val serializers = ref (
1.155 + Symtab.empty
1.156 + |> Symtab.update (
1.157 + #ml CodegenSerializer.serializers
1.158 + |> apsnd (fn seri => seri
1.159 + (nsp_dtcon, nsp_class, "")
1.160 + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
1.161 + )
1.162 + )
1.163 + |> Symtab.update (
1.164 + #haskell CodegenSerializer.serializers
1.165 + |> apsnd (fn seri => seri
1.166 + nsp_dtcon
1.167 + [[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]]
1.168 + )
1.169 + )
1.170 +);
1.171
1.172
1.173 (* theory data for code generator *)
1.174
1.175 type gens = {
1.176 appconst: ((int * int) * (appgen * stamp)) Symtab.table,
1.177 + eqextrs: (string * (eqextr * stamp)) list,
1.178 defgens: (string * (defgen * stamp)) list
1.179 };
1.180
1.181 -fun map_gens f { appconst, defgens } =
1.182 +fun map_gens f { appconst, eqextrs, defgens } =
1.183 let
1.184 - val (appconst, defgens) =
1.185 - f (appconst, defgens)
1.186 - in { appconst = appconst, defgens = defgens } : gens end;
1.187 + val (appconst, eqextrs, defgens) =
1.188 + f (appconst, eqextrs, defgens)
1.189 + in { appconst = appconst, eqextrs = eqextrs, defgens = defgens } : gens end;
1.190
1.191 fun merge_gens
1.192 - ({ appconst = appconst1 , defgens = defgens1 },
1.193 - { appconst = appconst2 , defgens = defgens2 }) =
1.194 + ({ appconst = appconst1 , eqextrs = eqextrs1, defgens = defgens1 },
1.195 + { appconst = appconst2 , eqextrs = eqextrs2, defgens = defgens2 }) =
1.196 { appconst = Symtab.merge
1.197 (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2)
1.198 (appconst1, appconst2),
1.199 - defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens;
1.200 -
1.201 -type lookups = {
1.202 - lookups_tyco: string Symtab.table,
1.203 - lookups_const: (typ * iexpr) list Symtab.table
1.204 -}
1.205 -
1.206 -fun map_lookups f { lookups_tyco, lookups_const } =
1.207 - let
1.208 - val (lookups_tyco, lookups_const) =
1.209 - f (lookups_tyco, lookups_const)
1.210 - in { lookups_tyco = lookups_tyco, lookups_const = lookups_const } : lookups end;
1.211 -
1.212 -fun merge_lookups
1.213 - ({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 },
1.214 - { lookups_tyco = lookups_tyco2, lookups_const = lookups_const2 }) =
1.215 - { lookups_tyco = Symtab.merge (op =) (lookups_tyco1, lookups_tyco2),
1.216 - lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) } : lookups;
1.217 + eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2),
1.218 + defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2)
1.219 + } : gens;
1.220
1.221 type logic_data = {
1.222 is_datatype: ((theory -> string -> bool) * stamp) option,
1.223 @@ -268,16 +234,15 @@
1.224 let
1.225 val ((is_datatype, get_all_datatype_cons), alias) =
1.226 f ((is_datatype, get_all_datatype_cons), alias)
1.227 - in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, alias = alias } : logic_data end;
1.228 + in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons,
1.229 + alias = alias } : logic_data end;
1.230
1.231 fun merge_logic_data
1.232 - ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, alias = alias1 },
1.233 - { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, alias = alias2 }) =
1.234 + ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1,
1.235 + alias = alias1 },
1.236 + { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2,
1.237 + alias = alias2 }) =
1.238 let
1.239 - fun merge_opt _ (x1, NONE) = x1
1.240 - | merge_opt _ (NONE, x2) = x2
1.241 - | merge_opt eq (SOME x1, SOME x2) =
1.242 - if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
1.243 in
1.244 { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
1.245 get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2),
1.246 @@ -285,28 +250,23 @@
1.247 Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
1.248 end;
1.249
1.250 -type serialize_data = {
1.251 - serializer: CodegenSerializer.serializer,
1.252 +type target_data = {
1.253 syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table,
1.254 syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table
1.255 };
1.256
1.257 -fun map_serialize_data f { serializer, syntax_tyco, syntax_const } =
1.258 +fun map_target_data f { syntax_tyco, syntax_const } =
1.259 let
1.260 val (syntax_tyco, syntax_const) =
1.261 f (syntax_tyco, syntax_const)
1.262 - in { serializer = serializer,
1.263 - syntax_tyco = syntax_tyco, syntax_const = syntax_const } : serialize_data
1.264 + in { syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data
1.265 end;
1.266
1.267 -fun merge_serialize_data
1.268 - ({ serializer = serializer,
1.269 - syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
1.270 - {serializer = _,
1.271 - syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
1.272 - { serializer = serializer,
1.273 - syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
1.274 - syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : serialize_data;
1.275 +fun merge_target_data
1.276 + ({ syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
1.277 + { syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
1.278 + { syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
1.279 + syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data;
1.280
1.281 structure CodegenData = TheoryDataFun
1.282 (struct
1.283 @@ -314,50 +274,44 @@
1.284 type T = {
1.285 modl: module,
1.286 gens: gens,
1.287 - lookups: lookups,
1.288 logic_data: logic_data,
1.289 - serialize_data: serialize_data Symtab.table
1.290 + target_data: target_data Symtab.table
1.291 };
1.292 val empty = {
1.293 modl = empty_module,
1.294 - gens = { appconst = Symtab.empty, defgens = [] } : gens,
1.295 - lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups,
1.296 + gens = { appconst = Symtab.empty, eqextrs = [], defgens = [] } : gens,
1.297 logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE,
1.298 alias = (Symtab.empty, Symtab.empty) } : logic_data,
1.299 - serialize_data =
1.300 + target_data =
1.301 Symtab.empty
1.302 - |> Symtab.update ("ml",
1.303 - { serializer = serializer_ml : CodegenSerializer.serializer,
1.304 - syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
1.305 - |> Symtab.update ("haskell",
1.306 - { serializer = serializer_hs : CodegenSerializer.serializer,
1.307 - syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
1.308 + |> Symtab.fold (fn (target, _) =>
1.309 + Symtab.update (target, { syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
1.310 + ) (! serializers)
1.311 } : T;
1.312 val copy = I;
1.313 val extend = I;
1.314 fun merge _ (
1.315 - { modl = modl1, gens = gens1, lookups = lookups1,
1.316 - serialize_data = serialize_data1, logic_data = logic_data1 },
1.317 - { modl = modl2, gens = gens2, lookups = lookups2,
1.318 - serialize_data = serialize_data2, logic_data = logic_data2 }
1.319 + { modl = modl1, gens = gens1,
1.320 + target_data = target_data1, logic_data = logic_data1 },
1.321 + { modl = modl2, gens = gens2,
1.322 + target_data = target_data2, logic_data = logic_data2 }
1.323 ) = {
1.324 modl = merge_module (modl1, modl2),
1.325 gens = merge_gens (gens1, gens2),
1.326 - lookups = merge_lookups (lookups1, lookups2),
1.327 logic_data = merge_logic_data (logic_data1, logic_data2),
1.328 - serialize_data = Symtab.join (K (merge_serialize_data #> SOME))
1.329 - (serialize_data1, serialize_data2)
1.330 + target_data = Symtab.join (K (merge_target_data #> SOME))
1.331 + (target_data1, target_data2)
1.332 };
1.333 fun print thy _ = writeln "sorry, this stuff is too complicated...";
1.334 end);
1.335
1.336 fun map_codegen_data f thy =
1.337 case CodegenData.get thy
1.338 - of { modl, gens, lookups, serialize_data, logic_data } =>
1.339 - let val (modl, gens, lookups, serialize_data, logic_data) =
1.340 - f (modl, gens, lookups, serialize_data, logic_data)
1.341 - in CodegenData.put { modl = modl, gens = gens, lookups = lookups,
1.342 - serialize_data = serialize_data, logic_data = logic_data } thy end;
1.343 + of { modl, gens, target_data, logic_data } =>
1.344 + let val (modl, gens, target_data, logic_data) =
1.345 + f (modl, gens, target_data, logic_data)
1.346 + in CodegenData.put { modl = modl, gens = gens,
1.347 + target_data = target_data, logic_data = logic_data } thy end;
1.348
1.349 fun print_codegen_generated thy =
1.350 let
1.351 @@ -370,13 +324,13 @@
1.352 let
1.353 val c = prep_const thy raw_c;
1.354 in map_codegen_data
1.355 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.356 + (fn (modl, gens, target_data, logic_data) =>
1.357 (modl,
1.358 gens |> map_gens
1.359 - (fn (appconst, defgens) =>
1.360 + (fn (appconst, eqextrs, defgens) =>
1.361 (appconst
1.362 |> Symtab.update (c, (bounds, (ag, stamp ()))),
1.363 - defgens)), lookups, serialize_data, logic_data)) thy
1.364 + eqextrs, defgens)), target_data, logic_data)) thy
1.365 end;
1.366
1.367 val add_appconst = gen_add_appconst Sign.intern_const;
1.368 @@ -384,62 +338,36 @@
1.369
1.370 fun add_defgen (name, dg) =
1.371 map_codegen_data
1.372 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.373 + (fn (modl, gens, target_data, logic_data) =>
1.374 (modl,
1.375 gens |> map_gens
1.376 - (fn (appconst, defgens) =>
1.377 - (appconst, defgens
1.378 + (fn (appconst, eqextrs, defgens) =>
1.379 + (appconst, eqextrs, defgens
1.380 |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))),
1.381 - lookups, serialize_data, logic_data));
1.382 + target_data, logic_data));
1.383
1.384 fun get_defgens thy tabs =
1.385 (map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy;
1.386
1.387 -fun add_lookup_tyco (src, dst) =
1.388 +fun add_eqextr (name, eqx) =
1.389 map_codegen_data
1.390 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.391 - (modl, gens,
1.392 - lookups |> map_lookups
1.393 - (fn (lookups_tyco, lookups_const) =>
1.394 - (lookups_tyco |> Symtab.update_new (src, dst),
1.395 - lookups_const)),
1.396 - serialize_data, logic_data));
1.397 + (fn (modl, gens, target_data, logic_data) =>
1.398 + (modl,
1.399 + gens |> map_gens
1.400 + (fn (appconst, eqextrs, defgens) =>
1.401 + (appconst, eqextrs
1.402 + |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())),
1.403 + defgens)),
1.404 + target_data, logic_data));
1.405
1.406 -val lookup_tyco = Symtab.lookup o #lookups_tyco o #lookups o CodegenData.get;
1.407 -
1.408 -fun add_lookup_const ((src, ty), dst) =
1.409 - map_codegen_data
1.410 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.411 - (modl, gens,
1.412 - lookups |> map_lookups
1.413 - (fn (lookups_tyco, lookups_const) =>
1.414 - (lookups_tyco,
1.415 - lookups_const |> Symtab.update_multi (src, (ty, dst)))),
1.416 - serialize_data, logic_data));
1.417 -
1.418 -fun lookup_const thy (f, ty) =
1.419 - (Symtab.lookup_multi o #lookups_const o #lookups o CodegenData.get) thy f
1.420 - |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty);
1.421 -
1.422 -fun set_is_datatype f =
1.423 - map_codegen_data
1.424 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.425 - (modl, gens, lookups, serialize_data,
1.426 - logic_data
1.427 - |> map_logic_data ((apfst o apfst) (K (SOME (f, stamp ()))))));
1.428 +fun get_eqextrs thy tabs =
1.429 + (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy;
1.430
1.431 fun is_datatype thy =
1.432 case (#is_datatype o #logic_data o CodegenData.get) thy
1.433 of NONE => K false
1.434 | SOME (f, _) => f thy;
1.435
1.436 -fun set_get_all_datatype_cons f =
1.437 - map_codegen_data
1.438 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.439 - (modl, gens, lookups, serialize_data,
1.440 - logic_data
1.441 - |> map_logic_data ((apfst o apsnd) (K (SOME (f, stamp ()))))));
1.442 -
1.443 fun get_all_datatype_cons thy =
1.444 case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
1.445 of NONE => []
1.446 @@ -447,8 +375,8 @@
1.447
1.448 fun add_alias (src, dst) =
1.449 map_codegen_data
1.450 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.451 - (modl, gens, lookups, serialize_data,
1.452 + (fn (modl, gens, target_data, logic_data) =>
1.453 + (modl, gens, target_data,
1.454 logic_data |> map_logic_data
1.455 (apsnd (fn (tab, tab_rev) =>
1.456 (tab |> Symtab.update (src, dst),
1.457 @@ -457,16 +385,6 @@
1.458
1.459 (* name handling *)
1.460
1.461 -val nsp_class = "class";
1.462 -val nsp_tyco = "tyco";
1.463 -val nsp_const = "const";
1.464 -val nsp_overl = "overl";
1.465 -val nsp_dtcon = "dtcon";
1.466 -val nsp_mem = "mem";
1.467 -val nsp_inst = "inst";
1.468 -val nsp_eq_inst = "eq_inst";
1.469 -val nsp_eq_pred = "eq";
1.470 -
1.471 val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get;
1.472 val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get;
1.473
1.474 @@ -477,6 +395,7 @@
1.475 |> apsnd (single #> cons shallow)
1.476 |> (op @)
1.477 |> NameSpace.pack;
1.478 +
1.479 fun dest_nsp nsp idf =
1.480 let
1.481 val idf' = NameSpace.unpack idf;
1.482 @@ -489,17 +408,43 @@
1.483 end;
1.484
1.485 fun idf_of_name thy shallow name =
1.486 - if is_number name
1.487 - then name
1.488 - else
1.489 - name
1.490 - |> alias_get thy
1.491 - |> add_nsp shallow;
1.492 + name
1.493 + |> alias_get thy
1.494 + |> add_nsp shallow;
1.495 +
1.496 fun name_of_idf thy shallow idf =
1.497 idf
1.498 |> dest_nsp shallow
1.499 |> Option.map (alias_rev thy);
1.500
1.501 +fun set_is_datatype f =
1.502 + map_codegen_data
1.503 + (fn (modl, gens, target_data, logic_data) =>
1.504 + (modl, gens, target_data,
1.505 + logic_data
1.506 + |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons)
1.507 + => (SOME (f, stamp ()), get_all_datatype_cons)))));
1.508 +
1.509 +fun set_get_all_datatype_cons f =
1.510 + map_codegen_data
1.511 + (fn (modl, gens, target_data, logic_data) =>
1.512 + (modl, gens, target_data,
1.513 + logic_data
1.514 + |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons)
1.515 + => (is_datatype, SOME (f, stamp ())))))));
1.516 +
1.517 +fun set_int_tyco tyco thy =
1.518 + (serializers := (
1.519 + ! serializers
1.520 + |> Symtab.update (
1.521 + #ml CodegenSerializer.serializers
1.522 + |> apsnd (fn seri => seri
1.523 + (nsp_dtcon, nsp_class, idf_of_name thy nsp_tyco tyco)
1.524 + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
1.525 + )
1.526 + )
1.527 + ); thy);
1.528 +
1.529
1.530 (* code generator instantiation *)
1.531
1.532 @@ -515,7 +460,7 @@
1.533
1.534 fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
1.535 let
1.536 - val thyname = (the o AList.lookup (op =) (ClassPackage.the_tycos thy cls)) tyco;
1.537 + val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco;
1.538 val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)));
1.539 in
1.540 trns
1.541 @@ -527,15 +472,11 @@
1.542 fun ensure_def_tyco thy tabs tyco trns =
1.543 let
1.544 val tyco' = idf_of_name thy nsp_tyco tyco;
1.545 - in case lookup_tyco thy tyco
1.546 - of NONE =>
1.547 - trns
1.548 - |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
1.549 - |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco'
1.550 - |> pair tyco'
1.551 - | SOME tyco =>
1.552 - trns
1.553 - |> pair tyco
1.554 + in
1.555 + trns
1.556 + |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
1.557 + |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco'
1.558 + |> pair tyco'
1.559 end;
1.560
1.561 fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) =
1.562 @@ -553,10 +494,10 @@
1.563 of Type (tyco, _) =>
1.564 try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco)
1.565 | _ => NONE;
1.566 - in case get_overloaded (c, ty)
1.567 + in case get_datatypecons (c, ty)
1.568 + of SOME c' => idf_of_name thy nsp_dtcon c'
1.569 + | NONE => case get_overloaded (c, ty)
1.570 of SOME idf => idf
1.571 - | NONE => case get_datatypecons (c, ty)
1.572 - of SOME c' => idf_of_name thy nsp_dtcon c'
1.573 | NONE => case Symtab.lookup clsmemtab c
1.574 of SOME _ => idf_of_name thy nsp_mem c
1.575 | NONE => idf_of_name thy nsp_const c
1.576 @@ -564,7 +505,7 @@
1.577
1.578 fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
1.579 case name_of_idf thy nsp_const idf
1.580 - of SOME c => SOME (c, Sign.the_const_constraint thy c)
1.581 + of SOME c => SOME (c, Sign.the_const_type thy c)
1.582 | NONE => (
1.583 case dest_nsp nsp_overl idf
1.584 of SOME _ =>
1.585 @@ -579,18 +520,14 @@
1.586 fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns =
1.587 let
1.588 val c' = idf_of_const thy tabs (c, ty);
1.589 - in case lookup_const thy (c, ty)
1.590 - of NONE =>
1.591 - trns
1.592 - |> debug 4 (fn _ => "generating constant " ^ quote c)
1.593 - |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c'
1.594 - |> pair c'
1.595 - | SOME (IConst (c, ty)) =>
1.596 - trns
1.597 - |> pair c
1.598 + in
1.599 + trns
1.600 + |> debug 4 (fn _ => "generating constant " ^ quote c)
1.601 + |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c'
1.602 + |> pair c'
1.603 end;
1.604
1.605 -fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns =
1.606 +(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns =
1.607 let
1.608 val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco;
1.609 val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco;
1.610 @@ -598,30 +535,30 @@
1.611 val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity;
1.612 fun mk_eq_pred _ trns =
1.613 trns
1.614 - |> succeed (eqpred, [])
1.615 + |> succeed (eqpred)
1.616 fun mk_eq_inst _ trns =
1.617 trns
1.618 |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred
1.619 - |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])), []);
1.620 + |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])));
1.621 in
1.622 trns
1.623 |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst
1.624 - end;
1.625 + end; *)
1.626
1.627
1.628 (* expression generators *)
1.629
1.630 -fun exprgen_sort thy tabs sort trns =
1.631 +fun exprgen_tyvar_sort thy tabs (v, sort) trns =
1.632 trns
1.633 |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort)
1.634 - |-> (fn sort => pair sort);
1.635 + |-> (fn sort => pair (unprefix "'" v, sort));
1.636
1.637 fun exprgen_type thy tabs (TVar _) trns =
1.638 error "TVar encountered during code generation"
1.639 - | exprgen_type thy tabs (TFree (v, sort)) trns =
1.640 + | exprgen_type thy tabs (TFree v_s) trns =
1.641 trns
1.642 - |> exprgen_sort thy tabs sort
1.643 - |-> (fn sort => pair (IVarT (v |> unprefix "'", sort)))
1.644 + |> exprgen_tyvar_sort thy tabs v_s
1.645 + |-> (fn v_s => pair (IVarT v_s))
1.646 | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
1.647 trns
1.648 |> exprgen_type thy tabs t1
1.649 @@ -644,19 +581,19 @@
1.650 |> fold_map (ensure_def_class thy tabs) clss
1.651 |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
1.652
1.653 -fun mk_itapp e [] = e
1.654 - | mk_itapp e lookup = IInst (e, lookup);
1.655 -
1.656 -fun appgen thy tabs ((f, ty), ts) trns =
1.657 +fun appgen_default thy tabs ((c, ty), ts) trns =
1.658 + trns
1.659 + |> ensure_def_const thy tabs (c, ty)
1.660 + ||>> (fold_map o fold_map) (mk_lookup thy tabs)
1.661 + (ClassPackage.extract_sortlookup thy (c, ty))
1.662 + ||>> exprgen_type thy tabs ty
1.663 + ||>> fold_map (exprgen_term thy tabs) ts
1.664 + |-> (fn (((c, ls), ty), es) =>
1.665 + pair (Library.foldl IInst ((IConst (c, ty)), ls) `$$ es))
1.666 +and appgen thy tabs ((f, ty), ts) trns =
1.667 case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
1.668 of SOME ((imin, imax), (ag, _)) =>
1.669 - let
1.670 - fun invoke ts trns =
1.671 - trns
1.672 - |> gen_invoke [("const application", ag thy tabs)] ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty
1.673 - ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts)))
1.674 - ((f, ty), ts)
1.675 - in if length ts < imin then
1.676 + if length ts < imin then
1.677 let
1.678 val d = imin - length ts;
1.679 val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d;
1.680 @@ -665,29 +602,22 @@
1.681 trns
1.682 |> debug 10 (fn _ => "eta-expanding")
1.683 |> fold_map (exprgen_type thy tabs) tys
1.684 - ||>> invoke (ts @ map2 (curry Free) vs tys)
1.685 + ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
1.686 |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e))
1.687 end
1.688 else if length ts > imax then
1.689 trns
1.690 |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")")
1.691 - |> invoke (Library.take (imax, ts))
1.692 + |> ag thy tabs ((f, ty), Library.take (imax, ts))
1.693 ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
1.694 |-> (fn es => pair (mk_apps es))
1.695 else
1.696 trns
1.697 |> debug 10 (fn _ => "keeping arguments")
1.698 - |> invoke ts
1.699 - end
1.700 + |> ag thy tabs ((f, ty), ts)
1.701 | NONE =>
1.702 trns
1.703 - |> ensure_def_const thy tabs (f, ty)
1.704 - ||>> (fold_map o fold_map) (mk_lookup thy tabs)
1.705 - (ClassPackage.extract_sortlookup thy (Sign.the_const_constraint thy f, ty))
1.706 - ||>> exprgen_type thy tabs ty
1.707 - ||>> fold_map (exprgen_term thy tabs) ts
1.708 - |-> (fn (((f, lookup), ty), es) =>
1.709 - pair (mk_itapp (IConst (f, ty)) lookup `$$ es))
1.710 + |> appgen_default thy tabs ((f, ty), ts)
1.711 and exprgen_term thy tabs (Const (f, ty)) trns =
1.712 trns
1.713 |> appgen thy tabs ((f, ty), [])
1.714 @@ -723,103 +653,106 @@
1.715
1.716 (* application generators *)
1.717
1.718 -fun appgen_neg thy tabs (("neg", Type ("fun", [ty, _])), ts) trns =
1.719 - trns
1.720 - |> exprgen_term thy tabs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty))
1.721 - |-> succeed;
1.722 -
1.723 -fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns =
1.724 +(* fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns =
1.725 trns
1.726 |> invoke_eq (exprgen_type thy tabs) (ensure_def_eq thy tabs) ty
1.727 |-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty)
1.728 | true => fn trns => trns
1.729 |> exprgen_term thy tabs t1
1.730 ||>> exprgen_term thy tabs t2
1.731 - |-> (fn (e1, e2) => succeed (Fun_eq `$ e1 `$ e2)));
1.732 + |-> (fn (e1, e2) => pair (Fun_eq `$ e1 `$ e2))); *)
1.733 +
1.734 +
1.735 +(* function extractors *)
1.736 +
1.737 +fun mk_fun thy tabs (c, ty) trns =
1.738 + case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs)
1.739 + of SOME (eq_thms, ty) =>
1.740 + let
1.741 + val sortctxt = ClassPackage.extract_sortctxt thy ty;
1.742 + fun dest_eqthm eq_thm =
1.743 + eq_thm
1.744 + |> prop_of
1.745 + |> Logic.dest_equals
1.746 + |> apfst (strip_comb #> snd);
1.747 + fun mk_eq (args, rhs) trns =
1.748 + trns
1.749 + |> fold_map (exprgen_term thy tabs o devarify_term) args
1.750 + ||>> (exprgen_term thy tabs o devarify_term) rhs
1.751 + |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
1.752 + in
1.753 + trns
1.754 + |> fold_map (mk_eq o dest_eqthm) eq_thms
1.755 + ||>> exprgen_type thy tabs (devarify_type ty)
1.756 + ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
1.757 + |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty)))
1.758 + end
1.759 + | NONE => (NONE, trns);
1.760 +
1.761 +fun eqextr_defs thy ((deftab, _), _) (c, ty) =
1.762 + let
1.763 + fun eq_typ (ty1, ty2) =
1.764 + Sign.typ_instance thy (ty1, ty2)
1.765 + andalso Sign.typ_instance thy (ty2, ty1)
1.766 + in
1.767 + Option.mapPartial (get_first (fn (ty', thm) => if eq_typ (ty, ty')
1.768 + then SOME ([thm], ty')
1.769 + else NONE
1.770 + )) (Symtab.lookup deftab c)
1.771 + end;
1.772
1.773
1.774 (* definition generators *)
1.775
1.776 -fun mk_fun thy tabs eqs ty trns =
1.777 - let
1.778 - val sortctxt = ClassPackage.extract_sortctxt thy ty;
1.779 - fun mk_sortvar (v, sort) trns =
1.780 - trns
1.781 - |> exprgen_sort thy tabs sort
1.782 - |-> (fn sort => pair (unprefix "'" v, sort))
1.783 - fun mk_eq (args, rhs) trns =
1.784 - trns
1.785 - |> fold_map (exprgen_term thy tabs o devarify_term) args
1.786 - ||>> (exprgen_term thy tabs o devarify_term) rhs
1.787 - |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
1.788 - in
1.789 - trns
1.790 - |> fold_map mk_eq eqs
1.791 - ||>> exprgen_type thy tabs (devarify_type ty)
1.792 - ||>> fold_map mk_sortvar sortctxt
1.793 - |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty))))
1.794 - end;
1.795 -
1.796 -fun defgen_tyco_fallback thy tabs tyco trns =
1.797 - if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco)
1.798 - ((#serialize_data o CodegenData.get) thy) false
1.799 - then
1.800 - trns
1.801 - |> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco)
1.802 - |> succeed (Nop, [])
1.803 - else
1.804 - trns
1.805 - |> fail ("no code generation fallback for " ^ quote tyco)
1.806 -
1.807 -fun defgen_const_fallback thy tabs c trns =
1.808 - if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const c)
1.809 - ((#serialize_data o CodegenData.get) thy) false
1.810 - then
1.811 - trns
1.812 - |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote c)
1.813 - |> succeed (Nop, [])
1.814 - else
1.815 - trns
1.816 - |> fail ("no code generation fallback for " ^ quote c)
1.817 -
1.818 -fun defgen_defs thy (tabs as ((deftab, _), _)) c trns =
1.819 - case Symtab.lookup deftab c
1.820 - of SOME (ty, (args, rhs)) =>
1.821 - trns
1.822 - |> debug 5 (fn _ => "trying defgen def for " ^ quote c)
1.823 - |> mk_fun thy tabs [(args, rhs)] (devarify_type ty)
1.824 - |-> (fn def => succeed (def, []))
1.825 - | _ => trns |> fail ("no definition found for " ^ quote c);
1.826 -
1.827 -fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) (cls : string) trns =
1.828 +fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) cls trns =
1.829 case name_of_idf thy nsp_class cls
1.830 of SOME cls =>
1.831 let
1.832 - val memnames = ClassPackage.the_consts thy (cls : string);
1.833 - val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames;
1.834 - val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes;
1.835 - val memidfs = map (idf_of_name thy nsp_mem) memnames;
1.836 - fun mk_instname (tyco, thyname) = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)))
1.837 - val instnames = map mk_instname (ClassPackage.the_tycos thy cls);
1.838 + val cs = (snd o ClassPackage.the_consts_sign thy) cls;
1.839 + val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs;
1.840 + val idfs = map (idf_of_name thy nsp_mem o fst) cs;
1.841 in
1.842 trns
1.843 |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
1.844 - |> fold_map (ensure_def_class thy tabs) (ClassPackage.get_superclasses thy cls)
1.845 - ||>> fold_map (exprgen_type thy tabs) memtypes
1.846 - |-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []),
1.847 - memidfs @ instnames))
1.848 + |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
1.849 + ||>> fold_map (exprgen_type thy tabs o snd) cs
1.850 + ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
1.851 + |-> (fn ((supcls, memtypes), sortctxts) => succeed
1.852 + (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), [])))
1.853 end
1.854 | _ =>
1.855 trns
1.856 |> fail ("no class definition found for " ^ quote cls);
1.857
1.858 +fun defgen_funs thy tabs c trns =
1.859 + case recconst_of_idf thy tabs c
1.860 + of SOME (c, ty) =>
1.861 + trns
1.862 + |> mk_fun thy tabs (c, ty)
1.863 + |-> (fn (SOME funn) => succeed (Fun funn)
1.864 + | NONE => fail ("no defining equations found for " ^ quote c))
1.865 + | NONE =>
1.866 + trns
1.867 + |> fail ("not a constant: " ^ quote c);
1.868 +
1.869 +fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
1.870 + case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
1.871 + of SOME (co, dtco) =>
1.872 + trns
1.873 + |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co)
1.874 + |> ensure_def_tyco thy tabs dtco
1.875 + |-> (fn dtco => succeed Undef)
1.876 + | _ =>
1.877 + trns
1.878 + |> fail ("not a datatype constructor: " ^ quote co);
1.879 +
1.880 fun defgen_clsmem thy tabs m trns =
1.881 case name_of_idf thy nsp_mem m
1.882 of SOME m =>
1.883 trns
1.884 |> debug 5 (fn _ => "trying defgen class member for " ^ quote m)
1.885 |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
1.886 - |-> (fn cls => succeed (Classmember cls, []))
1.887 + |-> (fn cls => succeed Undef)
1.888 | _ =>
1.889 trns |> fail ("no class member found for " ^ quote m)
1.890
1.891 @@ -827,70 +760,49 @@
1.892 case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst)
1.893 of SOME (_, (cls, tyco)) =>
1.894 let
1.895 - val arity = ClassPackage.get_arities thy [cls] tyco;
1.896 - val ms = map (fn m => (m, Sign.the_const_constraint thy m)) (ClassPackage.the_consts thy cls);
1.897 - val instmem_idfs = ClassPackage.get_inst_consts_sign thy (tyco, cls);
1.898 - val supclss = ClassPackage.get_superclasses thy cls;
1.899 - fun add_vars arity clsmems (trns as (_, modl)) =
1.900 - case get_def modl (idf_of_name thy nsp_class cls)
1.901 - of Class (_, _, members, _) => ((Term.invent_names
1.902 - (tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns)
1.903 - val ad_hoc_arity = map (fn (v, sort) => map_index (fn (i, _) => (ClassPackage.Lookup ([], (v, i)))) sort);
1.904 - (*! THIS IS ACTUALLY VERY AD-HOC... !*)
1.905 + val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco);
1.906 + fun gen_membr (m, ty) trns =
1.907 + trns
1.908 + |> mk_fun thy tabs (m, ty)
1.909 + |-> (fn SOME funn => pair (m, funn)
1.910 + | NONE => error ("could not derive definition for member " ^ quote m));
1.911 in
1.912 - (trns
1.913 + trns
1.914 |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
1.915 - |> (fold_map o fold_map) (ensure_def_class thy tabs) arity
1.916 - ||>> fold_map (ensure_def_const thy tabs) ms
1.917 - |-> (fn (arity, ms) => add_vars arity ms)
1.918 - ||>> ensure_def_class thy tabs cls
1.919 + |> ensure_def_class thy tabs cls
1.920 ||>> ensure_def_tyco thy tabs tyco
1.921 - ||>> fold_map (fn supcls => ensure_def_inst thy tabs (supcls, tyco)) supclss
1.922 - ||>> fold_map (fn supcls => (fold_map o fold_map) (mk_lookup thy tabs)
1.923 - (ClassPackage.extract_sortlookup thy
1.924 - (Type (tyco, map_index (fn (i, _) => TVar (("'a", i), [])) (ClassPackage.get_arities thy [supcls] tyco)),
1.925 - Type (tyco, map_index (fn (i, sort) => TFree (string_of_int i, sort)) arity)))) supclss
1.926 - ||>> fold_map (ensure_def_const thy tabs) instmem_idfs)
1.927 - |-> (fn ((((((arity, ms), cls), tyco), supinsts), supinstlookup), instmem_idfs)
1.928 - : ((((((string * string list) list * string list) * string) * string)
1.929 - * string list) * ClassPackage.sortlookup list list list) * string list
1.930 - =>
1.931 - succeed (Classinst ((cls, (tyco, arity)), (supclss ~~ (supinsts ~~ supinstlookup), ms ~~ map (rpair (ad_hoc_arity arity)) instmem_idfs)), []))
1.932 + ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
1.933 + ||>> fold_map gen_membr memdefs
1.934 + |-> (fn (((cls, tyco), arity), memdefs) =>
1.935 + succeed (Classinst ((cls, (tyco, arity)), memdefs)))
1.936 end
1.937 | _ =>
1.938 trns |> fail ("no class instance found for " ^ quote inst);
1.939
1.940
1.941 -(* trns
1.942 - |> ensure_def_const thy tabs (f, ty)
1.943 -
1.944 - ||>> exprgen_type thy tabs ty
1.945 - ||>> fold_map (exprgen_term thy tabs) ts
1.946 - |-> (fn (((f, lookup), ty), es) =>
1.947 - succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))*)
1.948 -
1.949 -
1.950 (* parametrized generators, for instantiation in HOL *)
1.951
1.952 -fun appgen_let strip_abs thy tabs (c, [t2, t3]) trns =
1.953 +fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns =
1.954 let
1.955 - fun dest_let (l as Const ("Let", _) $ t $ u) =
1.956 - (case strip_abs 1 u
1.957 - of ([p], u') => apfst (cons (p, t)) (dest_let u')
1.958 - | _ => ([], l))
1.959 + fun dest_let (l as Const (c', _) $ t $ u) =
1.960 + if c = c' then
1.961 + case strip_abs 1 u
1.962 + of ([p], u') => apfst (cons (p, t)) (dest_let u')
1.963 + | _ => ([], l)
1.964 + else ([], t)
1.965 | dest_let t = ([], t);
1.966 fun mk_let (l, r) trns =
1.967 trns
1.968 |> exprgen_term thy tabs l
1.969 ||>> exprgen_term thy tabs r
1.970 |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
1.971 - val (lets, body) = dest_let (Const c $ t2 $ t3)
1.972 + val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3)
1.973 in
1.974 trns
1.975 |> fold_map mk_let lets
1.976 ||>> exprgen_term thy tabs body
1.977 |-> (fn (lets, body) =>
1.978 - succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
1.979 + pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
1.980 end
1.981
1.982 fun appgen_split strip_abs thy tabs (c, [t2]) trns =
1.983 @@ -900,20 +812,19 @@
1.984 trns
1.985 |> exprgen_term thy tabs p
1.986 ||>> exprgen_term thy tabs body
1.987 - |-> (fn (IVarE v, body) => succeed (IAbs (v, body)))
1.988 + |-> (fn (IVarE v, body) => pair (IAbs (v, body)))
1.989 end;
1.990
1.991 -fun appgen_number_of dest_binum mk_int_to_nat thy tabs (("Numeral.number_of",
1.992 - Type ("fun", [_, Type ("IntDef.int", [])])), [bin]) trns =
1.993 - trns
1.994 - |> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer))
1.995 - handle TERM _
1.996 - => error ("not a number: " ^ Sign.string_of_term thy bin))
1.997 - | appgen_number_of dest_binum mk_int_to_nat thy tabs (("Numeral.number_of",
1.998 - Type ("fun", [_, Type ("nat", [])])), [bin]) trns =
1.999 - trns
1.1000 - |> exprgen_term thy tabs (mk_int_to_nat bin)
1.1001 - |-> succeed;
1.1002 +fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
1.1003 + Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
1.1004 + if tyco = tyco_int then
1.1005 + trns
1.1006 + |> exprgen_type thy tabs ty
1.1007 + |-> (fn ty => pair (CodegenThingol.IConst ((IntInf.toString o bin_to_int) bin, ty)))
1.1008 + else if tyco = tyco_nat then
1.1009 + trns
1.1010 + |> exprgen_term thy tabs (mk_int_to_nat bin)
1.1011 + else error ("invalid type constructor for numeral: " ^ quote tyco);
1.1012
1.1013 fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns =
1.1014 let
1.1015 @@ -938,13 +849,13 @@
1.1016 trns
1.1017 |> exprgen_term thy tabs t
1.1018 ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
1.1019 - |-> (fn (t, ds) => succeed (ICase (t, ds)))
1.1020 + |-> (fn (t, ds) => pair (ICase (t, ds)))
1.1021 end;
1.1022
1.1023 -fun gen_add_cg_case_const prep_c get_case_const_data raw_c thy =
1.1024 +fun gen_add_case_const prep_c get_case_const_data raw_c thy =
1.1025 let
1.1026 val c = prep_c thy raw_c;
1.1027 - val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_constraint thy) c;
1.1028 + val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_type thy) c;
1.1029 val cos = (the o get_case_const_data thy) c;
1.1030 val n_eta = length cos + 1;
1.1031 in
1.1032 @@ -952,8 +863,8 @@
1.1033 |> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos))
1.1034 end;
1.1035
1.1036 -val add_cg_case_const = gen_add_cg_case_const Sign.intern_const;
1.1037 -val add_cg_case_const_i = gen_add_cg_case_const (K I);
1.1038 +val add_case_const = gen_add_case_const Sign.intern_const;
1.1039 +val add_case_const_i = gen_add_case_const (K I);
1.1040
1.1041 fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns =
1.1042 case name_of_idf thy nsp_tyco dtco
1.1043 @@ -967,11 +878,10 @@
1.1044 in
1.1045 trns
1.1046 |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
1.1047 - |> fold_map (exprgen_sort thy tabs) (map snd vars)
1.1048 + |> fold_map (exprgen_tyvar_sort thy tabs) vars
1.1049 ||>> (fold_map o fold_map) (exprgen_type thy tabs o devarify_type) cotys
1.1050 |-> (fn (sorts, tys) => succeed (Datatype
1.1051 - (map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []),
1.1052 - coidfs))
1.1053 + ((sorts, coidfs ~~ tys), [])))
1.1054 end
1.1055 | NONE =>
1.1056 trns
1.1057 @@ -980,38 +890,6 @@
1.1058 trns
1.1059 |> fail ("not a type constructor: " ^ quote dtco)
1.1060
1.1061 -fun defgen_datacons get_datacons thy (tabs as (_, (_, _, dtcontab))) co trns =
1.1062 - case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
1.1063 - of SOME (co, dtco) =>
1.1064 - trns
1.1065 - |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co)
1.1066 - |> ensure_def_tyco thy tabs dtco
1.1067 - ||>> fold_map (exprgen_type thy tabs) ((the o get_datacons thy) (co, dtco))
1.1068 - |-> (fn (tyco, _) => succeed (Datatypecons tyco, []))
1.1069 - | _ =>
1.1070 - trns
1.1071 - |> fail ("not a datatype constructor: " ^ quote co);
1.1072 -
1.1073 -fun defgen_recfun get_equations thy tabs c trns =
1.1074 - case recconst_of_idf thy tabs c
1.1075 - of SOME (c, ty) =>
1.1076 - let
1.1077 - val (eqs, ty) = get_equations thy (c, ty);
1.1078 - in
1.1079 - case eqs
1.1080 - of (_::_) =>
1.1081 - trns
1.1082 - |> debug 5 (fn _ => "trying defgen recfun for " ^ quote c)
1.1083 - |> mk_fun thy tabs eqs (devarify_type ty)
1.1084 - |-> (fn def => succeed (def, []))
1.1085 - | _ =>
1.1086 - trns
1.1087 - |> fail ("no recursive definition found for " ^ quote c)
1.1088 - end
1.1089 - | NONE =>
1.1090 - trns
1.1091 - |> fail ("not a constant: " ^ quote c);
1.1092 -
1.1093
1.1094
1.1095 (** theory interface **)
1.1096 @@ -1020,46 +898,43 @@
1.1097 let
1.1098 fun extract_defs thy =
1.1099 let
1.1100 - fun dest t =
1.1101 + fun dest tm =
1.1102 let
1.1103 - val (lhs, rhs) = Logic.dest_equals t;
1.1104 - val (c, args) = strip_comb lhs;
1.1105 - val (s, T) = dest_Const c
1.1106 - in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
1.1107 + val (lhs, rhs) = Logic.dest_equals (prop_of tm);
1.1108 + val (t, args) = strip_comb lhs;
1.1109 + val (c, ty) = dest_Const t
1.1110 + in if forall is_Var args then SOME ((c, ty), tm) else NONE
1.1111 end handle TERM _ => NONE;
1.1112 fun prep_def def = (case Codegen.preprocess thy [def] of
1.1113 - [def'] => prop_of def' | _ => error "mk_auxtab: bad preprocessor");
1.1114 - fun add_def (name, t) defs = (case dest t of
1.1115 - NONE => defs
1.1116 - | SOME _ => (case (dest o prep_def oo Thm.get_axiom) thy name of
1.1117 - NONE => defs
1.1118 - | SOME (s, (T, (args, rhs))) => Symtab.update
1.1119 - (s, (T, (split_last (args @ [rhs]))) ::
1.1120 - if_none (Symtab.lookup defs s) []) defs))
1.1121 + [def'] => def' | _ => error "mk_auxtab: bad preprocessor");
1.1122 + fun add_def (name, _) =
1.1123 + case (dest o prep_def o Thm.get_axiom thy) name
1.1124 + of SOME ((c, ty), tm) =>
1.1125 + Symtab.default (c, []) #> Symtab.map_entry c (cons (ty, tm))
1.1126 + | NONE => I
1.1127 in
1.1128 Symtab.empty
1.1129 - |> fold (Symtab.fold add_def) (map
1.1130 - (snd o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
1.1131 + |> fold (Symtab.fold add_def o snd o #axioms o Theory.rep_theory)
1.1132 + (thy :: Theory.ancestors_of thy)
1.1133 end;
1.1134 fun mk_insttab thy =
1.1135 InstNameMangler.empty
1.1136 |> Symtab.fold_map
1.1137 - (fn (cls, (_, clsinsts)) => fold_map
1.1138 + (fn (cls, (clsmems, clsinsts)) => fold_map
1.1139 (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
1.1140 (ClassPackage.get_classtab thy)
1.1141 |-> (fn _ => I);
1.1142 - fun mk_overltabs thy defs =
1.1143 + fun mk_overltabs thy deftab =
1.1144 (Symtab.empty, ConstNameMangler.empty)
1.1145 |> Symtab.fold
1.1146 (fn (c, [_]) => I
1.1147 - | ("0", _) => I
1.1148 | (c, tytab) =>
1.1149 (fn (overltab1, overltab2) => (
1.1150 overltab1
1.1151 |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)),
1.1152 overltab2
1.1153 |> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab
1.1154 - ))) defs;
1.1155 + ))) deftab;
1.1156 fun mk_dtcontab thy =
1.1157 DatatypeconsNameMangler.empty
1.1158 |> fold_map
1.1159 @@ -1070,43 +945,31 @@
1.1160 in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
1.1161 ) (get_all_datatype_cons thy) [])
1.1162 |-> (fn _ => I);
1.1163 - fun mk_deftab thy defs overltab =
1.1164 - Symtab.empty
1.1165 - |> Symtab.fold
1.1166 - (fn (c, [ty_cdef]) =>
1.1167 - Symtab.update_new (idf_of_name thy nsp_const c, ty_cdef)
1.1168 - | ("0", _) => I
1.1169 - | (c, cdefs) => fold (fn (ty, cdef) =>
1.1170 - let
1.1171 - val c' = ConstNameMangler.get thy overltab
1.1172 - (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty))
1.1173 - in Symtab.update_new (c', (ty, cdef)) end) cdefs) defs;
1.1174 fun mk_clsmemtab thy =
1.1175 Symtab.empty
1.1176 |> Symtab.fold
1.1177 (fn (class, (clsmems, _)) => fold
1.1178 (fn clsmem => Symtab.update (clsmem, class)) clsmems)
1.1179 (ClassPackage.get_classtab thy);
1.1180 - val defs = extract_defs thy;
1.1181 + val deftab = extract_defs thy;
1.1182 val insttab = mk_insttab thy;
1.1183 - val overltabs = mk_overltabs thy defs;
1.1184 + val overltabs = mk_overltabs thy deftab;
1.1185 val dtcontab = mk_dtcontab thy;
1.1186 - val deftab = mk_deftab thy defs (snd overltabs);
1.1187 val clsmemtab = mk_clsmemtab thy;
1.1188 in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end;
1.1189
1.1190 -fun check_for_serializer serial_name serialize_data =
1.1191 - if Symtab.defined serialize_data serial_name
1.1192 - then serialize_data
1.1193 - else error ("unknown code serializer: " ^ quote serial_name);
1.1194 +fun check_for_target thy target =
1.1195 + if (Symtab.defined o #target_data o CodegenData.get) thy target
1.1196 + then ()
1.1197 + else error ("unknown code target language: " ^ quote target);
1.1198
1.1199 fun map_module f =
1.1200 - map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.1201 - (f modl, gens, lookups, serialize_data, logic_data));
1.1202 + map_codegen_data (fn (modl, gens, target_data, logic_data) =>
1.1203 + (f modl, gens, target_data, logic_data));
1.1204
1.1205 -fun expand_module defs gen thy =
1.1206 +fun expand_module gen thy =
1.1207 (#modl o CodegenData.get) thy
1.1208 - |> start_transact (gen thy defs)
1.1209 + |> start_transact (gen thy (mk_tabs thy))
1.1210 |-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
1.1211
1.1212 fun rename_inconsistent thy =
1.1213 @@ -1141,7 +1004,7 @@
1.1214 then
1.1215 (warning ("case constant " ^ quote case_c ^ " already present in application table, will not overwrite"); thy)
1.1216 else
1.1217 - add_cg_case_const_i get_case_const_data case_c thy;
1.1218 + add_case_const_i get_case_const_data case_c thy;
1.1219 in
1.1220 fold ensure (get_datatype_case_consts thy) thy
1.1221 end;
1.1222 @@ -1152,17 +1015,28 @@
1.1223
1.1224 (* primitive definitions *)
1.1225
1.1226 +fun read_typ thy =
1.1227 + Sign.read_typ (thy, K NONE);
1.1228 +
1.1229 fun read_const thy (raw_c, raw_ty) =
1.1230 let
1.1231 val c = Sign.intern_const thy raw_c;
1.1232 + val _ = if Sign.declared_const thy c
1.1233 + then ()
1.1234 + else error ("no such constant: " ^ quote c);
1.1235 val ty = case raw_ty
1.1236 of NONE => Sign.the_const_constraint thy c
1.1237 - | SOME raw_ty => Sign.read_typ (thy, K NONE) raw_ty;
1.1238 + | SOME raw_ty => read_typ thy raw_ty;
1.1239 in (c, ty) end;
1.1240
1.1241 +fun read_quote reader gen raw thy =
1.1242 + expand_module
1.1243 + (fn thy => fn tabs => gen thy tabs (reader thy raw))
1.1244 + thy;
1.1245 +
1.1246 fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy =
1.1247 let
1.1248 - val _ = if Symtab.defined ((#serialize_data o CodegenData.get) thy) target
1.1249 + val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target
1.1250 then () else error ("unknown target language: " ^ quote target);
1.1251 val tabs = mk_tabs thy;
1.1252 val name = prep_name thy tabs raw_name;
1.1253 @@ -1175,133 +1049,128 @@
1.1254 val add_prim_i = gen_add_prim ((K o K) I) I;
1.1255 val add_prim_class = gen_add_prim
1.1256 (fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy))
1.1257 - (Pretty.str o newline_correct o Symbol.strip_blanks);
1.1258 + (Pretty.str o CodegenSerializer.parse_targetdef I);
1.1259 val add_prim_tyco = gen_add_prim
1.1260 (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
1.1261 - (Pretty.str o newline_correct o Symbol.strip_blanks);
1.1262 + (Pretty.str o CodegenSerializer.parse_targetdef I);
1.1263 val add_prim_const = gen_add_prim
1.1264 (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
1.1265 - (Pretty.str o newline_correct o Symbol.strip_blanks);
1.1266 + (Pretty.str o CodegenSerializer.parse_targetdef I);
1.1267
1.1268 -val ensure_prim = (map_module o CodegenThingol.ensure_prim);
1.1269 +val ensure_prim = (map_module oo CodegenThingol.ensure_prim);
1.1270
1.1271
1.1272 (* syntax *)
1.1273
1.1274 -fun gen_prep_mfx read_quote mk_quote tabs mfx thy =
1.1275 +val parse_syntax_tyco =
1.1276 let
1.1277 - val proto_mfx = Codegen.parse_mixfix (read_quote thy) mfx;
1.1278 - fun generate thy tabs = fold_map (mk_quote thy tabs)
1.1279 - (Codegen.quotes_of proto_mfx);
1.1280 + fun mk reader raw_tyco target thy =
1.1281 + let
1.1282 + val _ = check_for_target thy target;
1.1283 + fun check_tyco tyco =
1.1284 + if Sign.declared_tyname thy tyco
1.1285 + then tyco
1.1286 + else error ("no such type constructor: " ^ quote tyco);
1.1287 + fun prep_tyco thy tyco =
1.1288 + tyco
1.1289 + |> Sign.intern_type thy
1.1290 + |> check_tyco
1.1291 + |> idf_of_name thy nsp_tyco;
1.1292 + val tyco = prep_tyco thy raw_tyco;
1.1293 + in
1.1294 + thy
1.1295 + |> ensure_prim tyco target
1.1296 + |> reader
1.1297 + |-> (fn pretty => map_codegen_data
1.1298 + (fn (modl, gens, target_data, logic_data) =>
1.1299 + (modl, gens,
1.1300 + target_data |> Symtab.map_entry target
1.1301 + (map_target_data
1.1302 + (fn (syntax_tyco, syntax_const) =>
1.1303 + (syntax_tyco |> Symtab.update_new
1.1304 + (tyco, (pretty, stamp ())),
1.1305 + syntax_const))),
1.1306 + logic_data)))
1.1307 + end;
1.1308 in
1.1309 - thy
1.1310 - |> expand_module tabs generate
1.1311 - |-> (fn tys => pair (Codegen.replace_quotes tys proto_mfx))
1.1312 + CodegenSerializer.parse_syntax (read_quote read_typ exprgen_type)
1.1313 + #-> (fn reader => pair (mk reader))
1.1314 end;
1.1315
1.1316 -fun gen_add_syntax_tyco prep_tyco prep_mfx raw_tyco (serial_name, (raw_mfx, fixity)) thy =
1.1317 +val parse_syntax_const =
1.1318 let
1.1319 - val tyco = prep_tyco thy raw_tyco;
1.1320 - val tabs = mk_tabs thy;
1.1321 + fun mk reader raw_const target thy =
1.1322 + let
1.1323 + val _ = check_for_target thy target;
1.1324 + val tabs = mk_tabs thy;
1.1325 + val c = idf_of_const thy tabs (read_const thy raw_const);
1.1326 + in
1.1327 + thy
1.1328 + |> ensure_prim c target
1.1329 + |> reader
1.1330 + |-> (fn pretty => map_codegen_data
1.1331 + (fn (modl, gens, target_data, logic_data) =>
1.1332 + (modl, gens,
1.1333 + target_data |> Symtab.map_entry target
1.1334 + (map_target_data
1.1335 + (fn (syntax_tyco, syntax_const) =>
1.1336 + (syntax_tyco,
1.1337 + syntax_const
1.1338 + |> Symtab.update_new
1.1339 + (c, (pretty, stamp ()))))),
1.1340 + logic_data)))
1.1341 + end;
1.1342 in
1.1343 - thy
1.1344 - |> ensure_prim tyco
1.1345 - |> prep_mfx tabs raw_mfx
1.1346 - |-> (fn mfx => map_codegen_data
1.1347 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.1348 - (modl, gens, lookups,
1.1349 - serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
1.1350 - (map_serialize_data
1.1351 - (fn (syntax_tyco, syntax_const) =>
1.1352 - (syntax_tyco |> Symtab.update_new
1.1353 - (tyco,
1.1354 - (((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ())),
1.1355 - syntax_const))),
1.1356 - logic_data)))
1.1357 + CodegenSerializer.parse_syntax (read_quote Sign.read_term exprgen_term)
1.1358 + #-> (fn reader => pair (mk reader))
1.1359 end;
1.1360
1.1361 -val add_syntax_tyco_i = gen_add_syntax_tyco (K I) (K pair);
1.1362 -val add_syntax_tyco = gen_add_syntax_tyco
1.1363 - (fn thy => idf_of_name thy nsp_tyco o Sign.intern_type thy)
1.1364 - (gen_prep_mfx (fn thy => typ_of o read_ctyp thy)
1.1365 - (fn thy => fn tabs => exprgen_type thy tabs o devarify_type));
1.1366 -
1.1367 -fun gen_add_syntax_const prep_const prep_mfx raw_c (serial_name, (raw_mfx, fixity)) thy =
1.1368 - let
1.1369 - val tabs = mk_tabs thy;
1.1370 - val c = prep_const thy tabs raw_c;
1.1371 - in
1.1372 - thy
1.1373 - |> ensure_prim c
1.1374 - |> prep_mfx tabs raw_mfx
1.1375 - |-> (fn mfx => map_codegen_data
1.1376 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
1.1377 - (modl, gens, lookups,
1.1378 - serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
1.1379 - (map_serialize_data
1.1380 - (fn (syntax_tyco, syntax_const) =>
1.1381 - (syntax_tyco,
1.1382 - syntax_const |> Symtab.update_new
1.1383 - (c,
1.1384 - (((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ()))))),
1.1385 - logic_data)))
1.1386 - end;
1.1387 -
1.1388 -val add_syntax_const_i = gen_add_syntax_const ((K o K) I) (K pair);
1.1389 -val add_syntax_const = gen_add_syntax_const
1.1390 - (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
1.1391 - (gen_prep_mfx (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT)
1.1392 - (fn thy => fn tabs => exprgen_term thy tabs o devarify_term));
1.1393 -
1.1394
1.1395
1.1396 (** code generation **)
1.1397
1.1398 -fun get_serializer thy serial_name =
1.1399 - (#serializer o (fn data => (the oo Symtab.lookup) data serial_name)
1.1400 - o #serialize_data o CodegenData.get) thy;
1.1401 -
1.1402 -fun mk_const thy (f, s_ty) =
1.1403 +fun generate_code raw_consts thy =
1.1404 let
1.1405 - val f' = Sign.intern_const thy f;
1.1406 - val ty = case s_ty
1.1407 - of NONE => Sign.the_const_constraint thy f'
1.1408 - | SOME s => Sign.read_typ (thy, K NONE) s;
1.1409 - in (f', ty) end;
1.1410 -
1.1411 -fun generate_code consts thy =
1.1412 - let
1.1413 - val tabs = mk_tabs thy;
1.1414 - val consts' = map (mk_const thy) consts;
1.1415 - fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts'
1.1416 + val consts = map (read_const thy) raw_consts;
1.1417 + fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
1.1418 in
1.1419 thy
1.1420 - |> expand_module tabs generate
1.1421 - |-> (fn consts => pair consts)
1.1422 + |> expand_module generate
1.1423 end;
1.1424
1.1425 -fun serialize_code serial_name filename consts thy =
1.1426 +fun serialize_code target filename raw_consts thy =
1.1427 let
1.1428 - val serialize_data =
1.1429 - thy
1.1430 - |> CodegenData.get
1.1431 - |> #serialize_data
1.1432 - |> check_for_serializer serial_name
1.1433 - |> (fn data => (the oo Symtab.lookup) data serial_name)
1.1434 - val serializer' = (get_serializer thy serial_name) serial_name
1.1435 - ((Option.map fst oo Symtab.lookup o #syntax_tyco) serialize_data)
1.1436 - ((Option.map fst oo Symtab.lookup o #syntax_const) serialize_data);
1.1437 - val compile_it = serial_name = "ml" andalso filename = "-";
1.1438 + fun get_serializer thy target =
1.1439 + let
1.1440 + val _ = check_for_target thy target;
1.1441 + val target_data =
1.1442 + thy
1.1443 + |> CodegenData.get
1.1444 + |> #target_data
1.1445 + |> (fn data => (the oo Symtab.lookup) data target);
1.1446 + in
1.1447 + (the o Symtab.lookup (! serializers)) target (
1.1448 + (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
1.1449 + (Option.map fst oo Symtab.lookup o #syntax_const) target_data
1.1450 + )
1.1451 + end;
1.1452 fun use_code code =
1.1453 - if compile_it
1.1454 + if target = "ml" andalso filename = "-"
1.1455 then use_text Context.ml_output false code
1.1456 else File.write (Path.unpack filename) (code ^ "\n");
1.1457 + fun serialize thy cs =
1.1458 + let
1.1459 + val module = (#modl o CodegenData.get) thy;
1.1460 + val seri = get_serializer thy target "Generated";
1.1461 + in case cs
1.1462 + of [] => seri NONE module () |> fst |> Pretty.output |> use_code
1.1463 + | cs => seri (SOME cs) module () |> fst |> Pretty.output |> use_code
1.1464 + end;
1.1465 in
1.1466 thy
1.1467 - |> (if is_some consts then generate_code (the consts) else pair [])
1.1468 - |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get)
1.1469 - | consts => `(serializer' (SOME consts) o #modl o CodegenData.get))
1.1470 - |-> (fn code => ((use_code o Pretty.output) code; I))
1.1471 + |> (if is_some raw_consts then generate_code (the raw_consts) else pair [])
1.1472 + |-> (fn cs => `(fn thy => serialize thy cs))
1.1473 + |-> (fn _ => I)
1.1474 end;
1.1475
1.1476
1.1477 @@ -1347,68 +1216,71 @@
1.1478 P.$$$ constantsK
1.1479 |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
1.1480 )
1.1481 - >> (fn ((serial_name, filename), consts) =>
1.1482 - Toplevel.theory (serialize_code serial_name filename consts))
1.1483 + >> (fn ((target, filename), raw_consts) =>
1.1484 + Toplevel.theory (serialize_code target filename raw_consts))
1.1485 );
1.1486
1.1487 val aliasP =
1.1488 OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
1.1489 - P.xname
1.1490 - -- P.xname
1.1491 - >> (fn (src, dst) => Toplevel.theory (add_alias (src, dst)))
1.1492 + Scan.repeat1 (P.name -- P.name)
1.1493 + >> (Toplevel.theory oo fold) add_alias
1.1494 );
1.1495
1.1496 val primclassP =
1.1497 OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl (
1.1498 P.xname
1.1499 + -- Scan.optional (P.$$$ dependingK |--
1.1500 + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
1.1501 -- Scan.repeat1 (P.name -- P.text)
1.1502 - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) []
1.1503 - >> (fn ((raw_class, primdefs), depends) =>
1.1504 + >> (fn ((raw_class, depends), primdefs) =>
1.1505 (Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs)
1.1506 );
1.1507
1.1508 val primtycoP =
1.1509 OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl (
1.1510 P.xname
1.1511 + -- Scan.optional (P.$$$ dependingK |--
1.1512 + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
1.1513 -- Scan.repeat1 (P.name -- P.text)
1.1514 - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) []
1.1515 - >> (fn ((raw_tyco, primdefs), depends) =>
1.1516 + >> (fn ((raw_tyco, depends), primdefs) =>
1.1517 (Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs)
1.1518 );
1.1519
1.1520 val primconstP =
1.1521 OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
1.1522 - (P.xname -- Scan.option P.typ)
1.1523 + (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
1.1524 + -- Scan.optional (P.$$$ dependingK |--
1.1525 + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
1.1526 -- Scan.repeat1 (P.name -- P.text)
1.1527 - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) []
1.1528 - >> (fn ((raw_const, primdefs), depends) =>
1.1529 + >> (fn ((raw_const, depends), primdefs) =>
1.1530 (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs)
1.1531 );
1.1532
1.1533 +val _ : OuterParse.token list -> (string -> string -> theory -> theory) * OuterParse.token list
1.1534 + = parse_syntax_tyco;
1.1535 +
1.1536 val syntax_tycoP =
1.1537 OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
1.1538 - P.xname
1.1539 - -- Scan.repeat1 (
1.1540 - P.name -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
1.1541 - -- CodegenSerializer.parse_fixity
1.1542 - )
1.1543 - >> (fn (raw_tyco, stxs) =>
1.1544 - (Toplevel.theory oo fold)
1.1545 - (fn ((target, raw_mfx), fixity) =>
1.1546 - add_syntax_tyco raw_tyco (target, (raw_mfx, fixity))) stxs)
1.1547 + Scan.repeat1 (
1.1548 + P.xname
1.1549 + -- Scan.repeat1 (
1.1550 + P.name -- parse_syntax_tyco
1.1551 + )
1.1552 + )
1.1553 + >> (Toplevel.theory oo fold) (fn (raw_tyco, syns) =>
1.1554 + fold (fn (target, modifier) => modifier raw_tyco target) syns)
1.1555 );
1.1556
1.1557 val syntax_constP =
1.1558 OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
1.1559 - (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
1.1560 - -- Scan.repeat1 (
1.1561 - P.name -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
1.1562 - -- CodegenSerializer.parse_fixity
1.1563 - )
1.1564 - >> (fn (raw_c, stxs) =>
1.1565 - (Toplevel.theory oo fold)
1.1566 - (fn ((target, raw_mfx), fixity) =>
1.1567 - add_syntax_const raw_c (target, (raw_mfx, fixity))) stxs)
1.1568 + Scan.repeat1 (
1.1569 + (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
1.1570 + -- Scan.repeat1 (
1.1571 + P.name -- parse_syntax_const
1.1572 + )
1.1573 + )
1.1574 + >> (Toplevel.theory oo fold) (fn (raw_c, syns) =>
1.1575 + fold (fn (target, modifier) => modifier raw_c target) syns)
1.1576 );
1.1577
1.1578 val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP,
1.1579 @@ -1419,67 +1291,16 @@
1.1580
1.1581 (** setup **)
1.1582
1.1583 -val _ =
1.1584 - let
1.1585 - val bool = Type ("bool", []);
1.1586 - val nat = Type ("nat", []);
1.1587 - val int = Type ("IntDef.int", []);
1.1588 - fun list t = Type ("List.list", [t]);
1.1589 - fun pair t1 t2 = Type ("*", [t1, t2]);
1.1590 - val A = TVar (("'a", 0), []);
1.1591 - val B = TVar (("'b", 0), []);
1.1592 - in Context.add_setup [
1.1593 - CodegenData.init,
1.1594 - add_appconst_i ("neg", ((0, 0), appgen_neg)),
1.1595 - add_appconst_i ("op =", ((2, 2), appgen_eq)),
1.1596 - add_defgen ("clsdecl", defgen_clsdecl),
1.1597 - add_defgen ("tyco_fallback", defgen_tyco_fallback),
1.1598 - add_defgen ("const_fallback", defgen_const_fallback),
1.1599 - add_defgen ("defs", defgen_defs),
1.1600 - add_defgen ("clsmem", defgen_clsmem),
1.1601 - add_defgen ("clsinst", defgen_clsinst),
1.1602 - add_alias ("op -->", "HOL.op_implies"),
1.1603 - add_alias ("op +", "HOL.op_add"),
1.1604 - add_alias ("op -", "HOL.op_minus"),
1.1605 - add_alias ("op *", "HOL.op_times"),
1.1606 - add_alias ("op <=", "Orderings.op_le"),
1.1607 - add_alias ("op <", "Orderings.op_lt"),
1.1608 - add_alias ("List.op @", "List.append"),
1.1609 - add_alias ("List.op mem", "List.member"),
1.1610 - add_alias ("Divides.op div", "Divides.div"),
1.1611 - add_alias ("Divides.op dvd", "Divides.dvd"),
1.1612 - add_alias ("Divides.op mod", "Divides.mod"),
1.1613 - add_lookup_tyco ("bool", type_bool),
1.1614 - add_lookup_tyco ("*", type_pair),
1.1615 - add_lookup_tyco ("IntDef.int", type_integer),
1.1616 - add_lookup_tyco ("List.list", type_list),
1.1617 - add_lookup_const (("True", bool), Cons_true),
1.1618 - add_lookup_const (("False", bool), Cons_false),
1.1619 - add_lookup_const (("Not", bool --> bool), Fun_not),
1.1620 - add_lookup_const (("op &", bool --> bool --> bool), Fun_and),
1.1621 - add_lookup_const (("op |", bool --> bool --> bool), Fun_or),
1.1622 - add_lookup_const (("HOL.If", bool --> A --> A --> A), Fun_if),
1.1623 - add_lookup_const (("Pair", A --> B --> pair A B), Cons_pair),
1.1624 - add_lookup_const (("fst", pair A B --> A), Fun_fst),
1.1625 - add_lookup_const (("snd", pair A B --> B), Fun_snd),
1.1626 - add_lookup_const (("List.list.Cons", A --> list A --> list A), Cons_cons),
1.1627 - add_lookup_const (("List.list.Nil", list A), Cons_nil),
1.1628 - add_lookup_const (("1", nat),
1.1629 - IApp (
1.1630 - IConst ("const.Suc", IFun (IType ("type.nat", []), IFun (IType ("type.nat", []), IType ("type.nat", [])))),
1.1631 - IConst ("const.Zero", IType ("type.nat", []))
1.1632 - )),
1.1633 - add_lookup_const (("0", int), Fun_0),
1.1634 - add_lookup_const (("1", int), Fun_1),
1.1635 - add_lookup_const (("op +", int --> int --> int), Fun_add),
1.1636 - add_lookup_const (("op *", int --> int --> int), Fun_mult),
1.1637 - add_lookup_const (("uminus", int --> int), Fun_minus),
1.1638 - add_lookup_const (("op <", int --> int --> bool), Fun_lt),
1.1639 - add_lookup_const (("op <=", int --> int --> bool), Fun_le),
1.1640 - add_lookup_const (("Wellfounded_Recursion.wfrec", ((A --> B) --> A --> B) --> A --> B), Fun_wfrec)
1.1641 - ] end;
1.1642 -
1.1643 -(* "op /" ??? *)
1.1644 +val _ = Context.add_setup [
1.1645 + CodegenData.init,
1.1646 +(* add_appconst_i ("op =", ((2, 2), appgen_eq)), *)
1.1647 + add_eqextr ("defs", eqextr_defs),
1.1648 + add_defgen ("clsdecl", defgen_clsdecl),
1.1649 + add_defgen ("funs", defgen_funs),
1.1650 + add_defgen ("clsmem", defgen_clsmem),
1.1651 + add_defgen ("datatypecons", defgen_datatypecons)(*,
1.1652 + add_defgen ("clsinst", defgen_clsinst) *)
1.1653 +];
1.1654
1.1655 end; (* local *)
1.1656