src/Tools/code/code_thingol.ML
author haftmann
Sat Sep 15 19:27:50 2007 +0200 (2007-09-15)
changeset 24591 6509626eb2c9
parent 24381 560e8ecdf633
child 24662 f79f6061525c
permissions -rw-r--r--
added explicit theorems
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@24591
    25
  type const = string * (dict list list * itype list (*types of arguments*))
haftmann@24219
    26
  datatype iterm =
haftmann@24591
    27
      IConst of const
haftmann@24219
    28
    | IVar of vname
haftmann@24219
    29
    | `$ of iterm * iterm
haftmann@24219
    30
    | `|-> of (vname * itype) * iterm
haftmann@24219
    31
    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@24219
    32
        (*((term, type), [(selector pattern, body term )]), primitive term)*)
haftmann@24219
    33
  val `-> : itype * itype -> itype;
haftmann@24219
    34
  val `--> : itype list * itype -> itype;
haftmann@24219
    35
  val `$$ : iterm * iterm list -> iterm;
haftmann@24219
    36
  val `|--> : (vname * itype) list * iterm -> iterm;
haftmann@24219
    37
  type typscheme = (vname * sort) list * itype;
haftmann@24219
    38
end;
haftmann@24219
    39
haftmann@24219
    40
signature CODE_THINGOL =
haftmann@24219
    41
sig
haftmann@24219
    42
  include BASIC_CODE_THINGOL;
haftmann@24219
    43
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
haftmann@24219
    44
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
haftmann@24219
    45
  val unfold_fun: itype -> itype list * itype;
haftmann@24219
    46
  val unfold_app: iterm -> iterm * iterm list;
haftmann@24219
    47
  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
haftmann@24219
    48
  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
haftmann@24219
    49
  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
haftmann@24219
    50
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
haftmann@24219
    51
  val unfold_const_app: iterm ->
haftmann@24219
    52
    ((string * (dict list list * itype list)) * iterm list) option;
haftmann@24219
    53
  val collapse_let: ((vname * itype) * iterm) * iterm
haftmann@24219
    54
    -> (iterm * itype) * (iterm * iterm) list;
haftmann@24219
    55
  val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
haftmann@24219
    56
  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    57
  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    58
  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    59
haftmann@24219
    60
  datatype def =
haftmann@24219
    61
      Bot
haftmann@24591
    62
    | Fun of typscheme * ((iterm list * iterm) * thm) list
haftmann@24219
    63
    | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
    64
    | Datatypecons of string
haftmann@24219
    65
    | Class of (class * string) list * (vname * (string * itype) list)
haftmann@24219
    66
    | Classop of class
haftmann@24219
    67
    | Classrel of class * class
haftmann@24219
    68
    | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
    69
          * ((class * (string * (string * dict list list))) list
haftmann@24591
    70
        * ((string * const) * thm) list);
haftmann@24219
    71
  type code = def Graph.T;
haftmann@24219
    72
  type transact;
haftmann@24219
    73
  val empty_code: code;
haftmann@24219
    74
  val merge_code: code * code -> code;
haftmann@24219
    75
  val project_code: bool (*delete empty funs*)
haftmann@24219
    76
    -> string list (*hidden*) -> string list option (*selected*)
haftmann@24219
    77
    -> code -> code;
haftmann@24219
    78
  val empty_funs: code -> string list;
haftmann@24219
    79
  val is_cons: code -> string -> bool;
haftmann@24283
    80
  val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
haftmann@24219
    81
haftmann@24252
    82
  val ensure_def: (string -> string) -> (transact -> def * transact) -> string
haftmann@24219
    83
    -> string -> transact -> transact;
haftmann@24219
    84
  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
haftmann@24219
    85
end;
haftmann@24219
    86
haftmann@24219
    87
structure CodeThingol: CODE_THINGOL =
haftmann@24219
    88
struct
haftmann@24219
    89
haftmann@24219
    90
(** auxiliary **)
haftmann@24219
    91
haftmann@24219
    92
fun unfoldl dest x =
haftmann@24219
    93
  case dest x
haftmann@24219
    94
   of NONE => (x, [])
haftmann@24219
    95
    | SOME (x1, x2) =>
haftmann@24219
    96
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
haftmann@24219
    97
haftmann@24219
    98
fun unfoldr dest x =
haftmann@24219
    99
  case dest x
haftmann@24219
   100
   of NONE => ([], x)
haftmann@24219
   101
    | SOME (x1, x2) =>
haftmann@24219
   102
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
haftmann@24219
   103
haftmann@24219
   104
haftmann@24219
   105
(** language core - types, pattern, expressions **)
haftmann@24219
   106
haftmann@24219
   107
(* language representation *)
haftmann@24219
   108
haftmann@24219
   109
type vname = string;
haftmann@24219
   110
haftmann@24219
   111
datatype dict =
haftmann@24219
   112
    DictConst of string * dict list list
haftmann@24219
   113
  | DictVar of string list * (vname * (int * int));
haftmann@24219
   114
haftmann@24219
   115
datatype itype =
haftmann@24219
   116
    `%% of string * itype list
haftmann@24219
   117
  | ITyVar of vname;
haftmann@24219
   118
haftmann@24591
   119
type const = string * (dict list list * itype list (*types of arguments*))
haftmann@24591
   120
haftmann@24219
   121
datatype iterm =
haftmann@24591
   122
    IConst of const
haftmann@24219
   123
  | IVar of vname
haftmann@24219
   124
  | `$ of iterm * iterm
haftmann@24219
   125
  | `|-> of (vname * itype) * iterm
haftmann@24219
   126
  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@24219
   127
    (*see also signature*)
haftmann@24219
   128
haftmann@24219
   129
(*
haftmann@24219
   130
  variable naming conventions
haftmann@24219
   131
haftmann@24219
   132
  bare names:
haftmann@24219
   133
    variable names          v
haftmann@24219
   134
    class names             class
haftmann@24219
   135
    type constructor names  tyco
haftmann@24219
   136
    datatype names          dtco
haftmann@24219
   137
    const names (general)   c
haftmann@24219
   138
    constructor names       co
haftmann@24219
   139
    class operation names   clsop (op)
haftmann@24219
   140
    arbitrary name          s
haftmann@24219
   141
haftmann@24219
   142
    v, c, co, clsop also annotated with types etc.
haftmann@24219
   143
haftmann@24219
   144
  constructs:
haftmann@24219
   145
    sort                    sort
haftmann@24219
   146
    type parameters         vs
haftmann@24219
   147
    type                    ty
haftmann@24219
   148
    type schemes            tysm
haftmann@24219
   149
    term                    t
haftmann@24219
   150
    (term as pattern)       p
haftmann@24219
   151
    instance (class, tyco)  inst
haftmann@24219
   152
 *)
haftmann@24219
   153
haftmann@24219
   154
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
haftmann@24219
   155
val op `--> = Library.foldr (op `->);
haftmann@24219
   156
val op `$$ = Library.foldl (op `$);
haftmann@24219
   157
val op `|--> = Library.foldr (op `|->);
haftmann@24219
   158
haftmann@24219
   159
val unfold_fun = unfoldr
haftmann@24219
   160
  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
haftmann@24219
   161
    | _ => NONE);
haftmann@24219
   162
haftmann@24219
   163
val unfold_app = unfoldl
haftmann@24219
   164
  (fn op `$ t => SOME t
haftmann@24219
   165
    | _ => NONE);
haftmann@24219
   166
haftmann@24219
   167
val split_abs =
haftmann@24219
   168
  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
haftmann@24219
   169
        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
haftmann@24219
   170
    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
haftmann@24219
   171
    | _ => NONE);
haftmann@24219
   172
haftmann@24219
   173
val unfold_abs = unfoldr split_abs;
haftmann@24219
   174
haftmann@24219
   175
val split_let = 
haftmann@24219
   176
  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
haftmann@24219
   177
    | _ => NONE);
haftmann@24219
   178
haftmann@24219
   179
val unfold_let = unfoldr split_let;
haftmann@24219
   180
haftmann@24219
   181
fun unfold_const_app t =
haftmann@24219
   182
 case unfold_app t
haftmann@24219
   183
  of (IConst c, ts) => SOME (c, ts)
haftmann@24219
   184
   | _ => NONE;
haftmann@24219
   185
haftmann@24219
   186
fun fold_aiterms f (t as IConst _) = f t
haftmann@24219
   187
  | fold_aiterms f (t as IVar _) = f t
haftmann@24219
   188
  | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
haftmann@24219
   189
  | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
haftmann@24219
   190
  | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
haftmann@24219
   191
haftmann@24219
   192
fun fold_constnames f =
haftmann@24219
   193
  let
haftmann@24219
   194
    fun add (IConst (c, _)) = f c
haftmann@24219
   195
      | add _ = I;
haftmann@24219
   196
  in fold_aiterms add end;
haftmann@24219
   197
haftmann@24219
   198
fun fold_varnames f =
haftmann@24219
   199
  let
haftmann@24219
   200
    fun add (IVar v) = f v
haftmann@24219
   201
      | add ((v, _) `|-> _) = f v
haftmann@24219
   202
      | add _ = I;
haftmann@24219
   203
  in fold_aiterms add end;
haftmann@24219
   204
haftmann@24219
   205
fun fold_unbound_varnames f =
haftmann@24219
   206
  let
haftmann@24219
   207
    fun add _ (IConst _) = I
haftmann@24219
   208
      | add vs (IVar v) = if not (member (op =) vs v) then f v else I
haftmann@24219
   209
      | add vs (t1 `$ t2) = add vs t1 #> add vs t2
haftmann@24219
   210
      | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
haftmann@24219
   211
      | add vs (ICase (_, t)) = add vs t;
haftmann@24219
   212
  in add [] end;
haftmann@24219
   213
haftmann@24219
   214
fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
haftmann@24219
   215
      let
haftmann@24219
   216
        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
haftmann@24219
   217
          b orelse v = w) t false;
haftmann@24219
   218
      in if v = w andalso forall (fn (t1, t2) =>
haftmann@24219
   219
        exists_v t1 orelse not (exists_v t2)) ds
haftmann@24219
   220
        then ((se, ty), ds)
haftmann@24219
   221
        else ((se, ty), [(IVar v, be)])
haftmann@24219
   222
      end
haftmann@24219
   223
  | collapse_let (((v, ty), se), be) =
haftmann@24219
   224
      ((se, ty), [(IVar v, be)])
haftmann@24219
   225
haftmann@24219
   226
fun eta_expand (c as (_, (_, tys)), ts) k =
haftmann@24219
   227
  let
haftmann@24219
   228
    val j = length ts;
haftmann@24219
   229
    val l = k - j;
haftmann@24219
   230
    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
haftmann@24219
   231
    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
haftmann@24219
   232
  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
haftmann@24219
   233
haftmann@24219
   234
haftmann@24219
   235
(** definitions, transactions **)
haftmann@24219
   236
haftmann@24219
   237
type typscheme = (vname * sort) list * itype;
haftmann@24219
   238
datatype def =
haftmann@24219
   239
    Bot
haftmann@24591
   240
  | Fun of typscheme * ((iterm list * iterm) * thm) list
haftmann@24219
   241
  | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
   242
  | Datatypecons of string
haftmann@24219
   243
  | Class of (class * string) list * (vname * (string * itype) list)
haftmann@24219
   244
  | Classop of class
haftmann@24219
   245
  | Classrel of class * class
haftmann@24219
   246
  | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
   247
        * ((class * (string * (string * dict list list))) list
haftmann@24591
   248
      * ((string * const) * thm) list);
haftmann@24219
   249
haftmann@24219
   250
type code = def Graph.T;
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@24381
   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@24381
   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@24591
   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@24381
   326
  | check_prep_def code (Fun (d, eqs)) =
haftmann@24381
   327
      Fun (d, check_funeqs eqs)
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@24591
   345
          if AList.defined (op =) (map fst 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@24283
   375
type transact = Graph.key option * code;
haftmann@24283
   376
haftmann@24219
   377
fun ensure_def labelled_name defgen msg name (dep, code) =
haftmann@24219
   378
  let
haftmann@24219
   379
    val msg' = (case dep
haftmann@24219
   380
     of NONE => msg
haftmann@24219
   381
      | SOME dep => msg ^ ", required for " ^ labelled_name dep);
haftmann@24219
   382
    fun add_dp NONE = I
haftmann@24219
   383
      | add_dp (SOME dep) = add_dep (dep, name);
haftmann@24219
   384
    fun prep_def def code =
haftmann@24219
   385
      (check_prep_def code def, code);
haftmann@24219
   386
    fun add_def false =
haftmann@24219
   387
          ensure_bot name
haftmann@24219
   388
          #> add_dp dep
haftmann@24252
   389
          #> curry defgen (SOME name)
haftmann@24252
   390
          ##> snd
haftmann@24219
   391
          #-> (fn def => prep_def def)
haftmann@24219
   392
          #-> (fn def => add_def_incr (name, def)
haftmann@24219
   393
          #> postprocess_def (name, def))
haftmann@24219
   394
      | add_def true =
haftmann@24219
   395
          add_dp dep;
haftmann@24219
   396
  in
haftmann@24219
   397
    code
haftmann@24219
   398
    |> add_def (can (Graph.get_node code) name)
haftmann@24219
   399
    |> pair dep
haftmann@24219
   400
  end;
haftmann@24219
   401
haftmann@24219
   402
fun start_transact f code =
haftmann@24252
   403
  (NONE, code)
haftmann@24252
   404
  |> f
haftmann@24252
   405
  |-> (fn x => fn (_, code) => (x, code));
haftmann@24219
   406
haftmann@24283
   407
fun add_eval_def (name, (t, ty)) code =
haftmann@24219
   408
  code
haftmann@24591
   409
  |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
haftmann@24219
   410
  |> fold (curry Graph.add_edge name) (Graph.keys code);
haftmann@24219
   411
haftmann@24219
   412
end; (*struct*)
haftmann@24219
   413
haftmann@24219
   414
haftmann@24219
   415
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;