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