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