# HG changeset patch # User haftmann # Date 1153913467 -7200 # Node ID f30b733850602ad56f7b539acbade6f151f9d286 # Parent 96a4b3b7a6aadfbe5e2e0cfa07c4971aaf620dfc added eval_term diff -r 96a4b3b7a6aa -r f30b73385060 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Wed Jul 26 11:32:55 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Wed Jul 26 13:31:07 2006 +0200 @@ -64,7 +64,7 @@ fun alias_get name = (fst o !) alias_ref name; fun alias_rev name = (snd o !) alias_ref name; -val nsp_module = ""; (* a dummy by convention *) +val nsp_module = ""; (*a dummy by convention*) val nsp_class = "class"; val nsp_tyco = "tyco"; val nsp_const = "const"; @@ -73,6 +73,7 @@ val nsp_mem = "mem"; val nsp_inst = "inst"; val nsp_instmem = "instmem"; +val nsp_eval = "EVAL"; (*only for evaluation*) fun add_nsp shallow name = name @@ -1040,24 +1041,11 @@ |> CodegenTheorems.notify_dirty |> `(#modl o CodegenData.get); -fun serialize_module module (target_data : target_data) cs seri = - let - val s_class = #syntax_class target_data - val s_tyco = #syntax_tyco target_data - val s_const = #syntax_const target_data - in - (seri ( - Symtab.lookup s_class, - (Option.map fst oo Symtab.lookup) s_tyco, - (Option.map fst oo Symtab.lookup) s_const - ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit) - end; - fun eval_term (ref_spec, t) thy = let val target_data = ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; - val eval = CodegenSerializer.eval_term nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]] + val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]] ((Option.map fst oo Symtab.lookup) (#syntax_tyco target_data), (Option.map fst oo Symtab.lookup) (#syntax_const target_data)) (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data)) @@ -1240,8 +1228,15 @@ |> CodegenData.get |> #target_data |> (fn data => (the oo Symtab.lookup) data target); + val s_class = #syntax_class target_data + val s_tyco = #syntax_tyco target_data + val s_const = #syntax_const target_data in - (serialize_module module target_data cs; thy) + (seri ( + Symtab.lookup s_class, + (Option.map fst oo Symtab.lookup) s_tyco, + (Option.map fst oo Symtab.lookup) s_const + ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy) end; in thy diff -r 96a4b3b7a6aa -r f30b73385060 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Wed Jul 26 11:32:55 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Wed Jul 26 13:31:07 2006 +0200 @@ -26,7 +26,7 @@ haskell: string * (string * string list -> serializer) }; val mk_flat_ml_resolver: string list -> string -> string; - val eval_term: string -> string list list + val eval_term: string -> string -> string list list -> (string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iterm pretty_syntax option) -> string list @@ -797,16 +797,16 @@ || parse_single_file serializer end; -fun eval_term nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl = +fun eval_term nsp_eval nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl = let - val (val_name, modl') = CodegenThingol.add_eval_def e modl; + val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl; val struct_name = "EVAL"; val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE)) - | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [val_name]); + | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]); val _ = serializer modl'; val val_name_struct = NameSpace.append struct_name val_name; - val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")"); + val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())"); val value = ! reff; in value end; diff -r 96a4b3b7a6aa -r f30b73385060 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Wed Jul 26 11:32:55 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Wed Jul 26 13:31:07 2006 +0200 @@ -88,7 +88,7 @@ val diff_module: module * module -> (string * def) list; val project_module: string list -> module -> module; val purge_module: string list -> module -> module; - val add_eval_def: iterm -> module -> string * module; + val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module; val delete_garbage: string list (*hidden definitions*) -> module -> module; val has_nsp: string -> string -> bool; val ensure_def: (string -> transact -> def transact_fin) -> bool -> string @@ -833,7 +833,7 @@ empty_module |> fold (fn name => add_def (name, get_def modl name)) selected (* |> fold ensure_bot (hidden @ bots') *) - |> fold (fn (x, y) => (writeln ("adding " ^ x ^ " -> " ^ y); add_dep (x, y))) adddeps + |> fold (fn (x, y) => ((*writeln ("adding " ^ x ^ " -> " ^ y);*) add_dep (x, y))) adddeps end; fun allimports_of modl = @@ -1028,13 +1028,14 @@ |-> (fn x => fn (_, modl) => (x, modl)) end; -fun add_eval_def e modl = +fun add_eval_def (shallow, e) modl = let - val name = hd (Name.invent_list (Graph.keys modl) "VALUE" 1); + val name = "VALUE"; + val sname = NameSpace.pack [shallow, name]; in modl - |> add_def (name, Fun ([([], e)], ([], "" `%% []))) - |> fold (curry add_dep name) (add_deps_of_term e []) + |> add_def (sname, Fun ([([], e)], ([("a", [])], ITyVar "a"))) + |> fold (curry add_dep sname) (add_deps_of_term e []) |> pair name end;