src/Pure/Tools/codegen_thingol.ML
author haftmann
Wed Aug 30 15:11:17 2006 +0200 (2006-08-30)
changeset 20439 1bf42b262a38
parent 20428 67fa1c6ba89e
child 20456 42be3a46dcd8
permissions -rw-r--r--
code refinements
haftmann@18380
     1
(*  Title:      Pure/Tools/codegen_thingol.ML
haftmann@18169
     2
    ID:         $Id$
haftmann@18169
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@18169
     4
haftmann@18169
     5
Intermediate language ("Thin-gol") for code extraction.
haftmann@18169
     6
*)
haftmann@18169
     7
haftmann@19167
     8
infix 8 `%%;
haftmann@19167
     9
infixr 6 `->;
haftmann@19167
    10
infixr 6 `-->;
haftmann@19167
    11
infix 4 `$;
haftmann@19167
    12
infix 4 `$$;
haftmann@19167
    13
infixr 3 `|->;
haftmann@19167
    14
infixr 3 `|-->;
haftmann@19167
    15
haftmann@19136
    16
signature BASIC_CODEGEN_THINGOL =
haftmann@18169
    17
sig
haftmann@18169
    18
  type vname = string;
haftmann@19167
    19
  type sortcontext = ClassPackage.sortcontext;
haftmann@19967
    20
  datatype iclasslookup =
haftmann@19967
    21
      Instance of string * iclasslookup list list
haftmann@19967
    22
    | Lookup of class list * (vname * int);
haftmann@18169
    23
  datatype itype =
haftmann@19167
    24
      `%% of string * itype list
haftmann@19167
    25
    | `-> of itype * itype
haftmann@19167
    26
    | ITyVar of vname;
haftmann@20105
    27
  datatype iterm =
haftmann@19202
    28
      IConst of string * (iclasslookup list list * itype)
haftmann@19167
    29
    | IVar of vname
haftmann@20105
    30
    | `$ of iterm * iterm
haftmann@20105
    31
    | `|-> of (vname * itype) * iterm
haftmann@20105
    32
    | INum of IntInf.int (*non-negative!*) * iterm
haftmann@20105
    33
    | IChar of string (*length one!*) * iterm
haftmann@20105
    34
    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@20439
    35
        (*((discriminendum term (td), discriminendum type (ty)),
haftmann@20439
    36
                [(selector pattern (p), body term (t))] (bs)),
haftmann@20439
    37
                pure term (t0))*)
haftmann@19136
    38
end;
haftmann@19136
    39
haftmann@19136
    40
signature CODEGEN_THINGOL =
haftmann@19136
    41
sig
haftmann@19136
    42
  include BASIC_CODEGEN_THINGOL;
haftmann@19167
    43
  val `--> : itype list * itype -> itype;
haftmann@20105
    44
  val `$$ : iterm * iterm list -> iterm;
haftmann@20105
    45
  val `|--> : (vname * itype) list * iterm -> iterm;
haftmann@18169
    46
  val pretty_itype: itype -> Pretty.T;
haftmann@20105
    47
  val pretty_iterm: iterm -> Pretty.T;
haftmann@18216
    48
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
haftmann@18216
    49
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
haftmann@18169
    50
  val unfold_fun: itype -> itype list * itype;
haftmann@20105
    51
  val unfold_app: iterm -> iterm * iterm list;
haftmann@20105
    52
  val unfold_abs: iterm -> (iterm * itype) list * iterm;
haftmann@20105
    53
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
haftmann@20105
    54
  val unfold_const_app: iterm ->
haftmann@20105
    55
    ((string * (iclasslookup list list * itype)) * iterm list) option;
haftmann@20105
    56
  val add_constnames: iterm -> string list -> string list;
haftmann@20105
    57
  val add_varnames: iterm -> string list -> string list;
haftmann@20105
    58
  val is_pat: (string -> bool) -> iterm -> bool;
haftmann@20105
    59
  val vars_distinct: iterm list -> bool;
haftmann@20105
    60
  val map_pure: (iterm -> 'a) -> iterm -> 'a;
haftmann@20105
    61
  val eta_expand: (string * (iclasslookup list list * itype)) * iterm list -> int -> iterm;
haftmann@20105
    62
  val resolve_tycos: (string -> string) -> itype * iterm list -> itype * iterm list;
haftmann@20105
    63
  val resolve_consts: (string -> string) -> iterm -> iterm;
haftmann@18170
    64
haftmann@20105
    65
  type funn = (iterm list * iterm) list * (sortcontext * itype);
haftmann@19167
    66
  type datatyp = sortcontext * (string * itype list) list;
haftmann@18170
    67
  datatype def =
haftmann@19816
    68
      Bot
haftmann@18702
    69
    | Fun of funn
haftmann@20191
    70
    | Typesyn of sortcontext * itype
haftmann@19042
    71
    | Datatype of datatyp
haftmann@18380
    72
    | Datatypecons of string
haftmann@19167
    73
    | Class of class list * (vname * (string * (sortcontext * itype)) list)
haftmann@18380
    74
    | Classmember of class
haftmann@20389
    75
    | Classinst of (class * (string * (vname * sort) list))
haftmann@20389
    76
          * ((class * iclasslookup list) list
haftmann@20389
    77
        * (string * iterm) list);
haftmann@18170
    78
  type module;
haftmann@18170
    79
  type transact;
haftmann@18170
    80
  type 'dst transact_fin;
haftmann@18170
    81
  val pretty_def: def -> Pretty.T;
haftmann@20191
    82
  val pretty_module: module -> Pretty.T;
haftmann@18360
    83
  val pretty_deps: module -> Pretty.T;
haftmann@18170
    84
  val empty_module: module;
haftmann@19341
    85
  val get_def: module -> string -> def;
haftmann@18170
    86
  val merge_module: module * module -> module;
haftmann@19042
    87
  val diff_module: module * module -> (string * def) list;
haftmann@19341
    88
  val project_module: string list -> module -> module;
haftmann@19341
    89
  val purge_module: string list -> module -> module;
haftmann@20428
    90
(*   val flat_funs_datatypes: module -> (string * def) list;  *)
haftmann@20216
    91
  val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module;
haftmann@20191
    92
  val delete_garbage: string list (*hidden definitions*) -> module -> module;
haftmann@18516
    93
  val has_nsp: string -> string -> bool;
haftmann@19884
    94
  val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
haftmann@19884
    95
    -> string -> transact -> transact;
haftmann@18170
    96
  val succeed: 'a -> transact -> 'a transact_fin;
haftmann@18170
    97
  val fail: string -> transact -> 'a transact_fin;
haftmann@19884
    98
  val message: string -> (transact -> 'a) -> transact -> 'a;
haftmann@18963
    99
  val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
haftmann@20389
   100
  val elim_classes: module -> funn -> (iterm list * iterm) list * itype;
haftmann@18216
   101
haftmann@19341
   102
  val debug: bool ref;
haftmann@19341
   103
  val debug_msg: ('a -> string) -> 'a -> 'a;
haftmann@18231
   104
  val soft_exc: bool ref;
haftmann@18216
   105
haftmann@18216
   106
  val serialize:
haftmann@19038
   107
    ((string -> string -> string) -> string -> (string * def) list -> 'a option)
haftmann@19341
   108
    -> ((string -> string) -> string list -> (string * string) * 'a list -> 'a option)
haftmann@18216
   109
    -> (string -> string option)
haftmann@18919
   110
    -> (string * string -> string)
haftmann@18850
   111
    -> string list list -> string -> module -> 'a option;
haftmann@18169
   112
end;
haftmann@18169
   113
haftmann@18850
   114
structure CodegenThingol: CODEGEN_THINGOL =
haftmann@18169
   115
struct
haftmann@18169
   116
haftmann@18170
   117
(** auxiliary **)
haftmann@18169
   118
haftmann@19341
   119
val debug = ref false;
haftmann@20405
   120
fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x);
haftmann@18231
   121
val soft_exc = ref true;
haftmann@18169
   122
haftmann@18169
   123
fun unfoldl dest x =
haftmann@18169
   124
  case dest x
haftmann@18169
   125
   of NONE => (x, [])
haftmann@18169
   126
    | SOME (x1, x2) =>
haftmann@18169
   127
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
haftmann@18169
   128
haftmann@18169
   129
fun unfoldr dest x =
haftmann@18169
   130
  case dest x
haftmann@18169
   131
   of NONE => ([], x)
haftmann@18169
   132
    | SOME (x1, x2) =>
haftmann@18169
   133
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
haftmann@18169
   134
haftmann@18170
   135
haftmann@18170
   136
haftmann@18170
   137
(** language core - types, pattern, expressions **)
haftmann@18169
   138
haftmann@18169
   139
(* language representation *)
haftmann@18169
   140
haftmann@18169
   141
type vname = string;
haftmann@18169
   142
haftmann@19167
   143
type sortcontext = ClassPackage.sortcontext;
haftmann@19967
   144
datatype iclasslookup =
haftmann@19967
   145
    Instance of string * iclasslookup list list
haftmann@19967
   146
  | Lookup of class list * (vname * int);
haftmann@18885
   147
haftmann@18169
   148
datatype itype =
haftmann@19167
   149
    `%% of string * itype list
haftmann@19167
   150
  | `-> of itype * itype
haftmann@19167
   151
  | ITyVar of vname;
haftmann@18169
   152
haftmann@20105
   153
datatype iterm =
haftmann@19202
   154
    IConst of string * (iclasslookup list list * itype)
haftmann@19167
   155
  | IVar of vname
haftmann@20105
   156
  | `$ of iterm * iterm
haftmann@20105
   157
  | `|-> of (vname * itype) * iterm
haftmann@20105
   158
  | INum of IntInf.int * iterm
haftmann@20105
   159
  | IChar of string * iterm
haftmann@20105
   160
  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@19167
   161
    (*see also signature*)
haftmann@18169
   162
haftmann@18380
   163
(*
haftmann@18380
   164
  variable naming conventions
haftmann@18380
   165
haftmann@18380
   166
  bare names:
haftmann@18380
   167
    variable names          v
haftmann@20439
   168
    class names             class
haftmann@18380
   169
    type constructor names  tyco
haftmann@18380
   170
    datatype names          dtco
haftmann@18380
   171
    const names (general)   c
haftmann@18380
   172
    constructor names       co
haftmann@20439
   173
    class operation names   clsop (op)
haftmann@18380
   174
    arbitrary name          s
haftmann@18380
   175
haftmann@20439
   176
    v, c, co, clsop also annotated with types usw.
haftmann@20439
   177
haftmann@18380
   178
  constructs:
haftmann@18380
   179
    sort                    sort
haftmann@20439
   180
    sort context            sctxt, vs (variables with sorts)
haftmann@18380
   181
    type                    ty
haftmann@20439
   182
    term                    t
haftmann@20439
   183
    (term as pattern)       p
haftmann@20439
   184
    instance (classs, tyco) inst
haftmann@18380
   185
 *)
haftmann@18380
   186
haftmann@19167
   187
val op `--> = Library.foldr (op `->);
haftmann@19167
   188
val op `$$ = Library.foldl (op `$);
haftmann@19167
   189
val op `|--> = Library.foldr (op `|->);
haftmann@18169
   190
haftmann@19150
   191
val pretty_sortcontext =
haftmann@19341
   192
  Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
haftmann@19150
   193
    [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
haftmann@19150
   194
haftmann@19167
   195
fun pretty_itype (tyco `%% tys) =
haftmann@19341
   196
      Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
haftmann@19167
   197
  | pretty_itype (ty1 `-> ty2) =
haftmann@18885
   198
      Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
haftmann@19167
   199
  | pretty_itype (ITyVar v) =
haftmann@19150
   200
      Pretty.str v;
haftmann@18885
   201
haftmann@20105
   202
fun pretty_iterm (IConst (c, _)) =
haftmann@19167
   203
      Pretty.str c
haftmann@20105
   204
  | pretty_iterm (IVar v) =
haftmann@19167
   205
      Pretty.str ("?" ^ v)
haftmann@20439
   206
  | pretty_iterm (t1 `$ t2) =
haftmann@19167
   207
      (Pretty.enclose "(" ")" o Pretty.breaks)
haftmann@20439
   208
        [pretty_iterm t1, pretty_iterm t2]
haftmann@20439
   209
  | pretty_iterm ((v, ty) `|-> t) =
haftmann@20105
   210
      (Pretty.enclose "(" ")" o Pretty.breaks)
haftmann@20439
   211
        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
haftmann@20105
   212
  | pretty_iterm (INum (n, _)) =
haftmann@19202
   213
      (Pretty.str o IntInf.toString) n
haftmann@20439
   214
  | pretty_iterm (IChar (h, _)) =
haftmann@20439
   215
      (Pretty.str o quote) h
haftmann@20439
   216
  | pretty_iterm (ICase (((t, _), bs), _)) =
haftmann@19167
   217
      (Pretty.enclose "(" ")" o Pretty.breaks) [
haftmann@19167
   218
        Pretty.str "case",
haftmann@20439
   219
        pretty_iterm t,
haftmann@20439
   220
        Pretty.enclose "(" ")" (map (fn (p, t) =>
haftmann@19167
   221
          (Pretty.block o Pretty.breaks) [
haftmann@20105
   222
            pretty_iterm p,
haftmann@19167
   223
            Pretty.str "=>",
haftmann@20439
   224
            pretty_iterm t
haftmann@18885
   225
          ]
haftmann@20439
   226
        ) bs)
haftmann@18885
   227
      ];
haftmann@18885
   228
haftmann@18169
   229
val unfold_fun = unfoldr
haftmann@20439
   230
  (fn op `-> ty => SOME ty
haftmann@18169
   231
    | _ => NONE);
haftmann@18169
   232
haftmann@18169
   233
val unfold_app = unfoldl
haftmann@20439
   234
  (fn op `$ t => SOME t
haftmann@18169
   235
    | _ => NONE);
haftmann@18169
   236
haftmann@18282
   237
val unfold_abs = unfoldr
haftmann@20439
   238
  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(p, t)]), _)) =>
haftmann@20439
   239
        if v = w then SOME ((p, ty), t) else SOME ((IVar v, ty), t)
haftmann@20439
   240
    | (v, ty) `|-> t => SOME ((IVar v, ty), t)
haftmann@18282
   241
    | _ => NONE)
haftmann@18282
   242
haftmann@18169
   243
val unfold_let = unfoldr
haftmann@20439
   244
  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
haftmann@18169
   245
    | _ => NONE);
haftmann@18169
   246
haftmann@20439
   247
fun unfold_const_app t =
haftmann@20439
   248
 case unfold_app t
haftmann@20439
   249
  of (IConst c, ts) => SOME (c, ts)
haftmann@18865
   250
   | _ => NONE;
haftmann@18865
   251
haftmann@19167
   252
fun map_itype _ (ty as ITyVar _) =
haftmann@19167
   253
      ty
haftmann@19167
   254
  | map_itype f (tyco `%% tys) =
haftmann@19167
   255
      tyco `%% map f tys
haftmann@20439
   256
  | map_itype f (ty1 `-> ty2) =
haftmann@20439
   257
      f ty1 `-> f ty2;
haftmann@18172
   258
haftmann@19150
   259
fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
haftmann@18282
   260
  let
haftmann@18282
   261
    exception NO_MATCH;
haftmann@19150
   262
    fun eq_sctxt subs sctxt1 sctxt2 =
haftmann@19597
   263
      map (fn (v : string, sort : string list) => case AList.lookup (op =) subs v
haftmann@19150
   264
       of NONE => raise NO_MATCH
haftmann@19597
   265
        | SOME (v' : string) => case AList.lookup (op =) sctxt2 v'
haftmann@19150
   266
           of NONE => raise NO_MATCH
haftmann@19150
   267
            | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1
haftmann@19167
   268
    fun eq (ITyVar v1) (ITyVar v2) subs =
haftmann@19150
   269
          (case AList.lookup (op =) subs v1
haftmann@19150
   270
           of NONE => subs |> AList.update (op =) (v1, v2)
haftmann@19150
   271
            | SOME v1' =>
haftmann@19150
   272
                if v1' <> v2
haftmann@19150
   273
                then raise NO_MATCH
haftmann@19150
   274
                else subs)
haftmann@19167
   275
      | eq (tyco1 `%% tys1) (tyco2 `%% tys2) subs =
haftmann@18282
   276
          if tyco1 <> tyco2
haftmann@18282
   277
          then raise NO_MATCH
haftmann@18282
   278
          else subs |> fold2 eq tys1 tys2
haftmann@19167
   279
      | eq (ty11 `-> ty12) (ty21 `-> ty22) subs =
haftmann@18282
   280
          subs |> eq ty11 ty21 |> eq ty12 ty22
haftmann@18282
   281
      | eq _ _ _ = raise NO_MATCH;
haftmann@18282
   282
  in
haftmann@18282
   283
    (eq ty1 ty2 []; true)
haftmann@18282
   284
    handle NO_MATCH => false
haftmann@18282
   285
  end;
haftmann@18282
   286
haftmann@18885
   287
fun instant_itype f =
haftmann@18885
   288
  let
haftmann@20439
   289
    fun instant (ITyVar v) = f v
haftmann@20439
   290
      | instant ty = map_itype instant ty;
haftmann@19215
   291
  in instant end;
haftmann@18885
   292
haftmann@20439
   293
fun is_pat is_cons (IConst (c, ([], _))) = is_cons c
haftmann@20439
   294
  | is_pat _ (IVar _) = true
haftmann@20439
   295
  | is_pat is_cons (t1 `$ t2) =
haftmann@20439
   296
      is_pat is_cons t1 andalso is_pat is_cons t2
haftmann@20439
   297
  | is_pat _ (INum _) = true
haftmann@20439
   298
  | is_pat _ (IChar _) = true
haftmann@19953
   299
  | is_pat _ _ = false;
haftmann@19202
   300
haftmann@20439
   301
fun map_pure f (t as IConst _) =
haftmann@20439
   302
      f t
haftmann@20439
   303
  | map_pure f (t as IVar _) =
haftmann@20439
   304
      f t
haftmann@20439
   305
  | map_pure f (t as _ `$ _) =
haftmann@20439
   306
      f t
haftmann@20439
   307
  | map_pure f (t as _ `|-> _) =
haftmann@20439
   308
      f t
haftmann@20439
   309
  | map_pure f (INum (_, t0)) =
haftmann@20439
   310
      f t0
haftmann@20439
   311
  | map_pure f (IChar (_, t0)) =
haftmann@20439
   312
      f t0
haftmann@20439
   313
  | map_pure f (ICase (_, t0)) =
haftmann@20439
   314
      f t0;
haftmann@18912
   315
haftmann@19607
   316
fun resolve_tycos _ = error "";
haftmann@19607
   317
fun resolve_consts _ = error "";
haftmann@18216
   318
haftmann@19202
   319
fun add_constnames (IConst (c, _)) =
haftmann@19202
   320
      insert (op =) c
haftmann@19202
   321
  | add_constnames (IVar _) =
haftmann@19167
   322
      I
haftmann@20439
   323
  | add_constnames (t1 `$ t2) =
haftmann@20439
   324
      add_constnames t1 #> add_constnames t2
haftmann@20439
   325
  | add_constnames (_ `|-> t) =
haftmann@20439
   326
      add_constnames t
haftmann@20439
   327
  | add_constnames (INum (_, t0)) =
haftmann@20439
   328
      add_constnames t0
haftmann@20439
   329
  | add_constnames (IChar (_, t0)) =
haftmann@20439
   330
      add_constnames t0
haftmann@20439
   331
  | add_constnames (ICase (_, t0)) =
haftmann@20439
   332
      add_constnames t0;
haftmann@19202
   333
haftmann@19202
   334
fun add_varnames (IConst _) =
haftmann@19202
   335
      I
haftmann@19202
   336
  | add_varnames (IVar v) =
haftmann@19167
   337
      insert (op =) v
haftmann@20439
   338
  | add_varnames (t1 `$ t2) =
haftmann@20439
   339
      add_varnames t1 #> add_varnames t2
haftmann@20439
   340
  | add_varnames ((v, _) `|-> t) =
haftmann@20439
   341
      insert (op =) v #> add_varnames t
haftmann@20439
   342
  | add_varnames (INum (_, t)) =
haftmann@20439
   343
      add_varnames t
haftmann@20439
   344
  | add_varnames (IChar (_, t)) =
haftmann@20439
   345
      add_varnames t
haftmann@20439
   346
  | add_varnames (ICase (((td, _), bs), _)) =
haftmann@20439
   347
      add_varnames td #> fold (fn (p, t) => add_varnames p #> add_varnames t) bs;
haftmann@18885
   348
haftmann@20439
   349
fun vars_distinct ts =
haftmann@18885
   350
  let
haftmann@20105
   351
    fun distinct _ NONE =
haftmann@20105
   352
          NONE
haftmann@20105
   353
      | distinct (IConst _) x =
haftmann@20105
   354
          x
haftmann@20105
   355
      | distinct (IVar v) (SOME vs) =
haftmann@20105
   356
          if member (op =) vs v then NONE else SOME (v::vs)
haftmann@20439
   357
      | distinct (t1 `$ t2) x =
haftmann@20439
   358
          x |> distinct t1 |> distinct t2
haftmann@20439
   359
      | distinct (_ `|-> t) x =
haftmann@20439
   360
          x |> distinct t
haftmann@20105
   361
      | distinct (INum _) x =
haftmann@20105
   362
          x
haftmann@20105
   363
      | distinct (IChar _) x =
haftmann@20105
   364
          x
haftmann@20439
   365
      | distinct (ICase (((td, _), bs), _)) x =
haftmann@20439
   366
          x |> distinct td |> fold (fn (p, t) => distinct p #> distinct t) bs;
haftmann@20439
   367
  in is_some (fold distinct ts (SOME [])) end;
haftmann@20105
   368
haftmann@20439
   369
fun eta_expand (c as (_, (_, ty)), ts) k =
haftmann@19607
   370
  let
haftmann@20439
   371
    val j = length ts;
haftmann@19607
   372
    val l = k - j;
haftmann@19607
   373
    val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
haftmann@20439
   374
    val vs_tys = Name.names (fold Name.declare (fold add_varnames ts []) Name.context) "a" tys;
haftmann@20439
   375
  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
haftmann@19607
   376
haftmann@18304
   377
haftmann@18282
   378
haftmann@18170
   379
(** language module system - definitions, modules, transactions **)
haftmann@18170
   380
haftmann@18170
   381
(* type definitions *)
haftmann@18170
   382
haftmann@20105
   383
type funn = (iterm list * iterm) list * (sortcontext * itype);
haftmann@19167
   384
type datatyp = sortcontext * (string * itype list) list;
haftmann@18702
   385
haftmann@18170
   386
datatype def =
haftmann@19816
   387
    Bot
haftmann@18702
   388
  | Fun of funn
haftmann@20191
   389
  | Typesyn of sortcontext * itype
haftmann@19042
   390
  | Datatype of datatyp
haftmann@18380
   391
  | Datatypecons of string
haftmann@20389
   392
  | Class of class list * (vname * (string * (sortcontext * itype)) list)
haftmann@18380
   393
  | Classmember of class
haftmann@20389
   394
  | Classinst of (class * (string * (vname * sort) list))
haftmann@20389
   395
          * ((class * iclasslookup list) list
haftmann@20389
   396
        * (string * iterm) list);
haftmann@18170
   397
haftmann@18170
   398
datatype node = Def of def | Module of node Graph.T;
haftmann@18170
   399
type module = node Graph.T;
haftmann@18702
   400
type transact = Graph.key option * module;
haftmann@19816
   401
type 'dst transact_fin = 'dst * module;
haftmann@18231
   402
exception FAIL of string list * exn option;
haftmann@18170
   403
haftmann@19597
   404
val eq_def = (op =) : def * def -> bool;
haftmann@18170
   405
haftmann@18170
   406
(* simple diagnosis *)
haftmann@18170
   407
haftmann@19816
   408
fun pretty_def Bot =
haftmann@19816
   409
      Pretty.str "<Bot>"
haftmann@19341
   410
  | pretty_def (Fun (eqs, (sortctxt, ty))) =
wenzelm@18812
   411
      Pretty.enum " |" "" "" (
haftmann@18170
   412
        map (fn (ps, body) =>
haftmann@18170
   413
          Pretty.block [
haftmann@20105
   414
            Pretty.enum "," "[" "]" (map pretty_iterm ps),
haftmann@18170
   415
            Pretty.str " |->",
haftmann@18170
   416
            Pretty.brk 1,
haftmann@20105
   417
            pretty_iterm body,
haftmann@18170
   418
            Pretty.str "::",
haftmann@19341
   419
            pretty_sortcontext sortctxt,
haftmann@19341
   420
            Pretty.str "/",
haftmann@18170
   421
            pretty_itype ty
haftmann@18170
   422
          ]) eqs
haftmann@18170
   423
        )
haftmann@18172
   424
  | pretty_def (Typesyn (vs, ty)) =
haftmann@18170
   425
      Pretty.block [
haftmann@19341
   426
        pretty_sortcontext vs,
haftmann@18170
   427
        Pretty.str " |=> ",
haftmann@18170
   428
        pretty_itype ty
haftmann@18170
   429
      ]
haftmann@19038
   430
  | pretty_def (Datatype (vs, cs)) =
haftmann@18170
   431
      Pretty.block [
haftmann@19341
   432
        pretty_sortcontext vs,
haftmann@18170
   433
        Pretty.str " |=> ",
haftmann@18852
   434
        Pretty.enum " |" "" ""
haftmann@18850
   435
          (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
haftmann@19038
   436
            (Pretty.str c :: map pretty_itype tys)) cs)
haftmann@18170
   437
      ]
haftmann@18380
   438
  | pretty_def (Datatypecons dtname) =
haftmann@18380
   439
      Pretty.str ("cons " ^ dtname)
haftmann@19038
   440
  | pretty_def (Class (supcls, (v, mems))) =
haftmann@18170
   441
      Pretty.block [
haftmann@20386
   442
        Pretty.str ("class var " ^ v ^ " extending "),
wenzelm@18812
   443
        Pretty.enum "," "[" "]" (map Pretty.str supcls),
haftmann@18282
   444
        Pretty.str " with ",
haftmann@18852
   445
        Pretty.enum "," "[" "]"
haftmann@18850
   446
          (map (fn (m, (_, ty)) => Pretty.block
haftmann@19038
   447
            [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
haftmann@18231
   448
      ]
haftmann@18380
   449
  | pretty_def (Classmember clsname) =
haftmann@18231
   450
      Pretty.block [
haftmann@18231
   451
        Pretty.str "class member belonging to ",
haftmann@18282
   452
        Pretty.str clsname
haftmann@18231
   453
      ]
haftmann@20389
   454
  | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
haftmann@18231
   455
      Pretty.block [
haftmann@18231
   456
        Pretty.str "class instance (",
haftmann@18282
   457
        Pretty.str clsname,
haftmann@18231
   458
        Pretty.str ", (",
haftmann@18231
   459
        Pretty.str tyco,
haftmann@18231
   460
        Pretty.str ", ",
haftmann@18852
   461
        Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
haftmann@18850
   462
          map Pretty.str o snd) arity),
haftmann@18515
   463
        Pretty.str "))"
haftmann@20389
   464
      ];
haftmann@18170
   465
haftmann@18170
   466
fun pretty_module modl =
haftmann@18170
   467
  let
haftmann@18170
   468
    fun pretty (name, Module modl) =
haftmann@18170
   469
          Pretty.block (
haftmann@18170
   470
            Pretty.str ("module " ^ name ^ " {")
haftmann@18170
   471
            :: Pretty.brk 1
haftmann@18170
   472
            :: Pretty.chunks (map pretty (AList.make (Graph.get_node modl)
wenzelm@19482
   473
                 (Graph.strong_conn modl |> flat |> rev)))
haftmann@18170
   474
            :: Pretty.str "}" :: nil
haftmann@18170
   475
          )
haftmann@18170
   476
      | pretty (name, Def def) =
haftmann@18170
   477
          Pretty.block [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def]
haftmann@18170
   478
  in pretty ("//", Module modl) end;
haftmann@18170
   479
haftmann@18360
   480
fun pretty_deps modl =
haftmann@18360
   481
  let
haftmann@18360
   482
    fun one_node key =
haftmann@18380
   483
      let
haftmann@18380
   484
        val preds_ = Graph.imm_preds modl key;
haftmann@18380
   485
        val succs_ = Graph.imm_succs modl key;
haftmann@18380
   486
        val mutbs = gen_inter (op =) (preds_, succs_);
wenzelm@19300
   487
        val preds = subtract (op =) mutbs preds_;
wenzelm@19300
   488
        val succs = subtract (op =) mutbs succs_;
haftmann@18380
   489
      in
haftmann@18380
   490
        (Pretty.block o Pretty.fbreaks) (
haftmann@18380
   491
          Pretty.str key
haftmann@18380
   492
          :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
haftmann@18380
   493
          @ map (fn s => Pretty.str ("<-- " ^ s)) preds
haftmann@18380
   494
          @ map (fn s => Pretty.str ("--> " ^ s)) succs
haftmann@18850
   495
          @ (the_list oo Option.mapPartial)
haftmann@18850
   496
            ((fn Module modl' => SOME (pretty_deps modl')
haftmann@18850
   497
               | _ => NONE) o Graph.get_node modl) (SOME key)
haftmann@18380
   498
        )
haftmann@18380
   499
      end
haftmann@18360
   500
  in
haftmann@18360
   501
    modl
haftmann@18360
   502
    |> Graph.strong_conn
wenzelm@19482
   503
    |> flat
haftmann@18360
   504
    |> rev
haftmann@18360
   505
    |> map one_node
haftmann@18360
   506
    |> Pretty.chunks
haftmann@18360
   507
  end;
haftmann@18360
   508
haftmann@18170
   509
haftmann@18170
   510
(* name handling *)
haftmann@18170
   511
haftmann@18170
   512
fun dest_name name =
haftmann@18170
   513
  let
haftmann@18170
   514
    val name' = NameSpace.unpack name
haftmann@18170
   515
    val (name'', name_base) = split_last name'
haftmann@18170
   516
    val (modl, shallow) = split_last name''
haftmann@18170
   517
  in (modl, NameSpace.pack [shallow, name_base]) end
haftmann@20389
   518
  handle Empty => error ("Not a qualified name: " ^ quote name);
haftmann@18170
   519
haftmann@18516
   520
fun has_nsp name shallow =
haftmann@18516
   521
  NameSpace.is_qualified name
haftmann@18516
   522
  andalso let
haftmann@18516
   523
    val name' = NameSpace.unpack name
haftmann@18516
   524
    val (name'', _) = split_last name'
haftmann@18516
   525
    val (_, shallow') = split_last name''
haftmann@18516
   526
  in shallow' = shallow end;
haftmann@18516
   527
haftmann@18170
   528
fun dest_modl (Module m) = m;
haftmann@18170
   529
fun dest_def (Def d) = d;
haftmann@18170
   530
haftmann@18170
   531
haftmann@18170
   532
(* modules *)
haftmann@18170
   533
haftmann@18170
   534
val empty_module = Graph.empty; (*read: "depends on"*)
haftmann@18170
   535
haftmann@18170
   536
fun get_def modl name =
haftmann@18170
   537
  case dest_name name
haftmann@18170
   538
   of (modlname, base) =>
haftmann@18170
   539
        let
haftmann@18170
   540
          fun get (Module node) [] =
haftmann@18170
   541
                (dest_def o Graph.get_node node) base
haftmann@18170
   542
            | get (Module node) (m::ms) =
haftmann@18170
   543
                get (Graph.get_node node m) ms
haftmann@18170
   544
        in get (Module modl) modlname end;
haftmann@18170
   545
haftmann@19816
   546
fun is_def modl name =
haftmann@19816
   547
  case try (get_def modl) name
haftmann@19816
   548
   of NONE => false
haftmann@19816
   549
    | SOME Bot => false
haftmann@19816
   550
    | _ => true;
haftmann@19816
   551
haftmann@18170
   552
fun add_def (name, def) =
haftmann@18170
   553
  let
haftmann@18170
   554
    val (modl, base) = dest_name name;
haftmann@18170
   555
    fun add [] =
haftmann@18170
   556
          Graph.new_node (base, Def def)
haftmann@18170
   557
      | add (m::ms) =
haftmann@18170
   558
          Graph.default_node (m, Module empty_module)
haftmann@18170
   559
          #> Graph.map_node m (Module o add ms o dest_modl)
haftmann@18170
   560
  in add modl end;
haftmann@18170
   561
haftmann@19816
   562
fun map_def name f =
haftmann@19816
   563
  let
haftmann@19816
   564
    val (modl, base) = dest_name name;
haftmann@19816
   565
    fun mapp [] =
haftmann@19816
   566
          Graph.map_node base (Def o f o dest_def)
haftmann@19816
   567
      | mapp (m::ms) =
haftmann@19816
   568
          Graph.map_node m (Module o mapp ms o dest_modl)
haftmann@19816
   569
  in mapp modl end;
haftmann@19816
   570
haftmann@19816
   571
fun ensure_bot name =
haftmann@19816
   572
  let
haftmann@19816
   573
    val (modl, base) = dest_name name;
haftmann@19816
   574
    fun ensure [] module =
haftmann@19816
   575
          (case try (Graph.get_node module) base
haftmann@19816
   576
           of NONE =>
haftmann@19816
   577
                module
haftmann@19816
   578
                |> Graph.new_node (base, Def Bot)
haftmann@20389
   579
            | SOME (Module _) => error ("Module already present: " ^ quote name)
haftmann@19816
   580
            | _ => module)
haftmann@19816
   581
      | ensure (m::ms) module =
haftmann@19816
   582
          module
haftmann@19816
   583
          |> Graph.default_node (m, Module empty_module)
haftmann@19816
   584
          |> Graph.map_node m (Module o ensure ms o dest_modl)
haftmann@19816
   585
  in ensure modl end;
haftmann@19816
   586
haftmann@19816
   587
fun add_def_incr strict (name, Bot) module =
haftmann@19816
   588
      (case try (get_def module) name
haftmann@20389
   589
       of NONE => if strict then error "Attempted to add Bot to module"
haftmann@19816
   590
            else map_def name (K Bot) module
haftmann@20389
   591
        | SOME Bot => if strict then error "Attempted to add Bot to module"
haftmann@19816
   592
            else map_def name (K Bot) module
haftmann@19816
   593
        | SOME _ => module)
haftmann@19816
   594
  | add_def_incr _ (name, def) module =
haftmann@19816
   595
      (case try (get_def module) name
haftmann@19816
   596
       of NONE => add_def (name, def) module
haftmann@19816
   597
        | SOME Bot => map_def name (K def) module
haftmann@19816
   598
        | SOME def' => if eq_def (def, def')
haftmann@19816
   599
            then module
haftmann@20389
   600
            else error ("Tried to overwrite definition " ^ quote name));
haftmann@19816
   601
haftmann@18170
   602
fun add_dep (name1, name2) modl =
haftmann@18170
   603
  if name1 = name2 then modl
haftmann@18170
   604
  else
haftmann@18170
   605
    let
haftmann@18170
   606
      val m1 = dest_name name1 |> apsnd single |> (op @);
haftmann@18170
   607
      val m2 = dest_name name2 |> apsnd single |> (op @);
haftmann@20105
   608
      val (ms, (r1, r2)) = chop_prefix (op =) (m1, m2);
haftmann@20105
   609
      val (ms, (s1::r1, s2::r2)) = chop_prefix (op =) (m1, m2);
haftmann@18170
   610
      val add_edge =
haftmann@18170
   611
        if null r1 andalso null r2
haftmann@18170
   612
        then Graph.add_edge
haftmann@19785
   613
        else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
haftmann@19884
   614
          handle Graph.CYCLES _ =>
haftmann@20389
   615
            error ("Adding dependency "
haftmann@19884
   616
              ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
haftmann@18170
   617
      fun add [] node =
haftmann@18170
   618
            node
haftmann@18170
   619
            |> add_edge (s1, s2)
haftmann@18170
   620
        | add (m::ms) node =
haftmann@18170
   621
            node
haftmann@18170
   622
            |> Graph.map_node m (Module o add ms o dest_modl);
haftmann@18170
   623
    in add ms modl end;
haftmann@18170
   624
haftmann@18170
   625
fun merge_module modl12 =
haftmann@18170
   626
  let
wenzelm@19025
   627
    fun join_module _ (Module m1, Module m2) =
wenzelm@19025
   628
          Module (merge_module (m1, m2))
wenzelm@19025
   629
      | join_module name (Def d1, Def d2) =
haftmann@19884
   630
          if eq_def (d1, d2) then Def d1 else Def Bot
wenzelm@19025
   631
      | join_module name _ = raise Graph.DUP name
wenzelm@19025
   632
  in Graph.join join_module modl12 end;
haftmann@18170
   633
haftmann@19042
   634
fun diff_module modl12 =
haftmann@19042
   635
  let
haftmann@20191
   636
    fun diff_entry prefix modl2 (name, Def def1) =
haftmann@19042
   637
          let
haftmann@19042
   638
            val e2 = try (Graph.get_node modl2) name
haftmann@19042
   639
          in if is_some e2 andalso eq_def (def1, (dest_def o the) e2)
haftmann@19042
   640
            then I
haftmann@19042
   641
            else cons (NameSpace.pack (prefix @ [name]), def1)
haftmann@19042
   642
          end
haftmann@19042
   643
      | diff_entry prefix modl2 (name, Module modl1) =
haftmann@19042
   644
          diff_modl (prefix @ [name]) (modl1,
haftmann@19042
   645
            (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name)
haftmann@19042
   646
    and diff_modl prefix (modl1, modl2) =
haftmann@19042
   647
      fold (diff_entry prefix modl2)
wenzelm@19466
   648
        ((AList.make (Graph.get_node modl1) o flat o Graph.strong_conn) modl1)
haftmann@19042
   649
  in diff_modl [] modl12 [] end;
haftmann@19042
   650
haftmann@19884
   651
fun project_module names modl =
haftmann@18335
   652
  let
haftmann@18335
   653
    datatype pathnode = PN of (string list * (string * pathnode) list);
haftmann@18335
   654
    fun mk_ipath ([], base) (PN (defs, modls)) =
haftmann@18335
   655
          PN (base :: defs, modls)
haftmann@18335
   656
      | mk_ipath (n::ns, base) (PN (defs, modls)) =
haftmann@18335
   657
          modls
haftmann@18335
   658
          |> AList.default (op =) (n, PN ([], []))
haftmann@18335
   659
          |> AList.map_entry (op =) n (mk_ipath (ns, base))
haftmann@18335
   660
          |> (pair defs #> PN);
haftmann@18335
   661
    fun select (PN (defs, modls)) (Module module) =
haftmann@18335
   662
      module
haftmann@20191
   663
      |> Graph.project (member (op =) ((*!*) Graph.all_succs module (defs @ map fst modls)))
haftmann@18335
   664
      |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
haftmann@18335
   665
      |> Module;
haftmann@18335
   666
  in
haftmann@18335
   667
    Module modl
haftmann@18850
   668
    |> select (fold (mk_ipath o dest_name)
haftmann@18850
   669
         (filter NameSpace.is_qualified names) (PN ([], [])))
haftmann@18335
   670
    |> dest_modl
haftmann@18335
   671
  end;
haftmann@18170
   672
haftmann@19884
   673
fun purge_module names modl =
haftmann@18702
   674
  let
haftmann@19884
   675
    fun split_names names =
haftmann@19884
   676
      fold
haftmann@19884
   677
        (fn ([], name) => apfst (cons name)
haftmann@19884
   678
          | (m::ms, name) => apsnd (AList.default (op =) (m : string, [])
haftmann@19884
   679
              #> AList.map_entry (op =) m (cons (ms, name))))
haftmann@19884
   680
        names ([], []);
haftmann@19884
   681
    fun purge names (Module modl) =
haftmann@19884
   682
      let
haftmann@19884
   683
        val (ndefs, nmodls) = split_names names;
haftmann@19884
   684
      in
haftmann@20191
   685
        modl
haftmann@19884
   686
        |> Graph.del_nodes (Graph.all_preds modl ndefs)
haftmann@20191
   687
        |> Graph.del_nodes ndefs
haftmann@20191
   688
        |> Graph.del_nodes (Graph.all_preds modl (map fst nmodls))
haftmann@19884
   689
        |> fold (fn (nmodl, names') => Graph.map_node nmodl (purge names')) nmodls
haftmann@19884
   690
        |> Module
haftmann@19884
   691
      end;
haftmann@18702
   692
  in
haftmann@19884
   693
    Module modl
haftmann@19884
   694
    |> purge (map dest_name names)
haftmann@19884
   695
    |> dest_modl
haftmann@18702
   696
  end;
haftmann@18702
   697
haftmann@20428
   698
fun flat_module modl =
haftmann@20428
   699
  maps (
haftmann@20428
   700
   fn (name, Module modl) => map (apfst (NameSpace.append name)) (flat_module modl)
haftmann@20428
   701
    | (name, Def def) => [(name, def)]
haftmann@20428
   702
  ) ((AList.make (Graph.get_node modl) o flat o Graph.strong_conn) modl)
haftmann@20428
   703
haftmann@20428
   704
(*
haftmann@20428
   705
fun flat_funs_datatypes modl =
haftmann@20428
   706
  map (
haftmann@20428
   707
   fn def as (_, Datatype _) => def
haftmann@20428
   708
    | (name, Fun (eqs, (sctxt, ty))) => let
haftmann@20428
   709
          val vs = fold (fn (rhs, lhs) => fold add_varnames rhs #> add_varnames lhs) eqs [];
haftmann@20428
   710
          fun fold_map_snd f (x, ys) = fold_map f ys #-> (fn zs => pair (x, zs));
haftmann@20428
   711
          fun all_ops_of class = [] : (class * (string * itype) list) list
haftmann@20428
   712
            (*FIXME; itype within current context*);
haftmann@20428
   713
          fun name_ops class = 
haftmann@20428
   714
            (fold_map o fold_map_snd)
haftmann@20428
   715
              (fn (c, ty) => Name.variants [c] #-> (fn [v] => pair (c, (ty, v)))) (all_ops_of class);
haftmann@20428
   716
          (*FIXME: should contain superclasses only once*)
haftmann@20428
   717
          val (octxt, _) = (fold_map o fold_map_snd) name_ops sctxt
haftmann@20428
   718
            (Name.make_context vs);
haftmann@20428
   719
          (* --> (iterm * itype) list *)
haftmann@20428
   720
          fun flat_classlookup (Instance (inst, lss)) =
haftmann@20428
   721
                (case get_def modl inst
haftmann@20428
   722
                 of (Classinst (_, (suparities, ops)))
haftmann@20428
   723
                      => maps (maps flat_classlookup o snd) suparities @ map (apsnd flat_iterm) ops
haftmann@20428
   724
                  | _ => error ("Bad instance: " ^ quote inst))
haftmann@20428
   725
            | flat_classlookup (Lookup (classes, (v, k))) =
haftmann@20428
   726
                let
haftmann@20428
   727
                  val parm_map = nth ((the o AList.lookup (op =) octxt) v)
haftmann@20428
   728
                    (if k = ~1 then 0 else k);
haftmann@20428
   729
                in map (apfst IVar o swap o snd) (case classes
haftmann@20428
   730
                 of class::_ => (the o AList.lookup (op =) parm_map) class
haftmann@20428
   731
                  | _ => (snd o hd) parm_map)
haftmann@20428
   732
                end
haftmann@20428
   733
          and flat_iterm (e as IConst (c, (lss, ty))) =
haftmann@20428
   734
                let
haftmann@20428
   735
                  val (es, tys) = split_list ((maps o maps) flat_classlookup lss)
haftmann@20428
   736
                in IConst (c, ([], tys `--> ty)) `$$ es end
haftmann@20428
   737
                (*FIXME Eliminierung von Projektionen*)
haftmann@20428
   738
            | flat_iterm (e as IVar _) =
haftmann@20428
   739
                e
haftmann@20428
   740
            | flat_iterm (e1 `$ e2) =
haftmann@20428
   741
                flat_iterm e1 `$ flat_iterm e2
haftmann@20428
   742
            | flat_iterm (v_ty `|-> e) =
haftmann@20428
   743
                v_ty `|-> flat_iterm e
haftmann@20428
   744
            | flat_iterm (INum (k, e)) =
haftmann@20428
   745
                INum (k, flat_iterm e)
haftmann@20428
   746
            | flat_iterm (IChar (s, e)) =
haftmann@20428
   747
                IChar (s, flat_iterm e)
haftmann@20428
   748
            | flat_iterm (ICase (((de, dty), es), e)) =
haftmann@20428
   749
                ICase (((flat_iterm de, dty), map (pairself flat_iterm) es), flat_iterm e);
haftmann@20428
   750
        in
haftmann@20428
   751
          (name, Fun (map (fn (lhs, rhs) => (map flat_iterm lhs, flat_iterm rhs)) eqs,
haftmann@20428
   752
            ([], maps ((maps o maps) (map (fst o snd) o snd) o snd) octxt `--> ty)))
haftmann@20428
   753
        end
haftmann@20428
   754
  ) (flat_module modl);
haftmann@20428
   755
*)
haftmann@20428
   756
haftmann@20191
   757
val add_deps_of_sortctxt =
haftmann@20191
   758
  fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort);
haftmann@20191
   759
haftmann@20191
   760
fun add_deps_of_classlookup (Instance (tyco, lss)) =
haftmann@20191
   761
      insert (op =) tyco
haftmann@20191
   762
      #> (fold o fold) add_deps_of_classlookup lss
haftmann@20191
   763
  | add_deps_of_classlookup (Lookup (clss, _)) =
haftmann@20191
   764
      fold (insert (op =)) clss;
haftmann@20191
   765
haftmann@20191
   766
fun add_deps_of_type (tyco `%% tys) =
haftmann@20191
   767
      insert (op =) tyco
haftmann@20191
   768
      #> fold add_deps_of_type tys
haftmann@20191
   769
  | add_deps_of_type  (ty1 `-> ty2) =
haftmann@20191
   770
      add_deps_of_type ty1
haftmann@20191
   771
      #> add_deps_of_type ty2
haftmann@20191
   772
  | add_deps_of_type (ITyVar v) =
haftmann@20191
   773
      I;
haftmann@20191
   774
haftmann@20191
   775
fun add_deps_of_term (IConst (c, (lss, ty))) =
haftmann@20191
   776
      insert (op =) c
haftmann@20191
   777
      #> add_deps_of_type ty
haftmann@20191
   778
      #> (fold o fold) add_deps_of_classlookup lss
haftmann@20191
   779
  | add_deps_of_term (IVar _) =
haftmann@20191
   780
      I
haftmann@20191
   781
  | add_deps_of_term (e1 `$ e2) =
haftmann@20191
   782
      add_deps_of_term e1 #> add_deps_of_term e2
haftmann@20191
   783
  | add_deps_of_term ((_, ty) `|-> e) =
haftmann@20191
   784
      add_deps_of_type ty
haftmann@20191
   785
      #> add_deps_of_term e
haftmann@20191
   786
  | add_deps_of_term (INum _) =
haftmann@20191
   787
      I
haftmann@20191
   788
  | add_deps_of_term (IChar (_, e)) =
haftmann@20191
   789
      add_deps_of_term e
haftmann@20191
   790
  | add_deps_of_term (ICase (_, e)) =
haftmann@20191
   791
      add_deps_of_term e;
haftmann@20191
   792
haftmann@20191
   793
fun deps_of Bot =
haftmann@20191
   794
      []
haftmann@20191
   795
  | deps_of (Fun (eqs, (sctxt, ty))) =
haftmann@20191
   796
      []
haftmann@20191
   797
      |> add_deps_of_sortctxt sctxt
haftmann@20191
   798
      |> add_deps_of_type ty
haftmann@20191
   799
      |> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
haftmann@20191
   800
  | deps_of (Typesyn (sctxt, ty)) =
haftmann@20191
   801
      []
haftmann@20191
   802
      |> add_deps_of_sortctxt sctxt
haftmann@20191
   803
      |> add_deps_of_type ty
haftmann@20191
   804
  | deps_of (Datatype (sctxt, cos)) =
haftmann@20191
   805
      []
haftmann@20191
   806
      |> add_deps_of_sortctxt sctxt
haftmann@20191
   807
      |> fold (fn (c, tys) => insert (op =) c #> fold add_deps_of_type tys) cos
haftmann@20191
   808
  | deps_of (Datatypecons dtco) =
haftmann@20191
   809
      [dtco]
haftmann@20191
   810
  | deps_of (Class (supclss, (_, memdecls))) =
haftmann@20191
   811
      []
haftmann@20191
   812
      |> fold (insert (op =)) supclss
haftmann@20191
   813
      |> fold (fn (name, (sctxt, ty)) =>
haftmann@20191
   814
            insert (op =) name
haftmann@20191
   815
            #> add_deps_of_sortctxt sctxt
haftmann@20191
   816
            #> add_deps_of_type ty
haftmann@20191
   817
      ) memdecls
haftmann@20191
   818
  | deps_of (Classmember class) =
haftmann@20191
   819
      [class]
haftmann@20389
   820
  | deps_of (Classinst ((class, (tyco, sctxt)), (suparities, memdefs))) =
haftmann@20191
   821
      []
haftmann@20191
   822
      |> insert (op =) class
haftmann@20191
   823
      |> insert (op =) tyco
haftmann@20191
   824
      |> add_deps_of_sortctxt sctxt
haftmann@20191
   825
      |> fold (fn (supclass, ls) =>
haftmann@20191
   826
            insert (op =) supclass
haftmann@20191
   827
            #> fold add_deps_of_classlookup ls
haftmann@20191
   828
      ) suparities
haftmann@20389
   829
      |> fold (fn (name, e) =>
haftmann@20191
   830
            insert (op =) name
haftmann@20389
   831
            #> add_deps_of_term e
haftmann@20389
   832
      ) memdefs;
haftmann@20191
   833
haftmann@20191
   834
fun delete_garbage hidden modl =
haftmann@20191
   835
  let
haftmann@20191
   836
    fun allnames modl =
haftmann@20191
   837
      let
haftmann@20191
   838
        val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
haftmann@20191
   839
        fun is_def (name, Module _) = NONE
haftmann@20191
   840
          | is_def (name, _) = SOME name;
haftmann@20191
   841
        fun is_modl (name, Module modl) = SOME (name, modl)
haftmann@20191
   842
          | is_modl (name, _) = NONE;
haftmann@20191
   843
        val defs = map_filter is_def entries;
haftmann@20191
   844
        val modls = map_filter is_modl entries;
haftmann@20191
   845
      in
haftmann@20191
   846
        defs
haftmann@20191
   847
        @ maps (fn (name, modl) => map (NameSpace.append name) (allnames modl)) modls
haftmann@20191
   848
      end;
haftmann@20191
   849
    fun alldeps modl =
haftmann@20191
   850
      let
haftmann@20191
   851
        val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
haftmann@20191
   852
        fun is_def (name, Module _) = NONE
haftmann@20191
   853
          | is_def (name, _) = SOME name;
haftmann@20191
   854
        fun is_modl (name, Module modl) = SOME (name, modl)
haftmann@20191
   855
          | is_modl (name, _) = NONE;
haftmann@20191
   856
        val defs = map_filter is_def entries;
haftmann@20191
   857
        val modls = map_filter is_modl entries;
haftmann@20191
   858
      in
haftmann@20191
   859
        maps (fn name => map (pair (name)) (Graph.imm_succs modl name)) defs
haftmann@20191
   860
        @ maps (fn (name, modl) => (map o pairself) (NameSpace.append name) (alldeps modl)) modls
haftmann@20191
   861
      end;
haftmann@20191
   862
    val names = subtract (op =) hidden (allnames modl);
haftmann@20353
   863
(*     val _ = writeln "HIDDEN";  *)
haftmann@20353
   864
(*     val _ = (writeln o commas) hidden;  *)
haftmann@20353
   865
(*     val _ = writeln "NAMES";  *)
haftmann@20353
   866
(*     val _ = (writeln o commas) names;  *)
haftmann@20191
   867
    fun is_bot name =
haftmann@20191
   868
      case get_def modl name of Bot => true | _ => false;
haftmann@20191
   869
    val bots = filter is_bot names;
haftmann@20191
   870
    val defs = filter (not o is_bot) names;
haftmann@20191
   871
    val expldeps =
haftmann@20191
   872
      Graph.empty
haftmann@20191
   873
      |> fold (fn name => Graph.new_node (name, ())) names
haftmann@20191
   874
      |> fold (fn name => fold (curry Graph.add_edge name)
haftmann@20191
   875
            (deps_of (get_def modl name) |> subtract (op =) hidden)) names
haftmann@20191
   876
    val bots' = fold (insert op =) bots (Graph.all_preds expldeps bots);
haftmann@20191
   877
    val selected = subtract (op =) bots' names;
haftmann@20191
   878
(*     val deps = filter (fn (x, y) => member (op =) selected x andalso member (op =) selected y)  *)
haftmann@20191
   879
    val adddeps = maps (fn (n, ns) => map (pair n) ns) (expldeps |> Graph.del_nodes bots' |> Graph.dest);
haftmann@20353
   880
(*    val _ = writeln "SELECTED";
haftmann@20191
   881
    val _ = (writeln o commas) selected;
haftmann@20191
   882
    val _ = writeln "DEPS";
haftmann@20353
   883
    val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps; *)
haftmann@20191
   884
  in
haftmann@20191
   885
    empty_module
haftmann@20191
   886
    |> fold (fn name => add_def (name, get_def modl name)) selected
haftmann@20191
   887
(*     |> fold ensure_bot (hidden @ bots')  *)
haftmann@20216
   888
    |> fold (fn (x, y) => ((*writeln ("adding " ^ x ^ " -> " ^ y);*) add_dep (x, y))) adddeps
haftmann@20191
   889
  end;
haftmann@20191
   890
haftmann@19884
   891
fun allimports_of modl =
haftmann@19884
   892
  let
haftmann@19884
   893
    fun imps_of prfx (Module modl) imps tab =
haftmann@19884
   894
          let
haftmann@19884
   895
            val this = NameSpace.pack prfx;
haftmann@19884
   896
            val name_con = (rev o Graph.strong_conn) modl;
haftmann@19884
   897
          in
haftmann@19884
   898
            tab
haftmann@19884
   899
            |> pair []
haftmann@19884
   900
            |> fold (fn names => fn (imps', tab) =>
haftmann@19884
   901
                tab
haftmann@20191
   902
                |> fold_map (fn name =>
haftmann@19884
   903
                     imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names
haftmann@19884
   904
                |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con
haftmann@20191
   905
            |-> (fn imps' =>
haftmann@19884
   906
               Symtab.update_new (this, imps' @ imps)
haftmann@19884
   907
            #> pair (this :: imps'))
haftmann@19884
   908
          end
haftmann@19884
   909
      | imps_of prfx (Def _) imps tab =
haftmann@19884
   910
          ([], tab);
haftmann@19884
   911
  in snd (imps_of [] (Module modl) [] Symtab.empty) end;
haftmann@19884
   912
haftmann@18702
   913
fun check_samemodule names =
haftmann@18702
   914
  fold (fn name =>
haftmann@18702
   915
    let
haftmann@18702
   916
      val modn = (fst o dest_name) name
haftmann@18702
   917
    in
haftmann@18702
   918
     fn NONE => SOME modn
haftmann@18850
   919
      | SOME mod' => if modn = mod' then SOME modn
haftmann@20386
   920
          else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
haftmann@18702
   921
    end
haftmann@18702
   922
  ) names NONE;
haftmann@18702
   923
haftmann@18702
   924
fun check_funeqs eqs =
haftmann@18702
   925
  (fold (fn (pats, _) =>
haftmann@18702
   926
    let
haftmann@18702
   927
      val l = length pats
haftmann@18702
   928
    in
haftmann@18702
   929
     fn NONE => SOME l
haftmann@18850
   930
      | SOME l' => if l = l' then SOME l
haftmann@20389
   931
          else error "Function definition with different number of arguments"
haftmann@18702
   932
    end
haftmann@18702
   933
  ) eqs NONE; eqs);
haftmann@18702
   934
haftmann@19816
   935
fun check_prep_def modl Bot =
haftmann@19816
   936
      Bot
haftmann@18702
   937
  | check_prep_def modl (Fun (eqs, d)) =
haftmann@18702
   938
      Fun (check_funeqs eqs, d)
haftmann@18702
   939
  | check_prep_def modl (d as Typesyn _) =
haftmann@18702
   940
      d
haftmann@19038
   941
  | check_prep_def modl (d as Datatype _) =
haftmann@19038
   942
      d
haftmann@18702
   943
  | check_prep_def modl (Datatypecons dtco) =
haftmann@20389
   944
      error "Attempted to add bare datatype constructor"
haftmann@19038
   945
  | check_prep_def modl (d as Class _) =
haftmann@19038
   946
      d
haftmann@18702
   947
  | check_prep_def modl (Classmember _) =
haftmann@20389
   948
      error "Attempted to add bare class member"
haftmann@20389
   949
  | check_prep_def modl (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
haftmann@18170
   950
      let
haftmann@19038
   951
        val Class (_, (v, membrs)) = get_def modl class;
haftmann@18702
   952
        val _ = if length memdefs > length memdefs
haftmann@20389
   953
          then error "Too many member definitions given"
haftmann@18702
   954
          else ();
haftmann@20389
   955
        fun check_memdef (m, _) =
haftmann@20389
   956
          if AList.defined (op =) memdefs m
haftmann@20389
   957
          then () else error ("Missing definition for member " ^ quote m);
haftmann@20389
   958
        val _ = map check_memdef memdefs;
haftmann@20389
   959
      in d end
haftmann@19213
   960
  | check_prep_def modl Classinstmember =
haftmann@20389
   961
      error "Attempted to add bare class instance member";
haftmann@18170
   962
haftmann@19038
   963
fun postprocess_def (name, Datatype (_, constrs)) =
haftmann@18702
   964
      (check_samemodule (name :: map fst constrs);
haftmann@18702
   965
      fold (fn (co, _) =>
haftmann@19816
   966
        add_def_incr true (co, Datatypecons name)
haftmann@18702
   967
        #> add_dep (co, name)
haftmann@18702
   968
        #> add_dep (name, co)
haftmann@18702
   969
      ) constrs
haftmann@18702
   970
      )
haftmann@19038
   971
  | postprocess_def (name, Class (_, (_, membrs))) =
haftmann@18702
   972
      (check_samemodule (name :: map fst membrs);
haftmann@18702
   973
      fold (fn (m, _) =>
haftmann@19816
   974
        add_def_incr true (m, Classmember name)
haftmann@18702
   975
        #> add_dep (m, name)
haftmann@18702
   976
        #> add_dep (name, m)
haftmann@18702
   977
      ) membrs
haftmann@18702
   978
      )
haftmann@18702
   979
  | postprocess_def _ =
haftmann@18702
   980
      I;
haftmann@18380
   981
haftmann@19884
   982
haftmann@19884
   983
(* transaction protocol *)
haftmann@18170
   984
haftmann@19816
   985
fun ensure_def defgen strict msg name (dep, modl) =
haftmann@18170
   986
  let
haftmann@20389
   987
    (*FIXME represent dependencies as tuple (name, name -> string), for better error msgs*)
haftmann@19816
   988
    val msg' = (case dep
haftmann@18702
   989
     of NONE => msg
haftmann@19884
   990
      | SOME dep => msg ^ ", required for " ^ quote dep)
haftmann@19816
   991
      ^ (if strict then " (strict)" else " (non-strict)");
haftmann@18702
   992
    fun add_dp NONE = I
haftmann@18702
   993
      | add_dp (SOME dep) =
haftmann@19341
   994
          debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
haftmann@18702
   995
          #> add_dep (dep, name);
haftmann@18702
   996
    fun prep_def def modl =
haftmann@18702
   997
      (check_prep_def modl def, modl);
haftmann@19816
   998
    fun invoke_generator name defgen modl =
haftmann@20191
   999
      if ! soft_exc (*that "!" isn't a "not"...*)
haftmann@19956
  1000
      then defgen name (SOME name, modl)
haftmann@19956
  1001
        handle FAIL (msgs, exc) =>
haftmann@19956
  1002
                if strict then raise FAIL (msg' :: msgs, exc)
haftmann@19956
  1003
                else (Bot, modl)
haftmann@20191
  1004
             | e => raise
haftmann@19956
  1005
                FAIL (["definition generator for " ^ quote name, msg'], SOME e)
haftmann@19956
  1006
      else defgen name (SOME name, modl)
haftmann@19956
  1007
        handle FAIL (msgs, exc) =>
haftmann@19884
  1008
              if strict then raise FAIL (msg' :: msgs, exc)
haftmann@19956
  1009
              else (Bot, modl);
haftmann@18170
  1010
  in
haftmann@18170
  1011
    modl
haftmann@18702
  1012
    |> (if can (get_def modl) name
haftmann@18702
  1013
        then
haftmann@19341
  1014
          debug_msg (fn _ => "asserting node " ^ quote name)
haftmann@18702
  1015
          #> add_dp dep
haftmann@18702
  1016
        else
haftmann@19816
  1017
          debug_msg (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
haftmann@19816
  1018
          #> ensure_bot name
haftmann@18702
  1019
          #> add_dp dep
haftmann@19341
  1020
          #> debug_msg (fn _ => "creating node " ^ quote name)
haftmann@19816
  1021
          #> invoke_generator name defgen
haftmann@18702
  1022
          #-> (fn def => prep_def def)
haftmann@18702
  1023
          #-> (fn def =>
haftmann@19341
  1024
             debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
haftmann@19341
  1025
          #> debug_msg (fn _ => "adding")
haftmann@19816
  1026
          #> add_def_incr strict (name, def)
haftmann@19341
  1027
          #> debug_msg (fn _ => "postprocessing")
haftmann@18702
  1028
          #> postprocess_def (name, def)
haftmann@19341
  1029
          #> debug_msg (fn _ => "adding done")
haftmann@18702
  1030
       ))
haftmann@18702
  1031
    |> pair dep
haftmann@18170
  1032
  end;
haftmann@18170
  1033
haftmann@19884
  1034
fun succeed some (_, modl) = (some, modl);
haftmann@19884
  1035
haftmann@19884
  1036
fun fail msg (_, modl) = raise FAIL ([msg], NONE);
haftmann@19884
  1037
haftmann@19884
  1038
fun message msg f trns =
haftmann@19884
  1039
  f trns handle FAIL (msgs, exc) =>
haftmann@19884
  1040
    raise FAIL (msg :: msgs, exc);
haftmann@19884
  1041
haftmann@18963
  1042
fun start_transact init f modl =
haftmann@18231
  1043
  let
haftmann@18963
  1044
    fun handle_fail f x =
haftmann@18963
  1045
      (f x
haftmann@18231
  1046
      handle FAIL (msgs, NONE) =>
haftmann@20389
  1047
        (error o cat_lines) ("Code generation failed, while:" :: msgs))
haftmann@18231
  1048
      handle FAIL (msgs, SOME e) =>
haftmann@20389
  1049
        ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e);
haftmann@18231
  1050
  in
haftmann@19884
  1051
    modl
haftmann@19884
  1052
    |> (if is_some init then ensure_bot (the init) else I)
haftmann@19884
  1053
    |> pair init
haftmann@18231
  1054
    |> handle_fail f
haftmann@19884
  1055
    |-> (fn x => fn (_, modl) => (x, modl))
haftmann@18231
  1056
  end;
haftmann@18172
  1057
haftmann@20216
  1058
fun add_eval_def (shallow, e) modl =
haftmann@20191
  1059
  let
haftmann@20216
  1060
    val name = "VALUE";
haftmann@20216
  1061
    val sname = NameSpace.pack [shallow, name];
haftmann@20191
  1062
  in
haftmann@20191
  1063
    modl
haftmann@20216
  1064
    |> add_def (sname, Fun ([([], e)], ([("a", [])], ITyVar "a")))
haftmann@20216
  1065
    |> fold (curry add_dep sname) (add_deps_of_term e [])
haftmann@20191
  1066
    |> pair name
haftmann@20191
  1067
  end;
haftmann@18172
  1068
haftmann@18335
  1069
haftmann@20389
  1070
(** eliminating classes in definitions **)
haftmann@20389
  1071
haftmann@20389
  1072
fun elim_classes modl (eqs, (sortctxt, ty)) =
haftmann@20389
  1073
  let
haftmann@20389
  1074
    fun elim_expr _ = ();
haftmann@20389
  1075
  in (error ""; (eqs, ty)) end;
haftmann@20389
  1076
haftmann@18216
  1077
(** generic serialization **)
haftmann@18216
  1078
haftmann@18216
  1079
(* resolving *)
haftmann@18216
  1080
haftmann@18885
  1081
structure NameMangler = NameManglerFun (
haftmann@18885
  1082
  type ctxt = (string * string -> string) * (string -> string option);
haftmann@18516
  1083
  type src = string * string;
haftmann@18516
  1084
  val ord = prod_ord string_ord string_ord;
haftmann@18963
  1085
  fun mk (postprocess, validate) ((shallow, name), 0) =
haftmann@18963
  1086
        let
haftmann@18963
  1087
          val name' = postprocess (shallow, name);
haftmann@18963
  1088
        in case validate name'
haftmann@18963
  1089
         of NONE => name'
haftmann@18963
  1090
          | _ => mk (postprocess, validate) ((shallow, name), 1)
haftmann@18963
  1091
        end
haftmann@18963
  1092
    | mk (postprocess, validate) (("", name), i) =
haftmann@19150
  1093
        postprocess ("", name ^ replicate_string i "'")
haftmann@19150
  1094
        |> perhaps validate
haftmann@19150
  1095
    | mk (postprocess, validate) ((shallow, name), 1) =
haftmann@19150
  1096
        postprocess (shallow, shallow ^ "_" ^ name)
haftmann@18885
  1097
        |> perhaps validate
haftmann@18963
  1098
    | mk (postprocess, validate) ((shallow, name), i) =
haftmann@19150
  1099
        postprocess (shallow, name ^ replicate_string i "'")
haftmann@18516
  1100
        |> perhaps validate;
haftmann@18516
  1101
  fun is_valid _ _ = true;
haftmann@18516
  1102
  fun maybe_unique _ _ = NONE;
haftmann@20389
  1103
  fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
haftmann@18516
  1104
);
haftmann@18516
  1105
haftmann@18963
  1106
fun mk_deresolver module nsp_conn postprocess validate =
haftmann@18885
  1107
  let
haftmann@18885
  1108
    datatype tabnode = N of string * tabnode Symtab.table option;
haftmann@18885
  1109
    fun mk module manglers tab =
haftmann@18885
  1110
      let
haftmann@18885
  1111
        fun mk_name name =
haftmann@18885
  1112
          case NameSpace.unpack name
haftmann@18885
  1113
           of [n] => ("", n)
haftmann@18885
  1114
            | [s, n] => (s, n);
haftmann@18885
  1115
        fun in_conn (shallow, conn) =
haftmann@18885
  1116
          member (op = : string * string -> bool) conn shallow;
haftmann@18885
  1117
        fun add_name name =
haftmann@18885
  1118
          let
haftmann@18885
  1119
            val n as (shallow, _) = mk_name name;
haftmann@18885
  1120
          in
haftmann@18885
  1121
            AList.map_entry_yield in_conn shallow (
haftmann@18963
  1122
              NameMangler.declare (postprocess, validate) n
haftmann@18885
  1123
              #-> (fn n' => pair (name, n'))
haftmann@18963
  1124
            ) #> apfst the
haftmann@18885
  1125
          end;
haftmann@18885
  1126
        val (renamings, manglers') =
haftmann@18885
  1127
          fold_map add_name (Graph.keys module) manglers;
haftmann@18885
  1128
        fun extend_tab (n, n') =
haftmann@18885
  1129
          if (length o NameSpace.unpack) n = 1
haftmann@18885
  1130
          then
haftmann@18885
  1131
            Symtab.update_new
haftmann@18885
  1132
              (n, N (n', SOME (mk ((dest_modl o Graph.get_node module) n) manglers' Symtab.empty)))
haftmann@18885
  1133
          else
haftmann@18885
  1134
            Symtab.update_new (n, N (n', NONE));
haftmann@18885
  1135
      in fold extend_tab renamings tab end;
haftmann@18885
  1136
    fun get_path_name [] tab =
haftmann@18885
  1137
          ([], SOME tab)
haftmann@18885
  1138
      | get_path_name [p] tab =
haftmann@18885
  1139
          let
haftmann@18885
  1140
            val SOME (N (p', tab')) = Symtab.lookup tab p
haftmann@18885
  1141
          in ([p'], tab') end
haftmann@18885
  1142
      | get_path_name [p1, p2] tab =
haftmann@18919
  1143
          (case Symtab.lookup tab p1
haftmann@20191
  1144
           of SOME (N (p', SOME tab')) =>
haftmann@18885
  1145
                let
haftmann@18885
  1146
                  val (ps', tab'') = get_path_name [p2] tab'
haftmann@18885
  1147
                in (p' :: ps', tab'') end
haftmann@18885
  1148
            | NONE =>
haftmann@18885
  1149
                let
haftmann@18885
  1150
                  val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2])
haftmann@18919
  1151
                in ([p'], NONE) end)
haftmann@18885
  1152
      | get_path_name (p::ps) tab =
haftmann@18885
  1153
          let
haftmann@18885
  1154
            val SOME (N (p', SOME tab')) = Symtab.lookup tab p
haftmann@18885
  1155
            val (ps', tab'') = get_path_name ps tab'
haftmann@18885
  1156
          in (p' :: ps', tab'') end;
haftmann@18885
  1157
    fun deresolv tab prefix name =
haftmann@19341
  1158
      let
haftmann@20105
  1159
        val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
haftmann@18885
  1160
        val (_, SOME tab') = get_path_name common tab;
haftmann@18885
  1161
        val (name', _) = get_path_name rem tab';
haftmann@20428
  1162
      in NameSpace.pack name' end handle BIND => (error ("Missing name: " ^ quote name ^ ", in " ^ quote (NameSpace.pack prefix)));
haftmann@18885
  1163
  in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
haftmann@18885
  1164
haftmann@18216
  1165
haftmann@18216
  1166
(* serialization *)
haftmann@18216
  1167
haftmann@18963
  1168
fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module =
haftmann@18216
  1169
  let
haftmann@19884
  1170
    val imptab = allimports_of module;
haftmann@18963
  1171
    val resolver = mk_deresolver module nsp_conn postprocess validate;
haftmann@19038
  1172
    fun sresolver s = (resolver o NameSpace.unpack) s
haftmann@18702
  1173
    fun mk_name prfx name =
haftmann@18850
  1174
      let
haftmann@18850
  1175
        val name_qual = NameSpace.pack (prfx @ [name])
haftmann@18850
  1176
      in (name_qual, resolver prfx name_qual) end;
haftmann@20191
  1177
    fun is_bot (_, (Def Bot)) = true
haftmann@20191
  1178
      | is_bot _ = false;
haftmann@18756
  1179
    fun mk_contents prfx module =
wenzelm@19482
  1180
      map_filter (seri prfx)
haftmann@18850
  1181
        ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
haftmann@19816
  1182
    and seri prfx [(name, Module modl)] =
haftmann@19884
  1183
          seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))
haftmann@18850
  1184
            (mk_name prfx name, mk_contents (prfx @ [name]) modl)
haftmann@18756
  1185
      | seri prfx ds =
haftmann@20191
  1186
          case filter_out is_bot ds
haftmann@20191
  1187
           of [] => NONE
haftmann@20191
  1188
            | ds' => seri_defs sresolver (NameSpace.pack prfx)
haftmann@20191
  1189
                (map (fn (name, Def def) => (fst (mk_name prfx name), def (*|> tap (Pretty.writeln o pretty_def)*))) ds')
haftmann@18216
  1190
  in
haftmann@19937
  1191
    seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
haftmann@18850
  1192
      (("", name_root), (mk_contents [] module))
haftmann@18216
  1193
  end;
haftmann@18216
  1194
haftmann@18169
  1195
end; (* struct *)
haftmann@19136
  1196
wenzelm@19300
  1197
structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;