src/Pure/Tools/codegen_thingol.ML
author haftmann
Thu, 28 Jun 2007 19:09:41 +0200
changeset 23516 f7d54060b5b0
parent 23028 d8c4a02e992a
child 23691 cedf9610b71d
permissions -rw-r--r--
proper collapse_let
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
     1
(*  Title:      Pure/Tools/codegen_thingol.ML
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     2
    ID:         $Id$
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     4
23028
d8c4a02e992a fixed comment
haftmann
parents: 22799
diff changeset
     5
Intermediate language ("Thin-gol") representing executable code.
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     6
*)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
     7
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
     8
infix 8 `%%;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
     9
infixr 6 `->;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    10
infixr 6 `-->;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    11
infix 4 `$;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    12
infix 4 `$$;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    13
infixr 3 `|->;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    14
infixr 3 `|-->;
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    15
19136
00ade10f611d some refinements
haftmann
parents: 19042
diff changeset
    16
signature BASIC_CODEGEN_THINGOL =
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    17
sig
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    18
  type vname = string;
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
    19
  datatype dict =
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
    20
      DictConst of string * dict list list
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
    21
    | DictVar of string list * (vname * (int * int));
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    22
  datatype itype =
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    23
      `%% of string * itype list
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    24
    | ITyVar of vname;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
    25
  datatype iterm =
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
    26
      IConst of string * (dict list list * itype list (*types of arguments*))
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
    27
    | IVar of vname
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
    28
    | `$ of iterm * iterm
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
    29
    | `|-> of (vname * itype) * iterm
21012
haftmann
parents: 20976
diff changeset
    30
    | ICase of (iterm * itype) * (iterm * iterm) list;
haftmann
parents: 20976
diff changeset
    31
        (*(discriminendum term (td), discriminendum type (ty)),
haftmann
parents: 20976
diff changeset
    32
                [(selector pattern (p), body term (t))] (bs))*)
21123
9f7c430cf9ac dropped constructiv `->
haftmann
parents: 21082
diff changeset
    33
  val `-> : itype * itype -> itype;
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    34
  val `--> : itype list * itype -> itype;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    35
  val `$$ : iterm * iterm list -> iterm;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    36
  val `|--> : (vname * itype) list * iterm -> iterm;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    37
  type typscheme = (vname * sort) list * itype;
19136
00ade10f611d some refinements
haftmann
parents: 19042
diff changeset
    38
end;
00ade10f611d some refinements
haftmann
parents: 19042
diff changeset
    39
00ade10f611d some refinements
haftmann
parents: 19042
diff changeset
    40
signature CODEGEN_THINGOL =
00ade10f611d some refinements
haftmann
parents: 19042
diff changeset
    41
sig
00ade10f611d some refinements
haftmann
parents: 19042
diff changeset
    42
  include BASIC_CODEGEN_THINGOL;
18216
db7d43b25c99 added serializer
haftmann
parents: 18172
diff changeset
    43
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
db7d43b25c99 added serializer
haftmann
parents: 18172
diff changeset
    44
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    45
  val unfold_fun: itype -> itype list * itype;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
    46
  val unfold_app: iterm -> iterm * iterm list;
22062
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
    47
  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
21012
haftmann
parents: 20976
diff changeset
    48
  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
22062
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
    49
  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
    50
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
    51
  val unfold_const_app: iterm ->
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
    52
    ((string * (dict list list * itype list)) * iterm list) option;
23516
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
    53
  val collapse_let: ((vname * itype) * iterm) * iterm -> iterm;
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
    54
  val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    55
  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    56
  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    57
  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
    58
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
    59
  datatype def =
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
    60
      Bot
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
    61
    | Fun of (iterm list * iterm) list * typscheme
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
    62
    | Datatype of (vname * sort) list * (string * itype list) list
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
    63
    | Datatypecons of string
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
    64
    | Class of (class * string) list * (vname * (string * itype) list)
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
    65
    | Classop of class
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
    66
    | Classrel of class * class
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
    67
    | Classinst of (class * (string * (vname * sort) list))
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
    68
          * ((class * (string * (string * dict list list))) list
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
    69
        * (string * iterm) list);
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    70
  type code = def Graph.T;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
    71
  type transact;
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    72
  val empty_code: code;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    73
  val get_def: code -> string -> def;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    74
  val merge_code: code * code -> code;
21012
haftmann
parents: 20976
diff changeset
    75
  val project_code: string list (*hidden*) -> string list option (*selected*)
haftmann
parents: 20976
diff changeset
    76
    -> code -> code;
21160
haftmann
parents: 21123
diff changeset
    77
  val add_eval_def: string (*bind name*) * iterm -> code -> code;
21012
haftmann
parents: 20976
diff changeset
    78
22037
fbf0a12d053f proper node names
haftmann
parents: 21937
diff changeset
    79
  val ensure_def: (string -> string) -> (transact -> def * code) -> bool -> string
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    80
    -> string -> transact -> transact;
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    81
  val succeed: 'a -> transact -> 'a * code;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
    82
  val fail: string -> transact -> 'a * code;
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
    83
  val message: string -> (transact -> 'a) -> transact -> 'a;
22185
haftmann
parents: 22076
diff changeset
    84
  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
18216
db7d43b25c99 added serializer
haftmann
parents: 18172
diff changeset
    85
20835
haftmann
parents: 20709
diff changeset
    86
  val trace: bool ref;
haftmann
parents: 20709
diff changeset
    87
  val tracing: ('a -> string) -> 'a -> 'a;
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    88
end;
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    89
18850
92ef83e5eaea various improvements
haftmann
parents: 18812
diff changeset
    90
structure CodegenThingol: CODEGEN_THINGOL =
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    91
struct
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    92
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
    93
(** auxiliary **)
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    94
20835
haftmann
parents: 20709
diff changeset
    95
val trace = ref false;
haftmann
parents: 20709
diff changeset
    96
fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    97
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    98
fun unfoldl dest x =
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
    99
  case dest x
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   100
   of NONE => (x, [])
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   101
    | SOME (x1, x2) =>
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   102
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   103
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   104
fun unfoldr dest x =
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   105
  case dest x
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   106
   of NONE => ([], x)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   107
    | SOME (x1, x2) =>
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   108
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   109
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   110
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   111
(** language core - types, pattern, expressions **)
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   112
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   113
(* language representation *)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   114
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   115
type vname = string;
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   116
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   117
datatype dict =
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   118
    DictConst of string * dict list list
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   119
  | DictVar of string list * (vname * (int * int));
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   120
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   121
datatype itype =
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   122
    `%% of string * itype list
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   123
  | ITyVar of vname;
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   124
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
   125
datatype iterm =
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
   126
    IConst of string * (dict list list * itype list)
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   127
  | IVar of vname
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
   128
  | `$ of iterm * iterm
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
   129
  | `|-> of (vname * itype) * iterm
21012
haftmann
parents: 20976
diff changeset
   130
  | ICase of (iterm * itype) * (iterm * iterm) list;
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   131
    (*see also signature*)
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   132
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   133
(*
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   134
  variable naming conventions
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   135
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   136
  bare names:
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   137
    variable names          v
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   138
    class names             class
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   139
    type constructor names  tyco
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   140
    datatype names          dtco
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   141
    const names (general)   c
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   142
    constructor names       co
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   143
    class operation names   clsop (op)
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   144
    arbitrary name          s
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   145
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   146
    v, c, co, clsop also annotated with types etc.
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   147
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   148
  constructs:
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   149
    sort                    sort
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
   150
    type parameters         vs
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   151
    type                    ty
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
   152
    type schemes            tysm
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   153
    term                    t
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   154
    (term as pattern)       p
21838
f9243336f54e fixed type
haftmann
parents: 21160
diff changeset
   155
    instance (class, tyco)  inst
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   156
 *)
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   157
21123
9f7c430cf9ac dropped constructiv `->
haftmann
parents: 21082
diff changeset
   158
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
19167
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   159
val op `--> = Library.foldr (op `->);
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   160
val op `$$ = Library.foldl (op `$);
f237c0cb3882 refined representation of codegen intermediate language
haftmann
parents: 19150
diff changeset
   161
val op `|--> = Library.foldr (op `|->);
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   162
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   163
val unfold_fun = unfoldr
21123
9f7c430cf9ac dropped constructiv `->
haftmann
parents: 21082
diff changeset
   164
  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   165
    | _ => NONE);
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   166
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   167
val unfold_app = unfoldl
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   168
  (fn op `$ t => SOME t
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   169
    | _ => NONE);
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   170
22062
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   171
val split_abs =
21012
haftmann
parents: 20976
diff changeset
   172
  (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) =>
haftmann
parents: 20976
diff changeset
   173
        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
haftmann
parents: 20976
diff changeset
   174
    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
22062
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   175
    | _ => NONE);
18282
98431741bda3 added haskell serializer
haftmann
parents: 18247
diff changeset
   176
22062
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   177
val unfold_abs = unfoldr split_abs;
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   178
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   179
val split_let = 
21012
haftmann
parents: 20976
diff changeset
   180
  (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t)
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   181
    | _ => NONE);
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents:
diff changeset
   182
22062
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   183
val unfold_let = unfoldr split_let;
f4cfc4101c8f more term inspection
haftmann
parents: 22037
diff changeset
   184
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   185
fun unfold_const_app t =
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   186
 case unfold_app t
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   187
  of (IConst c, ts) => SOME (c, ts)
18865
31aed965135c minor cleanups
haftmann
parents: 18852
diff changeset
   188
   | _ => NONE;
31aed965135c minor cleanups
haftmann
parents: 18852
diff changeset
   189
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   190
fun fold_aiterms f (t as IConst _) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   191
      f t
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   192
  | fold_aiterms f (t as IVar _) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   193
      f t
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   194
  | fold_aiterms f (t1 `$ t2) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   195
      fold_aiterms f t1 #> fold_aiterms f t2
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   196
  | fold_aiterms f (t as _ `|-> t') =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   197
      f t #> fold_aiterms f t'
21012
haftmann
parents: 20976
diff changeset
   198
  | fold_aiterms f (ICase ((td, _), bs)) =
haftmann
parents: 20976
diff changeset
   199
      fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
19202
0b9eb4b0ad98 substantial improvement in codegen iml
haftmann
parents: 19167
diff changeset
   200
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   201
fun fold_constnames f =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   202
  let
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   203
    fun add (IConst (c, _)) = f c
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   204
      | add _ = I;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   205
  in fold_aiterms add end;
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   206
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   207
fun fold_varnames f =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   208
  let
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   209
    fun add (IVar v) = f v
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   210
      | add ((v, _) `|-> _) = f v
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   211
      | add _ = I;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   212
  in fold_aiterms add end;
20709
645236e80885 some cleanup
haftmann
parents: 20600
diff changeset
   213
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   214
fun fold_unbound_varnames f =
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   215
  let
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   216
    fun add _ (IConst _) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   217
          I
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   218
      | add vs (IVar v) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   219
          if not (member (op =) vs v) then f v else I
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   220
      | add vs (t1 `$ t2) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   221
          add vs t1 #> add vs t2
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   222
      | add vs ((v, _) `|-> t) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   223
          add (insert (op =) v vs) t
21012
haftmann
parents: 20976
diff changeset
   224
      | add vs (ICase ((td, _), bs)) =
haftmann
parents: 20976
diff changeset
   225
          add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   226
  in add [] end;
20105
454f4be984b7 adaptions in codegen
haftmann
parents: 20071
diff changeset
   227
23516
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   228
fun collapse_let (((v, ty), se), be as ICase ((IVar w, _), ds)) =
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   229
      let
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   230
        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   231
          b orelse v = w) t false;
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   232
      in if v = w andalso forall (fn (t1, t2) =>
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   233
        exists_v t1 orelse not (exists_v t2)) ds
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   234
        then ICase ((se, ty), ds)
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   235
        else ICase ((se, ty), [(IVar v, be)])
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   236
      end
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   237
  | collapse_let (((v, ty), se), be) =
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   238
      ICase ((se, ty), [(IVar v, be)])
f7d54060b5b0 proper collapse_let
haftmann
parents: 23028
diff changeset
   239
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
   240
fun eta_expand (c as (_, (_, tys)), ts) k =
19607
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   241
  let
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   242
    val j = length ts;
19607
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   243
    val l = k - j;
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   244
    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
   245
    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
20439
1bf42b262a38 code refinements
haftmann
parents: 20428
diff changeset
   246
  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
19607
07eeb832f28d introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents: 19597
diff changeset
   247
18304
684832c9fa62 minor improvements
haftmann
parents: 18282
diff changeset
   248
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   249
(** definitions, transactions **)
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   250
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   251
(* type definitions *)
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   252
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
   253
type typscheme = (vname * sort) list * itype;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   254
datatype def =
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   255
    Bot
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
   256
  | Fun of (iterm list * iterm) list * typscheme
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
   257
  | Datatype of (vname * sort) list * (string * itype list) list
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   258
  | Datatypecons of string
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   259
  | Class of (class * string) list * (vname * (string * itype) list)
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   260
  | Classop of class
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   261
  | Classrel of class * class
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
   262
  | Classinst of (class * (string * (vname * sort) list))
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   263
        * ((class * (string * (string * dict list list))) list
20456
42be3a46dcd8 pervasive refinements
haftmann
parents: 20439
diff changeset
   264
      * (string * iterm) list);
19597
8ced57ffc090 major refinement of codegen_theorems.ML
haftmann
parents: 19482
diff changeset
   265
val eq_def = (op =) : def * def -> bool;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   266
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   267
type code = def Graph.T;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   268
type transact = Graph.key option * code;
21012
haftmann
parents: 20976
diff changeset
   269
exception FAIL of string list;
18360
a2c9506b62a7 improved class handling
haftmann
parents: 18335
diff changeset
   270
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   271
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   272
(* abstract code *)
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   273
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   274
val empty_code = Graph.empty : code; (*read: "depends on"*)
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   275
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   276
val get_def = Graph.get_node;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   277
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   278
fun ensure_bot name = Graph.default_node (name, Bot);
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   279
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   280
fun add_def_incr strict (name, Bot) code =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   281
      (case the_default Bot (try (get_def code) name)
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   282
       of Bot => if strict then error "Attempted to add Bot to code"
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   283
            else Graph.map_node name (K Bot) code
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   284
        | _ => code)
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   285
  | add_def_incr _ (name, def) code =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   286
      (case try (get_def code) name
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   287
       of NONE => Graph.new_node (name, def) code
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   288
        | SOME Bot => Graph.map_node name (K def) code
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   289
        | SOME def' => if eq_def (def, def')
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   290
            then code
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
   291
            else error ("Tried to overwrite definition " ^ quote name));
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   292
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   293
fun add_dep (dep as (name1, name2)) =
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   294
  if name1 = name2 then I else Graph.add_edge dep;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   295
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   296
val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot);
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   297
21012
haftmann
parents: 20976
diff changeset
   298
fun project_code hidden raw_selected code =
20466
7c20ddbd911b explicit table with constant types
haftmann
parents: 20456
diff changeset
   299
  let
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   300
    fun is_bot name = case get_def code name
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   301
     of Bot => true
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   302
      | _ => false;
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   303
    val names = subtract (op =) hidden (Graph.keys code);
21012
haftmann
parents: 20976
diff changeset
   304
    val deleted = Graph.all_preds code (filter is_bot names);
haftmann
parents: 20976
diff changeset
   305
    val selected = case raw_selected
haftmann
parents: 20976
diff changeset
   306
     of NONE => names |> subtract (op =) deleted 
haftmann
parents: 20976
diff changeset
   307
      | SOME sel => sel
haftmann
parents: 20976
diff changeset
   308
          |> subtract (op =) deleted
haftmann
parents: 20976
diff changeset
   309
          |> subtract (op =) hidden
haftmann
parents: 20976
diff changeset
   310
          |> Graph.all_succs code
haftmann
parents: 20976
diff changeset
   311
          |> subtract (op =) deleted
haftmann
parents: 20976
diff changeset
   312
          |> subtract (op =) hidden;
20191
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20175
diff changeset
   313
  in
21012
haftmann
parents: 20976
diff changeset
   314
    code
21937
4ba9531c60eb renamed Graph.project to Graph.subgraph;
wenzelm
parents: 21911
diff changeset
   315
    |> Graph.subgraph (member (op =) selected)
20191
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20175
diff changeset
   316
  end;
b43fd26e1aaa improvements for lazy code generation
haftmann
parents: 20175
diff changeset
   317
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   318
fun check_samemodule names =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   319
  fold (fn name =>
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   320
    let
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   321
      val module_name = (NameSpace.qualifier o NameSpace.qualifier) name
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   322
    in
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   323
     fn NONE => SOME module_name
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   324
      | SOME module_name' => if module_name = module_name' then SOME module_name
20386
d1cbe5aa6bf2 module restructuring
haftmann
parents: 20353
diff changeset
   325
          else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   326
    end
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   327
  ) names NONE;
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   328
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   329
fun check_funeqs eqs =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   330
  (fold (fn (pats, _) =>
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   331
    let
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   332
      val l = length pats
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   333
    in
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   334
     fn NONE => SOME l
18850
92ef83e5eaea various improvements
haftmann
parents: 18812
diff changeset
   335
      | SOME l' => if l = l' then SOME l
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
   336
          else error "Function definition with different number of arguments"
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   337
    end
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   338
  ) eqs NONE; eqs);
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   339
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   340
fun check_prep_def code Bot =
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   341
      Bot
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   342
  | check_prep_def code (Fun (eqs, d)) =
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   343
      Fun (check_funeqs eqs, d)
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   344
  | check_prep_def code (d as Datatype _) =
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   345
      d
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   346
  | check_prep_def code (Datatypecons dtco) =
22185
haftmann
parents: 22076
diff changeset
   347
      error "Attempted to add bare term constructor"
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   348
  | check_prep_def code (d as Class _) =
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   349
      d
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   350
  | check_prep_def code (Classop _) =
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   351
      error "Attempted to add bare class operation"
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   352
  | check_prep_def code (Classrel _) =
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   353
      error "Attempted to add bare class relation"
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   354
  | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   355
      let
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   356
        val Class (_, (_, classops)) = get_def code class;
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   357
        val _ = if length inst_classops > length classops
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   358
          then error "Too many class operations given"
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   359
          else ();
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   360
        fun check_classop (f, _) =
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   361
          if AList.defined (op =) inst_classops f
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   362
          then () else error ("Missing definition for class operation " ^ quote f);
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   363
        val _ = map check_classop classops;
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   364
      in d end;
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   365
19038
62c5f7591a43 improved handling of iml abstractions
haftmann
parents: 19025
diff changeset
   366
fun postprocess_def (name, Datatype (_, constrs)) =
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   367
      tap (fn _ => check_samemodule (name :: map fst constrs))
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   368
      #> fold (fn (co, _) =>
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   369
        add_def_incr true (co, Datatypecons name)
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   370
        #> add_dep (co, name)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   371
        #> add_dep (name, co)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   372
      ) constrs
22076
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   373
  | postprocess_def (name, Class (classrels, (_, classops))) =
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   374
      tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   375
      #> fold (fn (f, _) =>
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   376
        add_def_incr true (f, Classop name)
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   377
        #> add_dep (f, name)
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   378
        #> add_dep (name, f)
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   379
      ) classops
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   380
      #> fold (fn (superclass, classrel) =>
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   381
        add_def_incr true (classrel, Classrel (name, superclass))
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   382
        #> add_dep (classrel, name)
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   383
        #> add_dep (name, classrel)
42ae57200d96 changed dictionary representation to explicit classrel witnesses
haftmann
parents: 22062
diff changeset
   384
      ) classrels
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   385
  | postprocess_def _ =
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   386
      I;
18380
9668764224a7 substantial improvements for class code generation
haftmann
parents: 18361
diff changeset
   387
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   388
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   389
(* transaction protocol *)
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   390
22037
fbf0a12d053f proper node names
haftmann
parents: 21937
diff changeset
   391
fun ensure_def labelled_name defgen strict msg name (dep, code) =
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   392
  let
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   393
    val msg' = (case dep
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   394
     of NONE => msg
22037
fbf0a12d053f proper node names
haftmann
parents: 21937
diff changeset
   395
      | SOME dep => msg ^ ", required for " ^ labelled_name dep)
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   396
      ^ (if strict then " (strict)" else " (non-strict)");
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   397
    fun add_dp NONE = I
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   398
      | add_dp (SOME dep) =
22037
fbf0a12d053f proper node names
haftmann
parents: 21937
diff changeset
   399
          tracing (fn _ => "adding dependency " ^ labelled_name dep
fbf0a12d053f proper node names
haftmann
parents: 21937
diff changeset
   400
            ^ " -> " ^ labelled_name name)
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   401
          #> add_dep (dep, name);
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   402
    fun prep_def def code =
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   403
      (check_prep_def code def, code);
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   404
    fun invoke_generator name defgen code =
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   405
      defgen (SOME name, code)
21012
haftmann
parents: 20976
diff changeset
   406
        handle FAIL msgs =>
haftmann
parents: 20976
diff changeset
   407
          if strict then raise FAIL (msg' :: msgs)
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   408
          else (Bot, code);
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   409
  in
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   410
    code
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   411
    |> (if can (get_def code) name
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   412
        then
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
   413
          add_dp dep
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   414
        else
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
   415
          ensure_bot name
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   416
          #> add_dp dep
19816
a8c8ed1c85e0 removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents: 19785
diff changeset
   417
          #> invoke_generator name defgen
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   418
          #-> (fn def => prep_def def)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   419
          #-> (fn def =>
22305
0e56750a092b changed representation of constants
haftmann
parents: 22185
diff changeset
   420
             add_def_incr strict (name, def)
18702
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   421
          #> postprocess_def (name, def)
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   422
       ))
7dc7dcd63224 substantial improvements in code generator
haftmann
parents: 18517
diff changeset
   423
    |> pair dep
18170
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   424
  end;
73ce773f12de added module system
haftmann
parents: 18169
diff changeset
   425
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   426
fun succeed some (_, code) = (some, code);
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   427
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   428
fun fail msg (_, code) = raise FAIL [msg];
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   429
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   430
fun message msg f trns =
21012
haftmann
parents: 20976
diff changeset
   431
  f trns handle FAIL msgs =>
haftmann
parents: 20976
diff changeset
   432
    raise FAIL (msg :: msgs);
19884
a7be206d8655 improvements in code generator
haftmann
parents: 19816
diff changeset
   433
22185
haftmann
parents: 22076
diff changeset
   434
fun start_transact f code =
18231
2eea98bbf650 improved failure tracking
haftmann
parents: 18216
diff changeset
   435
  let
18963
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18919
diff changeset
   436
    fun handle_fail f x =
3adfc9dfb30a slight improvements in code generation
haftmann
parents: 18919
diff changeset
   437
      (f x
21012
haftmann
parents: 20976
diff changeset
   438
      handle FAIL msgs =>
20389
8b6ecb22ef35 cleanup
haftmann
parents: 20386
diff changeset
   439
        (error o cat_lines) ("Code generation failed, while:" :: msgs))
18231
2eea98bbf650 improved failure tracking
haftmann
parents: 18216
diff changeset
   440
  in
22185
haftmann
parents: 22076
diff changeset
   441
    (NONE, code)
18231
2eea98bbf650 improved failure tracking
haftmann
parents: 18216
diff changeset
   442
    |> handle_fail f
21082
82460fa3340d final Haskell serializer
haftmann
parents: 21012
diff changeset
   443
    |-> (fn x => fn (_, code) => (x, code))
18231
2eea98bbf650 improved failure tracking
haftmann
parents: 18216
diff changeset
   444
  end;
18172
8ff5bcfae27a added generic transformators
haftmann
parents: 18170
diff changeset
   445
21160
haftmann
parents: 21123
diff changeset
   446
fun add_eval_def (name, t) code =
haftmann
parents: 21123
diff changeset
   447
  code
haftmann
parents: 21123
diff changeset
   448
  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
haftmann
parents: 21123
diff changeset
   449
  |> fold (curry Graph.add_edge name) (Graph.keys code);
18172
8ff5bcfae27a added generic transformators
haftmann
parents: 18170
diff changeset
   450
20896
1484c7af6d68 cleaned up interfaces
haftmann
parents: 20855
diff changeset
   451
end; (*struct*)
18885
ee8b5c36ba2b substantial cleanup and simplifications
haftmann
parents: 18865
diff changeset
   452
18216
db7d43b25c99 added serializer
haftmann
parents: 18172
diff changeset
   453
19300
7689f81f8996 subtract (op =);
wenzelm
parents: 19253
diff changeset
   454
structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;