src/Tools/code/code_thingol.ML
author haftmann
Mon Dec 10 11:24:15 2007 +0100 (2007-12-10 ago)
changeset 25597 34860182b250
parent 25485 33840a854e63
child 25621 97ebdbdb0299
permissions -rw-r--r--
moved instance parameter management from class.ML to axclass.ML
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@24918
     6
Representation and translation.
haftmann@24219
     7
*)
haftmann@24219
     8
haftmann@24219
     9
infix 8 `%%;
haftmann@24219
    10
infixr 6 `->;
haftmann@24219
    11
infixr 6 `-->;
haftmann@24219
    12
infix 4 `$;
haftmann@24219
    13
infix 4 `$$;
haftmann@24219
    14
infixr 3 `|->;
haftmann@24219
    15
infixr 3 `|-->;
haftmann@24219
    16
haftmann@24219
    17
signature BASIC_CODE_THINGOL =
haftmann@24219
    18
sig
haftmann@24219
    19
  type vname = string;
haftmann@24219
    20
  datatype dict =
haftmann@24219
    21
      DictConst of string * dict list list
haftmann@24219
    22
    | DictVar of string list * (vname * (int * int));
haftmann@24219
    23
  datatype itype =
haftmann@24219
    24
      `%% of string * itype list
haftmann@24219
    25
    | ITyVar of vname;
haftmann@24591
    26
  type const = string * (dict list list * itype list (*types of arguments*))
haftmann@24219
    27
  datatype iterm =
haftmann@24591
    28
      IConst of const
haftmann@24219
    29
    | IVar of vname
haftmann@24219
    30
    | `$ of iterm * iterm
haftmann@24219
    31
    | `|-> of (vname * itype) * iterm
haftmann@24219
    32
    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@24219
    33
        (*((term, type), [(selector pattern, body term )]), primitive term)*)
haftmann@24219
    34
  val `-> : itype * itype -> itype;
haftmann@24219
    35
  val `--> : itype list * itype -> itype;
haftmann@24219
    36
  val `$$ : iterm * iterm list -> iterm;
haftmann@24219
    37
  val `|--> : (vname * itype) list * iterm -> iterm;
haftmann@24219
    38
  type typscheme = (vname * sort) list * itype;
haftmann@24219
    39
end;
haftmann@24219
    40
haftmann@24219
    41
signature CODE_THINGOL =
haftmann@24219
    42
sig
haftmann@24219
    43
  include BASIC_CODE_THINGOL;
haftmann@24219
    44
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
haftmann@24219
    45
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
haftmann@24219
    46
  val unfold_fun: itype -> itype list * itype;
haftmann@24219
    47
  val unfold_app: iterm -> iterm * iterm list;
haftmann@24219
    48
  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
haftmann@24219
    49
  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
haftmann@24219
    50
  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
haftmann@24219
    51
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
haftmann@24219
    52
  val unfold_const_app: iterm ->
haftmann@24219
    53
    ((string * (dict list list * itype list)) * iterm list) option;
haftmann@24219
    54
  val collapse_let: ((vname * itype) * iterm) * iterm
haftmann@24219
    55
    -> (iterm * itype) * (iterm * iterm) list;
haftmann@24219
    56
  val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
haftmann@24662
    57
  val contains_dictvar: iterm -> bool;
haftmann@24219
    58
  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    59
  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    60
  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
haftmann@24219
    61
haftmann@24918
    62
  datatype stmt =
haftmann@24219
    63
      Bot
haftmann@24591
    64
    | Fun of typscheme * ((iterm list * iterm) * thm) list
haftmann@24219
    65
    | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
    66
    | Datatypecons of string
haftmann@24811
    67
    | Class of vname * ((class * string) list * (string * itype) list)
haftmann@24219
    68
    | Classrel of class * class
haftmann@24837
    69
    | Classparam of class
haftmann@24219
    70
    | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
    71
          * ((class * (string * (string * dict list list))) list
haftmann@24591
    72
        * ((string * const) * thm) list);
haftmann@24918
    73
  type code = stmt Graph.T;
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@24219
    81
haftmann@24918
    82
  type transact;
haftmann@24918
    83
  val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
haftmann@24918
    84
    -> CodeFuncgr.T -> string -> transact -> string * transact;
haftmann@24918
    85
  val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
haftmann@24918
    86
    -> CodeFuncgr.T -> term -> transact -> string * transact;
haftmann@24918
    87
  val add_value_stmt: iterm * itype -> code -> code;
haftmann@24918
    88
  val transact: (transact -> 'a * transact) -> code -> 'a * code;
haftmann@24219
    89
end;
haftmann@24219
    90
haftmann@24219
    91
structure CodeThingol: CODE_THINGOL =
haftmann@24219
    92
struct
haftmann@24219
    93
haftmann@24219
    94
(** auxiliary **)
haftmann@24219
    95
haftmann@24219
    96
fun unfoldl dest x =
haftmann@24219
    97
  case dest x
haftmann@24219
    98
   of NONE => (x, [])
haftmann@24219
    99
    | SOME (x1, x2) =>
haftmann@24219
   100
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
haftmann@24219
   101
haftmann@24219
   102
fun unfoldr dest x =
haftmann@24219
   103
  case dest x
haftmann@24219
   104
   of NONE => ([], x)
haftmann@24219
   105
    | SOME (x1, x2) =>
haftmann@24219
   106
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
haftmann@24219
   107
haftmann@24219
   108
haftmann@24219
   109
(** language core - types, pattern, expressions **)
haftmann@24219
   110
haftmann@24219
   111
(* language representation *)
haftmann@24219
   112
haftmann@24219
   113
type vname = string;
haftmann@24219
   114
haftmann@24219
   115
datatype dict =
haftmann@24219
   116
    DictConst of string * dict list list
haftmann@24219
   117
  | DictVar of string list * (vname * (int * int));
haftmann@24219
   118
haftmann@24219
   119
datatype itype =
haftmann@24219
   120
    `%% of string * itype list
haftmann@24219
   121
  | ITyVar of vname;
haftmann@24219
   122
haftmann@24591
   123
type const = string * (dict list list * itype list (*types of arguments*))
haftmann@24591
   124
haftmann@24219
   125
datatype iterm =
haftmann@24591
   126
    IConst of const
haftmann@24219
   127
  | IVar of vname
haftmann@24219
   128
  | `$ of iterm * iterm
haftmann@24219
   129
  | `|-> of (vname * itype) * iterm
haftmann@24219
   130
  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
haftmann@24219
   131
    (*see also signature*)
haftmann@24219
   132
haftmann@24219
   133
(*
haftmann@24219
   134
  variable naming conventions
haftmann@24219
   135
haftmann@24219
   136
  bare names:
haftmann@24219
   137
    variable names          v
haftmann@24219
   138
    class names             class
haftmann@24219
   139
    type constructor names  tyco
haftmann@24219
   140
    datatype names          dtco
haftmann@24837
   141
    const names (general)   c (const)
haftmann@24219
   142
    constructor names       co
haftmann@24837
   143
    class parameter names   classparam
haftmann@24219
   144
    arbitrary name          s
haftmann@24219
   145
haftmann@24837
   146
    v, c, co, classparam also annotated with types etc.
haftmann@24219
   147
haftmann@24219
   148
  constructs:
haftmann@24219
   149
    sort                    sort
haftmann@24219
   150
    type parameters         vs
haftmann@24219
   151
    type                    ty
haftmann@24219
   152
    type schemes            tysm
haftmann@24219
   153
    term                    t
haftmann@24219
   154
    (term as pattern)       p
haftmann@24219
   155
    instance (class, tyco)  inst
haftmann@24219
   156
 *)
haftmann@24219
   157
haftmann@24219
   158
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
haftmann@24219
   159
val op `--> = Library.foldr (op `->);
haftmann@24219
   160
val op `$$ = Library.foldl (op `$);
haftmann@24219
   161
val op `|--> = Library.foldr (op `|->);
haftmann@24219
   162
haftmann@24219
   163
val unfold_fun = unfoldr
haftmann@24219
   164
  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
haftmann@24219
   165
    | _ => NONE);
haftmann@24219
   166
haftmann@24219
   167
val unfold_app = unfoldl
haftmann@24219
   168
  (fn op `$ t => SOME t
haftmann@24219
   169
    | _ => NONE);
haftmann@24219
   170
haftmann@24219
   171
val split_abs =
haftmann@24219
   172
  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
haftmann@24219
   173
        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
haftmann@24219
   174
    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
haftmann@24219
   175
    | _ => NONE);
haftmann@24219
   176
haftmann@24219
   177
val unfold_abs = unfoldr split_abs;
haftmann@24219
   178
haftmann@24219
   179
val split_let = 
haftmann@24219
   180
  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
haftmann@24219
   181
    | _ => NONE);
haftmann@24219
   182
haftmann@24219
   183
val unfold_let = unfoldr split_let;
haftmann@24219
   184
haftmann@24219
   185
fun unfold_const_app t =
haftmann@24219
   186
 case unfold_app t
haftmann@24219
   187
  of (IConst c, ts) => SOME (c, ts)
haftmann@24219
   188
   | _ => NONE;
haftmann@24219
   189
haftmann@24219
   190
fun fold_aiterms f (t as IConst _) = f t
haftmann@24219
   191
  | fold_aiterms f (t as IVar _) = f t
haftmann@24219
   192
  | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
haftmann@24219
   193
  | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
haftmann@24219
   194
  | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
haftmann@24219
   195
haftmann@24219
   196
fun fold_constnames f =
haftmann@24219
   197
  let
haftmann@24219
   198
    fun add (IConst (c, _)) = f c
haftmann@24219
   199
      | add _ = I;
haftmann@24219
   200
  in fold_aiterms add end;
haftmann@24219
   201
haftmann@24219
   202
fun fold_varnames f =
haftmann@24219
   203
  let
haftmann@24219
   204
    fun add (IVar v) = f v
haftmann@24219
   205
      | add ((v, _) `|-> _) = f v
haftmann@24219
   206
      | add _ = I;
haftmann@24219
   207
  in fold_aiterms add end;
haftmann@24219
   208
haftmann@24219
   209
fun fold_unbound_varnames f =
haftmann@24219
   210
  let
haftmann@24219
   211
    fun add _ (IConst _) = I
haftmann@24219
   212
      | add vs (IVar v) = if not (member (op =) vs v) then f v else I
haftmann@24219
   213
      | add vs (t1 `$ t2) = add vs t1 #> add vs t2
haftmann@24219
   214
      | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
haftmann@24219
   215
      | add vs (ICase (_, t)) = add vs t;
haftmann@24219
   216
  in add [] end;
haftmann@24219
   217
haftmann@24219
   218
fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
haftmann@24219
   219
      let
haftmann@24219
   220
        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
haftmann@24219
   221
          b orelse v = w) t false;
haftmann@24219
   222
      in if v = w andalso forall (fn (t1, t2) =>
haftmann@24219
   223
        exists_v t1 orelse not (exists_v t2)) ds
haftmann@24219
   224
        then ((se, ty), ds)
haftmann@24219
   225
        else ((se, ty), [(IVar v, be)])
haftmann@24219
   226
      end
haftmann@24219
   227
  | collapse_let (((v, ty), se), be) =
haftmann@24219
   228
      ((se, ty), [(IVar v, be)])
haftmann@24219
   229
haftmann@24219
   230
fun eta_expand (c as (_, (_, tys)), ts) k =
haftmann@24219
   231
  let
haftmann@24219
   232
    val j = length ts;
haftmann@24219
   233
    val l = k - j;
haftmann@24219
   234
    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
haftmann@24219
   235
    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
haftmann@24219
   236
  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
haftmann@24219
   237
haftmann@24662
   238
fun contains_dictvar t =
haftmann@24662
   239
  let
haftmann@24662
   240
    fun contains (DictConst (_, dss)) = (fold o fold) contains dss
haftmann@24662
   241
      | contains (DictVar _) = K true;
haftmann@24662
   242
  in
haftmann@24662
   243
    fold_aiterms
haftmann@24662
   244
      (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
haftmann@24662
   245
  end;
haftmann@24662
   246
  
haftmann@24219
   247
haftmann@24219
   248
(** definitions, transactions **)
haftmann@24219
   249
haftmann@24219
   250
type typscheme = (vname * sort) list * itype;
haftmann@24918
   251
datatype stmt =
haftmann@24219
   252
    Bot
haftmann@24591
   253
  | Fun of typscheme * ((iterm list * iterm) * thm) list
haftmann@24219
   254
  | Datatype of (vname * sort) list * (string * itype list) list
haftmann@24219
   255
  | Datatypecons of string
haftmann@24811
   256
  | Class of vname * ((class * string) list * (string * itype) list)
haftmann@24219
   257
  | Classrel of class * class
haftmann@24837
   258
  | Classparam of class
haftmann@24219
   259
  | Classinst of (class * (string * (vname * sort) list))
haftmann@24219
   260
        * ((class * (string * (string * dict list list))) list
haftmann@24591
   261
      * ((string * const) * thm) list);
haftmann@24219
   262
haftmann@24918
   263
type code = stmt Graph.T;
haftmann@24219
   264
haftmann@24219
   265
haftmann@24219
   266
(* abstract code *)
haftmann@24219
   267
haftmann@24219
   268
val empty_code = Graph.empty : code; (*read: "depends on"*)
haftmann@24219
   269
haftmann@24219
   270
fun ensure_bot name = Graph.default_node (name, Bot);
haftmann@24219
   271
haftmann@24219
   272
fun add_def_incr (name, Bot) code =
haftmann@24219
   273
      (case the_default Bot (try (Graph.get_node code) name)
haftmann@24219
   274
       of Bot => error "Attempted to add Bot to code"
haftmann@24219
   275
        | _ => code)
haftmann@24219
   276
  | add_def_incr (name, def) code =
haftmann@24219
   277
      (case try (Graph.get_node code) name
haftmann@24219
   278
       of NONE => Graph.new_node (name, def) code
haftmann@24219
   279
        | SOME Bot => Graph.map_node name (K def) code
haftmann@24219
   280
        | SOME _ => error ("Tried to overwrite definition " ^ quote name));
haftmann@24219
   281
haftmann@24811
   282
fun add_dep (NONE, _) = I
haftmann@24811
   283
  | add_dep (SOME name1, name2) =
haftmann@24811
   284
      if name1 = name2 then I else Graph.add_edge (name1, name2);
haftmann@24219
   285
haftmann@24219
   286
val merge_code : code * code -> code = Graph.merge (K true);
haftmann@24219
   287
haftmann@24219
   288
fun project_code delete_empty_funs hidden raw_selected code =
haftmann@24219
   289
  let
haftmann@24219
   290
    fun is_empty_fun name = case Graph.get_node code name
haftmann@24381
   291
     of Fun (_, []) => true
haftmann@24219
   292
      | _ => false;
haftmann@24219
   293
    val names = subtract (op =) hidden (Graph.keys code);
haftmann@24219
   294
    val deleted = Graph.all_preds code (filter is_empty_fun names);
haftmann@24219
   295
    val selected = case raw_selected
haftmann@24219
   296
     of NONE => names |> subtract (op =) deleted 
haftmann@24219
   297
      | SOME sel => sel
haftmann@24219
   298
          |> delete_empty_funs ? subtract (op =) deleted
haftmann@24219
   299
          |> subtract (op =) hidden
haftmann@24219
   300
          |> Graph.all_succs code
haftmann@24219
   301
          |> delete_empty_funs ? subtract (op =) deleted
haftmann@24219
   302
          |> subtract (op =) hidden;
haftmann@24219
   303
  in
haftmann@24219
   304
    code
haftmann@24219
   305
    |> Graph.subgraph (member (op =) selected)
haftmann@24219
   306
  end;
haftmann@24219
   307
haftmann@24219
   308
fun empty_funs code =
haftmann@24381
   309
  Graph.fold (fn (name, (Fun (_, []), _)) => cons name
haftmann@24219
   310
               | _ => I) code [];
haftmann@24219
   311
haftmann@24219
   312
fun is_cons code name = case Graph.get_node code name
haftmann@24219
   313
 of Datatypecons _ => true
haftmann@24219
   314
  | _ => false;
haftmann@24219
   315
haftmann@24219
   316
haftmann@24219
   317
(* transaction protocol *)
haftmann@24219
   318
haftmann@24283
   319
type transact = Graph.key option * code;
haftmann@24283
   320
haftmann@24918
   321
fun ensure_stmt stmtgen name (dep, code) =
haftmann@24219
   322
  let
haftmann@24219
   323
    fun add_def false =
haftmann@24219
   324
          ensure_bot name
haftmann@24811
   325
          #> add_dep (dep, name)
haftmann@24918
   326
          #> curry stmtgen (SOME name)
haftmann@24252
   327
          ##> snd
haftmann@24811
   328
          #-> (fn def => add_def_incr (name, def))
haftmann@24219
   329
      | add_def true =
haftmann@24811
   330
          add_dep (dep, name);
haftmann@24219
   331
  in
haftmann@24219
   332
    code
haftmann@24219
   333
    |> add_def (can (Graph.get_node code) name)
haftmann@24219
   334
    |> pair dep
haftmann@24918
   335
    |> pair name
haftmann@24219
   336
  end;
haftmann@24219
   337
haftmann@24918
   338
fun transact f code =
haftmann@24252
   339
  (NONE, code)
haftmann@24252
   340
  |> f
haftmann@24252
   341
  |-> (fn x => fn (_, code) => (x, code));
haftmann@24219
   342
haftmann@24918
   343
haftmann@24918
   344
(* translation kernel *)
haftmann@24918
   345
haftmann@24918
   346
fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
haftmann@24918
   347
  let
haftmann@24918
   348
    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
wenzelm@24969
   349
    val cs = #params (AxClass.get_info thy class);
haftmann@24918
   350
    val class' = CodeName.class thy class;
haftmann@24918
   351
    val stmt_class =
haftmann@24918
   352
      fold_map (fn superclass => ensure_class thy algbr funcgr superclass
haftmann@24918
   353
        ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
haftmann@24918
   354
      ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
haftmann@24918
   355
        ##>> exprgen_typ thy algbr funcgr ty) cs
wenzelm@24969
   356
      #>> (fn info => Class (unprefix "'" Name.aT, info))
haftmann@24918
   357
  in
haftmann@24918
   358
    ensure_stmt stmt_class class'
haftmann@24918
   359
  end
haftmann@24918
   360
and ensure_classrel thy algbr funcgr (subclass, superclass) =
haftmann@24918
   361
  let
haftmann@24918
   362
    val classrel' = CodeName.classrel thy (subclass, superclass);
haftmann@24918
   363
    val stmt_classrel =
haftmann@24918
   364
      ensure_class thy algbr funcgr subclass
haftmann@24918
   365
      ##>> ensure_class thy algbr funcgr superclass
haftmann@24918
   366
      #>> Classrel;
haftmann@24918
   367
  in
haftmann@24918
   368
    ensure_stmt stmt_classrel classrel'
haftmann@24918
   369
  end
haftmann@24918
   370
and ensure_tyco thy algbr funcgr "fun" =
haftmann@24918
   371
      pair "fun"
haftmann@24918
   372
  | ensure_tyco thy algbr funcgr tyco =
haftmann@24918
   373
      let
haftmann@24918
   374
        val stmt_datatype =
haftmann@24918
   375
          let
haftmann@24918
   376
            val (vs, cos) = Code.get_datatype thy tyco;
haftmann@24918
   377
          in
haftmann@24918
   378
            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   379
            ##>> fold_map (fn (c, tys) =>
haftmann@24918
   380
              ensure_const thy algbr funcgr c
haftmann@24918
   381
              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
haftmann@24918
   382
            #>> Datatype
haftmann@24918
   383
          end;
haftmann@24918
   384
        val tyco' = CodeName.tyco thy tyco;
haftmann@24918
   385
      in
haftmann@24918
   386
        ensure_stmt stmt_datatype tyco'
haftmann@24918
   387
      end
haftmann@24918
   388
and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
haftmann@24918
   389
  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
haftmann@24918
   390
  #>> (fn sort => (unprefix "'" v, sort))
haftmann@24918
   391
and exprgen_typ thy algbr funcgr (TFree vs) =
haftmann@24918
   392
      exprgen_tyvar_sort thy algbr funcgr vs
haftmann@24918
   393
      #>> (fn (v, sort) => ITyVar v)
haftmann@24918
   394
  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
haftmann@24918
   395
      ensure_tyco thy algbr funcgr tyco
haftmann@24918
   396
      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
haftmann@24918
   397
      #>> (fn (tyco, tys) => tyco `%% tys)
haftmann@24918
   398
and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
haftmann@24918
   399
  let
haftmann@24918
   400
    val pp = Sign.pp thy;
haftmann@24918
   401
    datatype typarg =
haftmann@24918
   402
        Global of (class * string) * typarg list list
haftmann@24918
   403
      | Local of (class * class) list * (string * (int * sort));
haftmann@24918
   404
    fun class_relation (Global ((_, tyco), yss), _) class =
haftmann@24918
   405
          Global ((class, tyco), yss)
haftmann@24918
   406
      | class_relation (Local (classrels, v), subclass) superclass =
haftmann@24918
   407
          Local ((subclass, superclass) :: classrels, v);
haftmann@24918
   408
    fun type_constructor tyco yss class =
haftmann@24918
   409
      Global ((class, tyco), (map o map) fst yss);
haftmann@24918
   410
    fun type_variable (TFree (v, sort)) =
haftmann@24918
   411
      let
haftmann@24918
   412
        val sort' = proj_sort sort;
haftmann@24918
   413
      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
haftmann@24918
   414
    val typargs = Sorts.of_sort_derivation pp algebra
haftmann@24918
   415
      {class_relation = class_relation, type_constructor = type_constructor,
haftmann@24918
   416
       type_variable = type_variable}
haftmann@24918
   417
      (ty_ctxt, proj_sort sort_decl);
haftmann@24918
   418
    fun mk_dict (Global (inst, yss)) =
haftmann@24918
   419
          ensure_inst thy algbr funcgr inst
haftmann@24918
   420
          ##>> (fold_map o fold_map) mk_dict yss
haftmann@24918
   421
          #>> (fn (inst, dss) => DictConst (inst, dss))
haftmann@24918
   422
      | mk_dict (Local (classrels, (v, (k, sort)))) =
haftmann@24918
   423
          fold_map (ensure_classrel thy algbr funcgr) classrels
haftmann@24918
   424
          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
haftmann@24918
   425
  in
haftmann@24918
   426
    fold_map mk_dict typargs
haftmann@24918
   427
  end
haftmann@24918
   428
and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
haftmann@24918
   429
  let
wenzelm@25042
   430
    val ty_decl = Consts.the_type consts c;
haftmann@24918
   431
    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
haftmann@24918
   432
    val sorts = map (snd o dest_TVar) tys_decl;
haftmann@24918
   433
  in
haftmann@24918
   434
    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
haftmann@24918
   435
  end
haftmann@24918
   436
and exprgen_eq thy algbr funcgr thm =
haftmann@24918
   437
  let
haftmann@24918
   438
    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
haftmann@24918
   439
      o Logic.unvarify o prop_of) thm;
haftmann@24918
   440
  in
haftmann@24918
   441
    fold_map (exprgen_term thy algbr funcgr) args
haftmann@24918
   442
    ##>> exprgen_term thy algbr funcgr rhs
haftmann@24918
   443
    #>> rpair thm
haftmann@24918
   444
  end
haftmann@24918
   445
and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
haftmann@24918
   446
  let
haftmann@24918
   447
    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
wenzelm@24969
   448
    val classparams = these (try (#params o AxClass.get_info thy) class);
haftmann@24918
   449
    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
haftmann@24918
   450
    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
haftmann@24918
   451
    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
haftmann@24918
   452
      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
haftmann@24918
   453
    val arity_typ = Type (tyco, map TFree vs);
haftmann@24918
   454
    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
haftmann@24918
   455
    fun exprgen_superarity superclass =
haftmann@24918
   456
      ensure_class thy algbr funcgr superclass
haftmann@24918
   457
      ##>> ensure_classrel thy algbr funcgr (class, superclass)
haftmann@24918
   458
      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
haftmann@24918
   459
      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
haftmann@24918
   460
            (superclass, (classrel, (inst, dss))));
haftmann@24918
   461
    fun exprgen_classparam_inst (c, ty) =
haftmann@24918
   462
      let
haftmann@24918
   463
        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
haftmann@25597
   464
        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
haftmann@24918
   465
        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
haftmann@24918
   466
          o Logic.dest_equals o Thm.prop_of) thm;
haftmann@24918
   467
      in
haftmann@24918
   468
        ensure_const thy algbr funcgr c
haftmann@24918
   469
        ##>> exprgen_const thy algbr funcgr c_ty
haftmann@24918
   470
        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
haftmann@24918
   471
      end;
haftmann@24918
   472
    val stmt_inst =
haftmann@24918
   473
      ensure_class thy algbr funcgr class
haftmann@24918
   474
      ##>> ensure_tyco thy algbr funcgr tyco
haftmann@24918
   475
      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   476
      ##>> fold_map exprgen_superarity superclasses
haftmann@24918
   477
      ##>> fold_map exprgen_classparam_inst classparams
haftmann@24918
   478
      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
haftmann@24918
   479
             Classinst ((class, (tyco, arity)), (superarities, classparams)));
haftmann@24918
   480
    val inst = CodeName.instance thy (class, tyco);
haftmann@24918
   481
  in
haftmann@24918
   482
    ensure_stmt stmt_inst inst
haftmann@24918
   483
  end
haftmann@24918
   484
and ensure_const thy (algbr as (_, consts)) funcgr c =
haftmann@24918
   485
  let
haftmann@24918
   486
    val c' = CodeName.const thy c;
haftmann@24918
   487
    fun stmt_datatypecons tyco =
haftmann@24918
   488
      ensure_tyco thy algbr funcgr tyco
haftmann@24918
   489
      #>> K (Datatypecons c');
haftmann@24918
   490
    fun stmt_classparam class =
haftmann@24918
   491
      ensure_class thy algbr funcgr class
haftmann@24918
   492
      #>> K (Classparam c');
haftmann@24918
   493
    fun stmt_fun trns =
haftmann@24918
   494
      let
haftmann@24918
   495
        val raw_thms = CodeFuncgr.funcs funcgr c;
haftmann@24918
   496
        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
haftmann@24918
   497
        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
haftmann@24918
   498
        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
haftmann@24918
   499
          then raw_thms
haftmann@24918
   500
          else map (CodeUnit.expand_eta 1) raw_thms;
haftmann@24918
   501
      in
haftmann@24918
   502
        trns
haftmann@24918
   503
        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   504
        ||>> exprgen_typ thy algbr funcgr ty
haftmann@24918
   505
        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
haftmann@24918
   506
        |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
haftmann@24918
   507
      end;
haftmann@24918
   508
    val stmtgen = case Code.get_datatype_of_constr thy c
haftmann@24918
   509
     of SOME tyco => stmt_datatypecons tyco
haftmann@24918
   510
      | NONE => (case AxClass.class_of_param thy c
haftmann@24918
   511
         of SOME class => stmt_classparam class
haftmann@24918
   512
          | NONE => stmt_fun)
haftmann@24918
   513
  in
haftmann@24918
   514
    ensure_stmt stmtgen c'
haftmann@24918
   515
  end
haftmann@24918
   516
and exprgen_term thy algbr funcgr (Const (c, ty)) =
haftmann@24918
   517
      exprgen_app thy algbr funcgr ((c, ty), [])
haftmann@24918
   518
  | exprgen_term thy algbr funcgr (Free (v, _)) =
haftmann@24918
   519
      pair (IVar v)
haftmann@24918
   520
  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
haftmann@24918
   521
      let
haftmann@24918
   522
        val (v, t) = Syntax.variant_abs abs;
haftmann@24918
   523
      in
haftmann@24918
   524
        exprgen_typ thy algbr funcgr ty
haftmann@24918
   525
        ##>> exprgen_term thy algbr funcgr t
haftmann@24918
   526
        #>> (fn (ty, t) => (v, ty) `|-> t)
haftmann@24918
   527
      end
haftmann@24918
   528
  | exprgen_term thy algbr funcgr (t as _ $ _) =
haftmann@24918
   529
      case strip_comb t
haftmann@24918
   530
       of (Const (c, ty), ts) =>
haftmann@24918
   531
            exprgen_app thy algbr funcgr ((c, ty), ts)
haftmann@24918
   532
        | (t', ts) =>
haftmann@24918
   533
            exprgen_term thy algbr funcgr t'
haftmann@24918
   534
            ##>> fold_map (exprgen_term thy algbr funcgr) ts
haftmann@24918
   535
            #>> (fn (t, ts) => t `$$ ts)
haftmann@24918
   536
and exprgen_const thy algbr funcgr (c, ty) =
haftmann@24918
   537
  ensure_const thy algbr funcgr c
haftmann@24918
   538
  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
haftmann@24918
   539
  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
haftmann@24918
   540
  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
haftmann@24918
   541
and exprgen_app_default thy algbr funcgr (c_ty, ts) =
haftmann@24918
   542
  exprgen_const thy algbr funcgr c_ty
haftmann@24918
   543
  ##>> fold_map (exprgen_term thy algbr funcgr) ts
haftmann@24918
   544
  #>> (fn (t, ts) => t `$$ ts)
haftmann@24918
   545
and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
haftmann@24918
   546
  let
haftmann@24918
   547
    val (tys, _) =
haftmann@24918
   548
      (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
haftmann@24918
   549
    val dt = nth ts n;
haftmann@24918
   550
    val dty = nth tys n;
haftmann@24918
   551
    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
haftmann@24918
   552
      | is_undefined _ = false;
haftmann@24918
   553
    fun mk_case (co, n) t =
haftmann@24918
   554
      let
haftmann@24918
   555
        val (vs, body) = Term.strip_abs_eta n t;
haftmann@24918
   556
        val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
haftmann@24918
   557
      in if is_undefined body then NONE else SOME (selector, body) end;
haftmann@24918
   558
    fun mk_ds [] =
haftmann@24918
   559
          let
haftmann@24918
   560
            val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
haftmann@24918
   561
          in [(Free v_ty, body)] end
haftmann@24918
   562
      | mk_ds cases = map_filter (uncurry mk_case)
haftmann@24918
   563
          (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
haftmann@24918
   564
  in
haftmann@24918
   565
    exprgen_term thy algbr funcgr dt
haftmann@24918
   566
    ##>> exprgen_typ thy algbr funcgr dty
haftmann@24918
   567
    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
haftmann@24918
   568
          ##>> exprgen_term thy algbr funcgr body) (mk_ds cases)
haftmann@24918
   569
    ##>> exprgen_app_default thy algbr funcgr app
haftmann@24918
   570
    #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
haftmann@24918
   571
  end
haftmann@24918
   572
and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
haftmann@24918
   573
 of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
haftmann@24918
   574
      if length ts < i then
haftmann@24918
   575
        let
haftmann@24918
   576
          val k = length ts;
haftmann@24918
   577
          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
haftmann@24918
   578
          val ctxt = (fold o fold_aterms)
haftmann@24918
   579
            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
haftmann@24918
   580
          val vs = Name.names ctxt "a" tys;
haftmann@24918
   581
        in
haftmann@24918
   582
          fold_map (exprgen_typ thy algbr funcgr) tys
haftmann@24918
   583
          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
haftmann@24918
   584
          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
haftmann@24918
   585
        end
haftmann@24918
   586
      else if length ts > i then
haftmann@24918
   587
        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
haftmann@24918
   588
        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
haftmann@24918
   589
        #>> (fn (t, ts) => t `$$ ts)
haftmann@24918
   590
      else
haftmann@24918
   591
        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
haftmann@24918
   592
      end
haftmann@24918
   593
  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
haftmann@24918
   594
haftmann@24918
   595
fun ensure_value thy algbr funcgr t = 
haftmann@24918
   596
  let
haftmann@24918
   597
    val ty = fastype_of t;
haftmann@24918
   598
    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
haftmann@24918
   599
      o dest_TFree))) t [];
haftmann@24918
   600
    val stmt_value =
haftmann@24918
   601
      fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   602
      ##>> exprgen_typ thy algbr funcgr ty
haftmann@24918
   603
      ##>> exprgen_term thy algbr funcgr t
haftmann@24918
   604
      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
haftmann@24918
   605
  in
haftmann@24918
   606
    ensure_stmt stmt_value CodeName.value_name
haftmann@24918
   607
  end;
haftmann@24918
   608
haftmann@24918
   609
fun add_value_stmt (t, ty) code =
haftmann@24219
   610
  code
haftmann@24918
   611
  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
haftmann@24918
   612
  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
haftmann@24219
   613
haftmann@24219
   614
end; (*struct*)
haftmann@24219
   615
haftmann@24219
   616
haftmann@24219
   617
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;