src/Tools/code/code_thingol.ML
author haftmann
Fri Aug 10 17:04:34 2007 +0200 (2007-08-10)
changeset 24219 e558fe311376
child 24252 4eb5bc6af008
permissions -rw-r--r--
new structure for code generator modules
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@24219
    81
  val ensure_def: (string -> string) -> (transact -> def * code) -> string
haftmann@24219
    82
    -> string -> transact -> transact;
haftmann@24219
    83
  val succeed: 'a -> transact -> 'a * code;
haftmann@24219
    84
  val fail: string -> transact -> 'a * code;
haftmann@24219
    85
  val message: string -> (transact -> 'a) -> transact -> 'a;
haftmann@24219
    86
  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
haftmann@24219
    87
end;
haftmann@24219
    88
haftmann@24219
    89
structure CodeThingol: CODE_THINGOL =
haftmann@24219
    90
struct
haftmann@24219
    91
haftmann@24219
    92
(** auxiliary **)
haftmann@24219
    93
haftmann@24219
    94
fun unfoldl dest x =
haftmann@24219
    95
  case dest x
haftmann@24219
    96
   of NONE => (x, [])
haftmann@24219
    97
    | SOME (x1, x2) =>
haftmann@24219
    98
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
haftmann@24219
    99
haftmann@24219
   100
fun unfoldr dest x =
haftmann@24219
   101
  case dest x
haftmann@24219
   102
   of NONE => ([], x)
haftmann@24219
   103
    | SOME (x1, x2) =>
haftmann@24219
   104
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
haftmann@24219
   105
haftmann@24219
   106
haftmann@24219
   107
(** language core - types, pattern, expressions **)
haftmann@24219
   108
haftmann@24219
   109
(* language representation *)
haftmann@24219
   110
haftmann@24219
   111
type vname = string;
haftmann@24219
   112
haftmann@24219
   113
datatype dict =
haftmann@24219
   114
    DictConst of string * dict list list
haftmann@24219
   115
  | DictVar of string list * (vname * (int * int));
haftmann@24219
   116
haftmann@24219
   117
datatype itype =
haftmann@24219
   118
    `%% of string * itype list
haftmann@24219
   119
  | ITyVar of vname;
haftmann@24219
   120
haftmann@24219
   121
datatype iterm =
haftmann@24219
   122
    IConst of string * (dict list list * itype list)
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 definitions *)
haftmann@24219
   238
haftmann@24219
   239
type typscheme = (vname * sort) list * itype;
haftmann@24219
   240
datatype def =
haftmann@24219
   241
    Bot
haftmann@24219
   242
  | Fun of (iterm list * iterm) list * typscheme
haftmann@24219
   243
  | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
   244
  | Datatypecons of string
haftmann@24219
   245
  | Class of (class * string) list * (vname * (string * itype) list)
haftmann@24219
   246
  | Classop of class
haftmann@24219
   247
  | Classrel of class * class
haftmann@24219
   248
  | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
   249
        * ((class * (string * (string * dict list list))) list
haftmann@24219
   250
      * (string * iterm) list);
haftmann@24219
   251
haftmann@24219
   252
type code = def Graph.T;
haftmann@24219
   253
type transact = Graph.key option * code;
haftmann@24219
   254
exception FAIL of string list;
haftmann@24219
   255
haftmann@24219
   256
haftmann@24219
   257
(* abstract code *)
haftmann@24219
   258
haftmann@24219
   259
val empty_code = Graph.empty : code; (*read: "depends on"*)
haftmann@24219
   260
haftmann@24219
   261
fun ensure_bot name = Graph.default_node (name, Bot);
haftmann@24219
   262
haftmann@24219
   263
fun add_def_incr (name, Bot) code =
haftmann@24219
   264
      (case the_default Bot (try (Graph.get_node code) name)
haftmann@24219
   265
       of Bot => error "Attempted to add Bot to code"
haftmann@24219
   266
        | _ => code)
haftmann@24219
   267
  | add_def_incr (name, def) code =
haftmann@24219
   268
      (case try (Graph.get_node code) name
haftmann@24219
   269
       of NONE => Graph.new_node (name, def) code
haftmann@24219
   270
        | SOME Bot => Graph.map_node name (K def) code
haftmann@24219
   271
        | SOME _ => error ("Tried to overwrite definition " ^ quote name));
haftmann@24219
   272
haftmann@24219
   273
fun add_dep (dep as (name1, name2)) =
haftmann@24219
   274
  if name1 = name2 then I else Graph.add_edge dep;
haftmann@24219
   275
haftmann@24219
   276
val merge_code : code * code -> code = Graph.merge (K true);
haftmann@24219
   277
haftmann@24219
   278
fun project_code delete_empty_funs hidden raw_selected code =
haftmann@24219
   279
  let
haftmann@24219
   280
    fun is_empty_fun name = case Graph.get_node code name
haftmann@24219
   281
     of Fun ([], _) => true
haftmann@24219
   282
      | _ => false;
haftmann@24219
   283
    val names = subtract (op =) hidden (Graph.keys code);
haftmann@24219
   284
    val deleted = Graph.all_preds code (filter is_empty_fun names);
haftmann@24219
   285
    val selected = case raw_selected
haftmann@24219
   286
     of NONE => names |> subtract (op =) deleted 
haftmann@24219
   287
      | SOME sel => sel
haftmann@24219
   288
          |> delete_empty_funs ? subtract (op =) deleted
haftmann@24219
   289
          |> subtract (op =) hidden
haftmann@24219
   290
          |> Graph.all_succs code
haftmann@24219
   291
          |> delete_empty_funs ? subtract (op =) deleted
haftmann@24219
   292
          |> subtract (op =) hidden;
haftmann@24219
   293
  in
haftmann@24219
   294
    code
haftmann@24219
   295
    |> Graph.subgraph (member (op =) selected)
haftmann@24219
   296
  end;
haftmann@24219
   297
haftmann@24219
   298
fun empty_funs code =
haftmann@24219
   299
  Graph.fold (fn (name, (Fun ([], _), _)) => cons name
haftmann@24219
   300
               | _ => I) code [];
haftmann@24219
   301
haftmann@24219
   302
fun is_cons code name = case Graph.get_node code name
haftmann@24219
   303
 of Datatypecons _ => true
haftmann@24219
   304
  | _ => false;
haftmann@24219
   305
haftmann@24219
   306
fun check_samemodule names =
haftmann@24219
   307
  fold (fn name =>
haftmann@24219
   308
    let
haftmann@24219
   309
      val module_name = (NameSpace.qualifier o NameSpace.qualifier) name
haftmann@24219
   310
    in
haftmann@24219
   311
     fn NONE => SOME module_name
haftmann@24219
   312
      | SOME module_name' => if module_name = module_name' then SOME module_name
haftmann@24219
   313
          else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
haftmann@24219
   314
    end
haftmann@24219
   315
  ) names NONE;
haftmann@24219
   316
haftmann@24219
   317
fun check_funeqs eqs =
haftmann@24219
   318
  (fold (fn (pats, _) =>
haftmann@24219
   319
    let
haftmann@24219
   320
      val l = length pats
haftmann@24219
   321
    in
haftmann@24219
   322
     fn NONE => SOME l
haftmann@24219
   323
      | SOME l' => if l = l' then SOME l
haftmann@24219
   324
          else error "Function definition with different number of arguments"
haftmann@24219
   325
    end
haftmann@24219
   326
  ) eqs NONE; eqs);
haftmann@24219
   327
haftmann@24219
   328
fun check_prep_def code Bot =
haftmann@24219
   329
      Bot
haftmann@24219
   330
  | check_prep_def code (Fun (eqs, d)) =
haftmann@24219
   331
      Fun (check_funeqs eqs, d)
haftmann@24219
   332
  | check_prep_def code (d as Datatype _) =
haftmann@24219
   333
      d
haftmann@24219
   334
  | check_prep_def code (Datatypecons dtco) =
haftmann@24219
   335
      error "Attempted to add bare term constructor"
haftmann@24219
   336
  | check_prep_def code (d as Class _) =
haftmann@24219
   337
      d
haftmann@24219
   338
  | check_prep_def code (Classop _) =
haftmann@24219
   339
      error "Attempted to add bare class operation"
haftmann@24219
   340
  | check_prep_def code (Classrel _) =
haftmann@24219
   341
      error "Attempted to add bare class relation"
haftmann@24219
   342
  | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
haftmann@24219
   343
      let
haftmann@24219
   344
        val Class (_, (_, classops)) = Graph.get_node code class;
haftmann@24219
   345
        val _ = if length inst_classops > length classops
haftmann@24219
   346
          then error "Too many class operations given"
haftmann@24219
   347
          else ();
haftmann@24219
   348
        fun check_classop (f, _) =
haftmann@24219
   349
          if AList.defined (op =) inst_classops f
haftmann@24219
   350
          then () else error ("Missing definition for class operation " ^ quote f);
haftmann@24219
   351
        val _ = map check_classop classops;
haftmann@24219
   352
      in d end;
haftmann@24219
   353
haftmann@24219
   354
fun postprocess_def (name, Datatype (_, constrs)) =
haftmann@24219
   355
      tap (fn _ => check_samemodule (name :: map fst constrs))
haftmann@24219
   356
      #> fold (fn (co, _) =>
haftmann@24219
   357
        add_def_incr (co, Datatypecons name)
haftmann@24219
   358
        #> add_dep (co, name)
haftmann@24219
   359
        #> add_dep (name, co)
haftmann@24219
   360
      ) constrs
haftmann@24219
   361
  | postprocess_def (name, Class (classrels, (_, classops))) =
haftmann@24219
   362
      tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
haftmann@24219
   363
      #> fold (fn (f, _) =>
haftmann@24219
   364
        add_def_incr (f, Classop name)
haftmann@24219
   365
        #> add_dep (f, name)
haftmann@24219
   366
        #> add_dep (name, f)
haftmann@24219
   367
      ) classops
haftmann@24219
   368
      #> fold (fn (superclass, classrel) =>
haftmann@24219
   369
        add_def_incr (classrel, Classrel (name, superclass))
haftmann@24219
   370
        #> add_dep (classrel, name)
haftmann@24219
   371
        #> add_dep (name, classrel)
haftmann@24219
   372
      ) classrels
haftmann@24219
   373
  | postprocess_def _ =
haftmann@24219
   374
      I;
haftmann@24219
   375
haftmann@24219
   376
haftmann@24219
   377
(* transaction protocol *)
haftmann@24219
   378
haftmann@24219
   379
fun ensure_def labelled_name defgen msg name (dep, code) =
haftmann@24219
   380
  let
haftmann@24219
   381
    val msg' = (case dep
haftmann@24219
   382
     of NONE => msg
haftmann@24219
   383
      | SOME dep => msg ^ ", required for " ^ labelled_name dep);
haftmann@24219
   384
    fun add_dp NONE = I
haftmann@24219
   385
      | add_dp (SOME dep) = add_dep (dep, name);
haftmann@24219
   386
    fun prep_def def code =
haftmann@24219
   387
      (check_prep_def code def, code);
haftmann@24219
   388
    fun invoke_generator name defgen code =
haftmann@24219
   389
      defgen (SOME name, code) handle FAIL msgs => raise FAIL (msg' :: msgs);
haftmann@24219
   390
    fun add_def false =
haftmann@24219
   391
          ensure_bot name
haftmann@24219
   392
          #> add_dp dep
haftmann@24219
   393
          #> invoke_generator name defgen
haftmann@24219
   394
          #-> (fn def => prep_def def)
haftmann@24219
   395
          #-> (fn def => add_def_incr (name, def)
haftmann@24219
   396
          #> postprocess_def (name, def))
haftmann@24219
   397
      | add_def true =
haftmann@24219
   398
          add_dp dep;
haftmann@24219
   399
  in
haftmann@24219
   400
    code
haftmann@24219
   401
    |> add_def (can (Graph.get_node code) name)
haftmann@24219
   402
    |> pair dep
haftmann@24219
   403
  end;
haftmann@24219
   404
haftmann@24219
   405
fun succeed some (_, code) = (some, code);
haftmann@24219
   406
haftmann@24219
   407
fun fail msg (_, code) = raise FAIL [msg];
haftmann@24219
   408
haftmann@24219
   409
fun message msg f trns =
haftmann@24219
   410
  f trns handle FAIL msgs =>
haftmann@24219
   411
    raise FAIL (msg :: msgs);
haftmann@24219
   412
haftmann@24219
   413
fun start_transact f code =
haftmann@24219
   414
  let
haftmann@24219
   415
    fun handle_fail f x =
haftmann@24219
   416
      (f x
haftmann@24219
   417
      handle FAIL msgs =>
haftmann@24219
   418
        (error o cat_lines) ("Code generation failed, while:" :: msgs))
haftmann@24219
   419
  in
haftmann@24219
   420
    (NONE, code)
haftmann@24219
   421
    |> handle_fail f
haftmann@24219
   422
    |-> (fn x => fn (_, code) => (x, code))
haftmann@24219
   423
  end;
haftmann@24219
   424
haftmann@24219
   425
fun add_eval_def (name, t) code =
haftmann@24219
   426
  code
haftmann@24219
   427
  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
haftmann@24219
   428
  |> fold (curry Graph.add_edge name) (Graph.keys code);
haftmann@24219
   429
haftmann@24219
   430
end; (*struct*)
haftmann@24219
   431
haftmann@24219
   432
haftmann@24219
   433
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;