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