# HG changeset patch # User haftmann # Date 1168327912 -3600 # Node ID fbf0a12d053f39643077c3222671d619c709281d # Parent 8919dbe67c907677f1c5b13321400b97bc8e4ef8 proper node names diff -r 8919dbe67c90 -r fbf0a12d053f src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Jan 09 08:31:51 2007 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Jan 09 08:31:52 2007 +0100 @@ -74,18 +74,13 @@ -> code -> code; val add_eval_def: string (*bind name*) * iterm -> code -> code; - val ensure_def: (transact -> def * code) -> bool -> string + val ensure_def: (string -> string) -> (transact -> def * code) -> bool -> string -> string -> transact -> transact; val succeed: 'a -> transact -> 'a * code; val fail: string -> transact -> 'a * code; val message: string -> (transact -> 'a) -> transact -> 'a; val start_transact: string option -> (transact -> 'a * transact) -> code -> 'a * code; - type var_ctxt; - val make_vars: string list -> var_ctxt; - val intro_vars: string list -> var_ctxt -> var_ctxt; - val lookup_var: var_ctxt -> string -> string; - val trace: bool ref; val tracing: ('a -> string) -> 'a -> 'a; end; @@ -383,16 +378,16 @@ (* transaction protocol *) -fun ensure_def defgen strict msg name (dep, code) = +fun ensure_def labelled_name defgen strict msg name (dep, code) = let - (*FIXME represent dependencies as tuple (name, name -> string), for better error msgs*) val msg' = (case dep of NONE => msg - | SOME dep => msg ^ ", required for " ^ quote dep) + | SOME dep => msg ^ ", required for " ^ labelled_name dep) ^ (if strict then " (strict)" else " (non-strict)"); fun add_dp NONE = I | add_dp (SOME dep) = - tracing (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name) + tracing (fn _ => "adding dependency " ^ labelled_name dep + ^ " -> " ^ labelled_name name) #> add_dep (dep, name); fun prep_def def code = (check_prep_def code def, code); @@ -405,13 +400,14 @@ code |> (if can (get_def code) name then - tracing (fn _ => "asserting node " ^ quote name) + tracing (fn _ => "asserting definition " ^ labelled_name name) #> add_dp dep else - tracing (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)")) + tracing (fn _ => "allocating definition " ^ labelled_name name + ^ (if strict then " (strict)" else " (non-strict)")) #> ensure_bot name #> add_dp dep - #> tracing (fn _ => "creating node " ^ quote name) + #> tracing (fn _ => "creating definition " ^ labelled_name name) #> invoke_generator name defgen #-> (fn def => prep_def def) #-> (fn def => @@ -451,24 +447,6 @@ |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_"))) |> fold (curry Graph.add_edge name) (Graph.keys code); - -(** variable name contexts **) - -type var_ctxt = string Symtab.table * Name.context; - -fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, - Name.make_context names); - -fun intro_vars names (namemap, namectxt) = - let - val (names', namectxt') = Name.variants names namectxt; - val namemap' = fold2 (curry Symtab.update) names names' namemap; - in (namemap', namectxt') end; - -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name - of SOME name' => name' - | NONE => error ("invalid name in context: " ^ quote name); - end; (*struct*)