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