src/Tools/code/code_thingol.ML
author haftmann
Mon Aug 13 21:22:41 2007 +0200 (2007-08-13)
changeset 24252 4eb5bc6af008
parent 24219 e558fe311376
child 24283 8ca96f4e49cd
permissions -rw-r--r--
simplified
haftmann@24219
     1
(*  Title:      Tools/code/code_thingol.ML
haftmann@24219
     2
    ID:         $Id$
haftmann@24219
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@24219
     4
haftmann@24219
     5
Intermediate language ("Thin-gol") representing executable code.
haftmann@24219
     6
*)
haftmann@24219
     7
haftmann@24219
     8
infix 8 `%%;
haftmann@24219
     9
infixr 6 `->;
haftmann@24219
    10
infixr 6 `-->;
haftmann@24219
    11
infix 4 `$;
haftmann@24219
    12
infix 4 `$$;
haftmann@24219
    13
infixr 3 `|->;
haftmann@24219
    14
infixr 3 `|-->;
haftmann@24219
    15
haftmann@24219
    16
signature BASIC_CODE_THINGOL =
haftmann@24219
    17
sig
haftmann@24219
    18
  type vname = string;
haftmann@24219
    19
  datatype dict =
haftmann@24219
    20
      DictConst of string * dict list list
haftmann@24219
    21
    | DictVar of string list * (vname * (int * int));
haftmann@24219
    22
  datatype itype =
haftmann@24219
    23
      `%% of string * itype list
haftmann@24219
    24
    | ITyVar of vname;
haftmann@24219
    25
  datatype iterm =
haftmann@24219
    26
      IConst of string * (dict list list * itype list (*types of arguments*))
haftmann@24219
    27
    | IVar of vname
haftmann@24219
    28
    | `$ of iterm * iterm
haftmann@24219
    29
    | `|-> of (vname * itype) * iterm
haftmann@24219
    30
    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@24219
    31
        (*((term, type), [(selector pattern, body term )]), primitive term)*)
haftmann@24219
    32
  val `-> : itype * itype -> itype;
haftmann@24219
    33
  val `--> : itype list * itype -> itype;
haftmann@24219
    34
  val `$$ : iterm * iterm list -> iterm;
haftmann@24219
    35
  val `|--> : (vname * itype) list * iterm -> iterm;
haftmann@24219
    36
  type typscheme = (vname * sort) list * itype;
haftmann@24219
    37
end;
haftmann@24219
    38
haftmann@24219
    39
signature CODE_THINGOL =
haftmann@24219
    40
sig
haftmann@24219
    41
  include BASIC_CODE_THINGOL;
haftmann@24219
    42
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
haftmann@24219
    43
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
haftmann@24219
    44
  val unfold_fun: itype -> itype list * itype;
haftmann@24219
    45
  val unfold_app: iterm -> iterm * iterm list;
haftmann@24219
    46
  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
haftmann@24219
    47
  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
haftmann@24219
    48
  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
haftmann@24219
    49
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
haftmann@24219
    50
  val unfold_const_app: iterm ->
haftmann@24219
    51
    ((string * (dict list list * itype list)) * iterm list) option;
haftmann@24219
    52
  val collapse_let: ((vname * itype) * iterm) * iterm
haftmann@24219
    53
    -> (iterm * itype) * (iterm * iterm) list;
haftmann@24219
    54
  val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
haftmann@24219
    55
  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    56
  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    57
  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    58
haftmann@24219
    59
  datatype def =
haftmann@24219
    60
      Bot
haftmann@24219
    61
    | Fun of (iterm list * iterm) list * typscheme
haftmann@24219
    62
    | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
    63
    | Datatypecons of string
haftmann@24219
    64
    | Class of (class * string) list * (vname * (string * itype) list)
haftmann@24219
    65
    | Classop of class
haftmann@24219
    66
    | Classrel of class * class
haftmann@24219
    67
    | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
    68
          * ((class * (string * (string * dict list list))) list
haftmann@24219
    69
        * (string * iterm) list);
haftmann@24219
    70
  type code = def Graph.T;
haftmann@24219
    71
  type transact;
haftmann@24219
    72
  val empty_code: code;
haftmann@24219
    73
  val merge_code: code * code -> code;
haftmann@24219
    74
  val project_code: bool (*delete empty funs*)
haftmann@24219
    75
    -> string list (*hidden*) -> string list option (*selected*)
haftmann@24219
    76
    -> code -> code;
haftmann@24219
    77
  val empty_funs: code -> string list;
haftmann@24219
    78
  val is_cons: code -> string -> bool;
haftmann@24219
    79
  val add_eval_def: string (*bind name*) * iterm -> code -> code;
haftmann@24219
    80
haftmann@24252
    81
  val ensure_def: (string -> string) -> (transact -> def * transact) -> string
haftmann@24219
    82
    -> string -> transact -> transact;
haftmann@24219
    83
  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
haftmann@24219
    84
end;
haftmann@24219
    85
haftmann@24219
    86
structure CodeThingol: CODE_THINGOL =
haftmann@24219
    87
struct
haftmann@24219
    88
haftmann@24219
    89
(** auxiliary **)
haftmann@24219
    90
haftmann@24219
    91
fun unfoldl dest x =
haftmann@24219
    92
  case dest x
haftmann@24219
    93
   of NONE => (x, [])
haftmann@24219
    94
    | SOME (x1, x2) =>
haftmann@24219
    95
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
haftmann@24219
    96
haftmann@24219
    97
fun unfoldr dest x =
haftmann@24219
    98
  case dest x
haftmann@24219
    99
   of NONE => ([], x)
haftmann@24219
   100
    | SOME (x1, x2) =>
haftmann@24219
   101
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
haftmann@24219
   102
haftmann@24219
   103
haftmann@24219
   104
(** language core - types, pattern, expressions **)
haftmann@24219
   105
haftmann@24219
   106
(* language representation *)
haftmann@24219
   107
haftmann@24219
   108
type vname = string;
haftmann@24219
   109
haftmann@24219
   110
datatype dict =
haftmann@24219
   111
    DictConst of string * dict list list
haftmann@24219
   112
  | DictVar of string list * (vname * (int * int));
haftmann@24219
   113
haftmann@24219
   114
datatype itype =
haftmann@24219
   115
    `%% of string * itype list
haftmann@24219
   116
  | ITyVar of vname;
haftmann@24219
   117
haftmann@24219
   118
datatype iterm =
haftmann@24219
   119
    IConst of string * (dict list list * itype list)
haftmann@24219
   120
  | IVar of vname
haftmann@24219
   121
  | `$ of iterm * iterm
haftmann@24219
   122
  | `|-> of (vname * itype) * iterm
haftmann@24219
   123
  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@24219
   124
    (*see also signature*)
haftmann@24219
   125
haftmann@24219
   126
(*
haftmann@24219
   127
  variable naming conventions
haftmann@24219
   128
haftmann@24219
   129
  bare names:
haftmann@24219
   130
    variable names          v
haftmann@24219
   131
    class names             class
haftmann@24219
   132
    type constructor names  tyco
haftmann@24219
   133
    datatype names          dtco
haftmann@24219
   134
    const names (general)   c
haftmann@24219
   135
    constructor names       co
haftmann@24219
   136
    class operation names   clsop (op)
haftmann@24219
   137
    arbitrary name          s
haftmann@24219
   138
haftmann@24219
   139
    v, c, co, clsop also annotated with types etc.
haftmann@24219
   140
haftmann@24219
   141
  constructs:
haftmann@24219
   142
    sort                    sort
haftmann@24219
   143
    type parameters         vs
haftmann@24219
   144
    type                    ty
haftmann@24219
   145
    type schemes            tysm
haftmann@24219
   146
    term                    t
haftmann@24219
   147
    (term as pattern)       p
haftmann@24219
   148
    instance (class, tyco)  inst
haftmann@24219
   149
 *)
haftmann@24219
   150
haftmann@24219
   151
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
haftmann@24219
   152
val op `--> = Library.foldr (op `->);
haftmann@24219
   153
val op `$$ = Library.foldl (op `$);
haftmann@24219
   154
val op `|--> = Library.foldr (op `|->);
haftmann@24219
   155
haftmann@24219
   156
val unfold_fun = unfoldr
haftmann@24219
   157
  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
haftmann@24219
   158
    | _ => NONE);
haftmann@24219
   159
haftmann@24219
   160
val unfold_app = unfoldl
haftmann@24219
   161
  (fn op `$ t => SOME t
haftmann@24219
   162
    | _ => NONE);
haftmann@24219
   163
haftmann@24219
   164
val split_abs =
haftmann@24219
   165
  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
haftmann@24219
   166
        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
haftmann@24219
   167
    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
haftmann@24219
   168
    | _ => NONE);
haftmann@24219
   169
haftmann@24219
   170
val unfold_abs = unfoldr split_abs;
haftmann@24219
   171
haftmann@24219
   172
val split_let = 
haftmann@24219
   173
  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
haftmann@24219
   174
    | _ => NONE);
haftmann@24219
   175
haftmann@24219
   176
val unfold_let = unfoldr split_let;
haftmann@24219
   177
haftmann@24219
   178
fun unfold_const_app t =
haftmann@24219
   179
 case unfold_app t
haftmann@24219
   180
  of (IConst c, ts) => SOME (c, ts)
haftmann@24219
   181
   | _ => NONE;
haftmann@24219
   182
haftmann@24219
   183
fun fold_aiterms f (t as IConst _) = f t
haftmann@24219
   184
  | fold_aiterms f (t as IVar _) = f t
haftmann@24219
   185
  | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
haftmann@24219
   186
  | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
haftmann@24219
   187
  | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
haftmann@24219
   188
haftmann@24219
   189
fun fold_constnames f =
haftmann@24219
   190
  let
haftmann@24219
   191
    fun add (IConst (c, _)) = f c
haftmann@24219
   192
      | add _ = I;
haftmann@24219
   193
  in fold_aiterms add end;
haftmann@24219
   194
haftmann@24219
   195
fun fold_varnames f =
haftmann@24219
   196
  let
haftmann@24219
   197
    fun add (IVar v) = f v
haftmann@24219
   198
      | add ((v, _) `|-> _) = f v
haftmann@24219
   199
      | add _ = I;
haftmann@24219
   200
  in fold_aiterms add end;
haftmann@24219
   201
haftmann@24219
   202
fun fold_unbound_varnames f =
haftmann@24219
   203
  let
haftmann@24219
   204
    fun add _ (IConst _) = I
haftmann@24219
   205
      | add vs (IVar v) = if not (member (op =) vs v) then f v else I
haftmann@24219
   206
      | add vs (t1 `$ t2) = add vs t1 #> add vs t2
haftmann@24219
   207
      | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
haftmann@24219
   208
      | add vs (ICase (_, t)) = add vs t;
haftmann@24219
   209
  in add [] end;
haftmann@24219
   210
haftmann@24219
   211
fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
haftmann@24219
   212
      let
haftmann@24219
   213
        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
haftmann@24219
   214
          b orelse v = w) t false;
haftmann@24219
   215
      in if v = w andalso forall (fn (t1, t2) =>
haftmann@24219
   216
        exists_v t1 orelse not (exists_v t2)) ds
haftmann@24219
   217
        then ((se, ty), ds)
haftmann@24219
   218
        else ((se, ty), [(IVar v, be)])
haftmann@24219
   219
      end
haftmann@24219
   220
  | collapse_let (((v, ty), se), be) =
haftmann@24219
   221
      ((se, ty), [(IVar v, be)])
haftmann@24219
   222
haftmann@24219
   223
fun eta_expand (c as (_, (_, tys)), ts) k =
haftmann@24219
   224
  let
haftmann@24219
   225
    val j = length ts;
haftmann@24219
   226
    val l = k - j;
haftmann@24219
   227
    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
haftmann@24219
   228
    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
haftmann@24219
   229
  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
haftmann@24219
   230
haftmann@24219
   231
haftmann@24219
   232
(** definitions, transactions **)
haftmann@24219
   233
haftmann@24219
   234
(* type definitions *)
haftmann@24219
   235
haftmann@24219
   236
type typscheme = (vname * sort) list * itype;
haftmann@24219
   237
datatype def =
haftmann@24219
   238
    Bot
haftmann@24219
   239
  | Fun of (iterm list * iterm) list * typscheme
haftmann@24219
   240
  | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
   241
  | Datatypecons of string
haftmann@24219
   242
  | Class of (class * string) list * (vname * (string * itype) list)
haftmann@24219
   243
  | Classop of class
haftmann@24219
   244
  | Classrel of class * class
haftmann@24219
   245
  | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
   246
        * ((class * (string * (string * dict list list))) list
haftmann@24219
   247
      * (string * iterm) list);
haftmann@24219
   248
haftmann@24219
   249
type code = def Graph.T;
haftmann@24219
   250
type transact = Graph.key option * code;
haftmann@24219
   251
haftmann@24219
   252
haftmann@24219
   253
(* abstract code *)
haftmann@24219
   254
haftmann@24219
   255
val empty_code = Graph.empty : code; (*read: "depends on"*)
haftmann@24219
   256
haftmann@24219
   257
fun ensure_bot name = Graph.default_node (name, Bot);
haftmann@24219
   258
haftmann@24219
   259
fun add_def_incr (name, Bot) code =
haftmann@24219
   260
      (case the_default Bot (try (Graph.get_node code) name)
haftmann@24219
   261
       of Bot => error "Attempted to add Bot to code"
haftmann@24219
   262
        | _ => code)
haftmann@24219
   263
  | add_def_incr (name, def) code =
haftmann@24219
   264
      (case try (Graph.get_node code) name
haftmann@24219
   265
       of NONE => Graph.new_node (name, def) code
haftmann@24219
   266
        | SOME Bot => Graph.map_node name (K def) code
haftmann@24219
   267
        | SOME _ => error ("Tried to overwrite definition " ^ quote name));
haftmann@24219
   268
haftmann@24219
   269
fun add_dep (dep as (name1, name2)) =
haftmann@24219
   270
  if name1 = name2 then I else Graph.add_edge dep;
haftmann@24219
   271
haftmann@24219
   272
val merge_code : code * code -> code = Graph.merge (K true);
haftmann@24219
   273
haftmann@24219
   274
fun project_code delete_empty_funs hidden raw_selected code =
haftmann@24219
   275
  let
haftmann@24219
   276
    fun is_empty_fun name = case Graph.get_node code name
haftmann@24219
   277
     of Fun ([], _) => true
haftmann@24219
   278
      | _ => false;
haftmann@24219
   279
    val names = subtract (op =) hidden (Graph.keys code);
haftmann@24219
   280
    val deleted = Graph.all_preds code (filter is_empty_fun names);
haftmann@24219
   281
    val selected = case raw_selected
haftmann@24219
   282
     of NONE => names |> subtract (op =) deleted 
haftmann@24219
   283
      | SOME sel => sel
haftmann@24219
   284
          |> delete_empty_funs ? subtract (op =) deleted
haftmann@24219
   285
          |> subtract (op =) hidden
haftmann@24219
   286
          |> Graph.all_succs code
haftmann@24219
   287
          |> delete_empty_funs ? subtract (op =) deleted
haftmann@24219
   288
          |> subtract (op =) hidden;
haftmann@24219
   289
  in
haftmann@24219
   290
    code
haftmann@24219
   291
    |> Graph.subgraph (member (op =) selected)
haftmann@24219
   292
  end;
haftmann@24219
   293
haftmann@24219
   294
fun empty_funs code =
haftmann@24219
   295
  Graph.fold (fn (name, (Fun ([], _), _)) => cons name
haftmann@24219
   296
               | _ => I) code [];
haftmann@24219
   297
haftmann@24219
   298
fun is_cons code name = case Graph.get_node code name
haftmann@24219
   299
 of Datatypecons _ => true
haftmann@24219
   300
  | _ => false;
haftmann@24219
   301
haftmann@24219
   302
fun check_samemodule names =
haftmann@24219
   303
  fold (fn name =>
haftmann@24219
   304
    let
haftmann@24219
   305
      val module_name = (NameSpace.qualifier o NameSpace.qualifier) name
haftmann@24219
   306
    in
haftmann@24219
   307
     fn NONE => SOME module_name
haftmann@24219
   308
      | SOME module_name' => if module_name = module_name' then SOME module_name
haftmann@24219
   309
          else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
haftmann@24219
   310
    end
haftmann@24219
   311
  ) names NONE;
haftmann@24219
   312
haftmann@24219
   313
fun check_funeqs eqs =
haftmann@24219
   314
  (fold (fn (pats, _) =>
haftmann@24219
   315
    let
haftmann@24219
   316
      val l = length pats
haftmann@24219
   317
    in
haftmann@24219
   318
     fn NONE => SOME l
haftmann@24219
   319
      | SOME l' => if l = l' then SOME l
haftmann@24219
   320
          else error "Function definition with different number of arguments"
haftmann@24219
   321
    end
haftmann@24219
   322
  ) eqs NONE; eqs);
haftmann@24219
   323
haftmann@24219
   324
fun check_prep_def code Bot =
haftmann@24219
   325
      Bot
haftmann@24219
   326
  | check_prep_def code (Fun (eqs, d)) =
haftmann@24219
   327
      Fun (check_funeqs eqs, d)
haftmann@24219
   328
  | check_prep_def code (d as Datatype _) =
haftmann@24219
   329
      d
haftmann@24219
   330
  | check_prep_def code (Datatypecons dtco) =
haftmann@24219
   331
      error "Attempted to add bare term constructor"
haftmann@24219
   332
  | check_prep_def code (d as Class _) =
haftmann@24219
   333
      d
haftmann@24219
   334
  | check_prep_def code (Classop _) =
haftmann@24219
   335
      error "Attempted to add bare class operation"
haftmann@24219
   336
  | check_prep_def code (Classrel _) =
haftmann@24219
   337
      error "Attempted to add bare class relation"
haftmann@24219
   338
  | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
haftmann@24219
   339
      let
haftmann@24219
   340
        val Class (_, (_, classops)) = Graph.get_node code class;
haftmann@24219
   341
        val _ = if length inst_classops > length classops
haftmann@24219
   342
          then error "Too many class operations given"
haftmann@24219
   343
          else ();
haftmann@24219
   344
        fun check_classop (f, _) =
haftmann@24219
   345
          if AList.defined (op =) inst_classops f
haftmann@24219
   346
          then () else error ("Missing definition for class operation " ^ quote f);
haftmann@24219
   347
        val _ = map check_classop classops;
haftmann@24219
   348
      in d end;
haftmann@24219
   349
haftmann@24219
   350
fun postprocess_def (name, Datatype (_, constrs)) =
haftmann@24219
   351
      tap (fn _ => check_samemodule (name :: map fst constrs))
haftmann@24219
   352
      #> fold (fn (co, _) =>
haftmann@24219
   353
        add_def_incr (co, Datatypecons name)
haftmann@24219
   354
        #> add_dep (co, name)
haftmann@24219
   355
        #> add_dep (name, co)
haftmann@24219
   356
      ) constrs
haftmann@24219
   357
  | postprocess_def (name, Class (classrels, (_, classops))) =
haftmann@24219
   358
      tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
haftmann@24219
   359
      #> fold (fn (f, _) =>
haftmann@24219
   360
        add_def_incr (f, Classop name)
haftmann@24219
   361
        #> add_dep (f, name)
haftmann@24219
   362
        #> add_dep (name, f)
haftmann@24219
   363
      ) classops
haftmann@24219
   364
      #> fold (fn (superclass, classrel) =>
haftmann@24219
   365
        add_def_incr (classrel, Classrel (name, superclass))
haftmann@24219
   366
        #> add_dep (classrel, name)
haftmann@24219
   367
        #> add_dep (name, classrel)
haftmann@24219
   368
      ) classrels
haftmann@24219
   369
  | postprocess_def _ =
haftmann@24219
   370
      I;
haftmann@24219
   371
haftmann@24219
   372
haftmann@24219
   373
(* transaction protocol *)
haftmann@24219
   374
haftmann@24219
   375
fun ensure_def labelled_name defgen msg name (dep, code) =
haftmann@24219
   376
  let
haftmann@24219
   377
    val msg' = (case dep
haftmann@24219
   378
     of NONE => msg
haftmann@24219
   379
      | SOME dep => msg ^ ", required for " ^ labelled_name dep);
haftmann@24219
   380
    fun add_dp NONE = I
haftmann@24219
   381
      | add_dp (SOME dep) = add_dep (dep, name);
haftmann@24219
   382
    fun prep_def def code =
haftmann@24219
   383
      (check_prep_def code def, code);
haftmann@24219
   384
    fun add_def false =
haftmann@24219
   385
          ensure_bot name
haftmann@24219
   386
          #> add_dp dep
haftmann@24252
   387
          #> curry defgen (SOME name)
haftmann@24252
   388
          ##> snd
haftmann@24219
   389
          #-> (fn def => prep_def def)
haftmann@24219
   390
          #-> (fn def => add_def_incr (name, def)
haftmann@24219
   391
          #> postprocess_def (name, def))
haftmann@24219
   392
      | add_def true =
haftmann@24219
   393
          add_dp dep;
haftmann@24219
   394
  in
haftmann@24219
   395
    code
haftmann@24219
   396
    |> add_def (can (Graph.get_node code) name)
haftmann@24219
   397
    |> pair dep
haftmann@24219
   398
  end;
haftmann@24219
   399
haftmann@24219
   400
fun start_transact f code =
haftmann@24252
   401
  (NONE, code)
haftmann@24252
   402
  |> f
haftmann@24252
   403
  |-> (fn x => fn (_, code) => (x, code));
haftmann@24219
   404
haftmann@24219
   405
fun add_eval_def (name, t) code =
haftmann@24219
   406
  code
haftmann@24219
   407
  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
haftmann@24219
   408
  |> fold (curry Graph.add_edge name) (Graph.keys code);
haftmann@24219
   409
haftmann@24219
   410
end; (*struct*)
haftmann@24219
   411
haftmann@24219
   412
haftmann@24219
   413
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;