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