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