src/Tools/code/code_thingol.ML
author haftmann
Tue Jul 01 07:58:37 2008 +0200 (2008-07-01)
changeset 27422 73d25d422124
parent 27103 d8549f4d900b
child 27609 b23c9ad0fe7d
permissions -rw-r--r--
tuned
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
fun ensure_stmt stmtgen name (dep, program) =
haftmann@24219
   302
  let
haftmann@27103
   303
    val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
haftmann@27103
   304
    fun add_stmt false =
haftmann@27103
   305
          Graph.default_node (name, NoStmt)
haftmann@27103
   306
          #> add_dep
haftmann@24918
   307
          #> curry stmtgen (SOME name)
haftmann@24252
   308
          ##> snd
haftmann@27103
   309
          #-> (fn stmt => Graph.map_node name (K stmt))
haftmann@27103
   310
      | add_stmt true =
haftmann@27103
   311
          add_dep;
haftmann@24219
   312
  in
haftmann@27103
   313
    program
haftmann@27103
   314
    |> add_stmt (can (Graph.get_node program) name)
haftmann@24219
   315
    |> pair dep
haftmann@24918
   316
    |> pair name
haftmann@24219
   317
  end;
haftmann@24219
   318
haftmann@26972
   319
fun not_wellsorted thy thm ty sort e =
haftmann@26972
   320
  let
haftmann@26972
   321
    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
haftmann@26972
   322
    val err_thm = case thm
haftmann@26972
   323
     of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
haftmann@26972
   324
    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
haftmann@26972
   325
      ^ Syntax.string_of_sort_global thy sort;
haftmann@26972
   326
  in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
haftmann@26972
   327
haftmann@26972
   328
fun ensure_class thy (algbr as (_, algebra)) funcgr class =
haftmann@24918
   329
  let
haftmann@24918
   330
    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
wenzelm@24969
   331
    val cs = #params (AxClass.get_info thy class);
haftmann@24918
   332
    val class' = CodeName.class thy class;
haftmann@24918
   333
    val stmt_class =
haftmann@24918
   334
      fold_map (fn superclass => ensure_class thy algbr funcgr superclass
haftmann@24918
   335
        ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
haftmann@24918
   336
      ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
haftmann@24918
   337
        ##>> exprgen_typ thy algbr funcgr ty) cs
wenzelm@24969
   338
      #>> (fn info => Class (unprefix "'" Name.aT, info))
haftmann@27422
   339
  in ensure_stmt stmt_class class' end
haftmann@24918
   340
and ensure_classrel thy algbr funcgr (subclass, superclass) =
haftmann@24918
   341
  let
haftmann@24918
   342
    val classrel' = CodeName.classrel thy (subclass, superclass);
haftmann@24918
   343
    val stmt_classrel =
haftmann@24918
   344
      ensure_class thy algbr funcgr subclass
haftmann@24918
   345
      ##>> ensure_class thy algbr funcgr superclass
haftmann@24918
   346
      #>> Classrel;
haftmann@27422
   347
  in ensure_stmt stmt_classrel classrel' end
haftmann@24918
   348
and ensure_tyco thy algbr funcgr "fun" =
haftmann@24918
   349
      pair "fun"
haftmann@24918
   350
  | ensure_tyco thy algbr funcgr tyco =
haftmann@24918
   351
      let
haftmann@24918
   352
        val stmt_datatype =
haftmann@24918
   353
          let
haftmann@24918
   354
            val (vs, cos) = Code.get_datatype thy tyco;
haftmann@24918
   355
          in
haftmann@24918
   356
            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   357
            ##>> fold_map (fn (c, tys) =>
haftmann@24918
   358
              ensure_const thy algbr funcgr c
haftmann@24918
   359
              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
haftmann@24918
   360
            #>> Datatype
haftmann@24918
   361
          end;
haftmann@24918
   362
        val tyco' = CodeName.tyco thy tyco;
haftmann@27422
   363
      in ensure_stmt stmt_datatype tyco' end
haftmann@26972
   364
and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
haftmann@24918
   365
  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
haftmann@24918
   366
  #>> (fn sort => (unprefix "'" v, sort))
haftmann@27422
   367
and exprgen_typ thy algbr funcgr (TFree v_sort) =
haftmann@27422
   368
      exprgen_tyvar_sort thy algbr funcgr v_sort
haftmann@24918
   369
      #>> (fn (v, sort) => ITyVar v)
haftmann@24918
   370
  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
haftmann@24918
   371
      ensure_tyco thy algbr funcgr tyco
haftmann@24918
   372
      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
haftmann@24918
   373
      #>> (fn (tyco, tys) => tyco `%% tys)
haftmann@26972
   374
and exprgen_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
haftmann@24918
   375
  let
wenzelm@26939
   376
    val pp = Syntax.pp_global thy;
haftmann@24918
   377
    datatype typarg =
haftmann@24918
   378
        Global of (class * string) * typarg list list
haftmann@24918
   379
      | Local of (class * class) list * (string * (int * sort));
haftmann@24918
   380
    fun class_relation (Global ((_, tyco), yss), _) class =
haftmann@24918
   381
          Global ((class, tyco), yss)
haftmann@24918
   382
      | class_relation (Local (classrels, v), subclass) superclass =
haftmann@24918
   383
          Local ((subclass, superclass) :: classrels, v);
haftmann@24918
   384
    fun type_constructor tyco yss class =
haftmann@24918
   385
      Global ((class, tyco), (map o map) fst yss);
haftmann@24918
   386
    fun type_variable (TFree (v, sort)) =
haftmann@24918
   387
      let
haftmann@24918
   388
        val sort' = proj_sort sort;
haftmann@24918
   389
      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
haftmann@24918
   390
    val typargs = Sorts.of_sort_derivation pp algebra
haftmann@24918
   391
      {class_relation = class_relation, type_constructor = type_constructor,
haftmann@26972
   392
       type_variable = type_variable} (ty, proj_sort sort)
haftmann@26972
   393
      handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
haftmann@24918
   394
    fun mk_dict (Global (inst, yss)) =
haftmann@24918
   395
          ensure_inst thy algbr funcgr inst
haftmann@24918
   396
          ##>> (fold_map o fold_map) mk_dict yss
haftmann@24918
   397
          #>> (fn (inst, dss) => DictConst (inst, dss))
haftmann@24918
   398
      | mk_dict (Local (classrels, (v, (k, sort)))) =
haftmann@24918
   399
          fold_map (ensure_classrel thy algbr funcgr) classrels
haftmann@24918
   400
          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
haftmann@27422
   401
  in fold_map mk_dict typargs end
haftmann@24918
   402
and exprgen_eq thy algbr funcgr thm =
haftmann@24918
   403
  let
haftmann@24918
   404
    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
haftmann@24918
   405
      o Logic.unvarify o prop_of) thm;
haftmann@24918
   406
  in
haftmann@26972
   407
    fold_map (exprgen_term thy algbr funcgr (SOME thm)) args
haftmann@26972
   408
    ##>> exprgen_term thy algbr funcgr (SOME thm) rhs
haftmann@24918
   409
    #>> rpair thm
haftmann@24918
   410
  end
haftmann@26972
   411
and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
haftmann@24918
   412
  let
haftmann@24918
   413
    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
wenzelm@24969
   414
    val classparams = these (try (#params o AxClass.get_info thy) class);
haftmann@24918
   415
    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
haftmann@24918
   416
    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
haftmann@24918
   417
    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
haftmann@24918
   418
      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
haftmann@24918
   419
    val arity_typ = Type (tyco, map TFree vs);
haftmann@24918
   420
    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
haftmann@24918
   421
    fun exprgen_superarity superclass =
haftmann@24918
   422
      ensure_class thy algbr funcgr superclass
haftmann@24918
   423
      ##>> ensure_classrel thy algbr funcgr (class, superclass)
haftmann@26972
   424
      ##>> exprgen_dicts thy algbr funcgr NONE (arity_typ, [superclass])
haftmann@24918
   425
      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
haftmann@24918
   426
            (superclass, (classrel, (inst, dss))));
haftmann@24918
   427
    fun exprgen_classparam_inst (c, ty) =
haftmann@24918
   428
      let
haftmann@24918
   429
        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
haftmann@25597
   430
        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
haftmann@24918
   431
        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
haftmann@24918
   432
          o Logic.dest_equals o Thm.prop_of) thm;
haftmann@24918
   433
      in
haftmann@24918
   434
        ensure_const thy algbr funcgr c
haftmann@26972
   435
        ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty
haftmann@24918
   436
        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
haftmann@24918
   437
      end;
haftmann@24918
   438
    val stmt_inst =
haftmann@24918
   439
      ensure_class thy algbr funcgr class
haftmann@24918
   440
      ##>> ensure_tyco thy algbr funcgr tyco
haftmann@24918
   441
      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   442
      ##>> fold_map exprgen_superarity superclasses
haftmann@24918
   443
      ##>> fold_map exprgen_classparam_inst classparams
haftmann@24918
   444
      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
haftmann@24918
   445
             Classinst ((class, (tyco, arity)), (superarities, classparams)));
haftmann@24918
   446
    val inst = CodeName.instance thy (class, tyco);
haftmann@27422
   447
  in ensure_stmt stmt_inst inst end
haftmann@26972
   448
and ensure_const thy algbr funcgr c =
haftmann@24918
   449
  let
haftmann@24918
   450
    val c' = CodeName.const thy c;
haftmann@24918
   451
    fun stmt_datatypecons tyco =
haftmann@24918
   452
      ensure_tyco thy algbr funcgr tyco
haftmann@25621
   453
      #>> Datatypecons;
haftmann@24918
   454
    fun stmt_classparam class =
haftmann@24918
   455
      ensure_class thy algbr funcgr class
haftmann@25621
   456
      #>> Classparam;
haftmann@24918
   457
    fun stmt_fun trns =
haftmann@24918
   458
      let
haftmann@24918
   459
        val raw_thms = CodeFuncgr.funcs funcgr c;
haftmann@26972
   460
        val (vs, raw_ty) = CodeFuncgr.typ funcgr c;
haftmann@26972
   461
        val ty = Logic.unvarifyT raw_ty;
haftmann@24918
   462
        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
haftmann@24918
   463
          then raw_thms
haftmann@24918
   464
          else map (CodeUnit.expand_eta 1) raw_thms;
haftmann@24918
   465
      in
haftmann@24918
   466
        trns
haftmann@24918
   467
        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   468
        ||>> exprgen_typ thy algbr funcgr ty
haftmann@24918
   469
        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
haftmann@24918
   470
        |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
haftmann@24918
   471
      end;
haftmann@24918
   472
    val stmtgen = case Code.get_datatype_of_constr thy c
haftmann@24918
   473
     of SOME tyco => stmt_datatypecons tyco
haftmann@24918
   474
      | NONE => (case AxClass.class_of_param thy c
haftmann@24918
   475
         of SOME class => stmt_classparam class
haftmann@24918
   476
          | NONE => stmt_fun)
haftmann@27422
   477
  in ensure_stmt stmtgen c' end
haftmann@26972
   478
and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
haftmann@26972
   479
      exprgen_app thy algbr funcgr thm ((c, ty), [])
haftmann@26972
   480
  | exprgen_term thy algbr funcgr thm (Free (v, _)) =
haftmann@24918
   481
      pair (IVar v)
haftmann@26972
   482
  | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
haftmann@24918
   483
      let
haftmann@24918
   484
        val (v, t) = Syntax.variant_abs abs;
haftmann@24918
   485
      in
haftmann@24918
   486
        exprgen_typ thy algbr funcgr ty
haftmann@26972
   487
        ##>> exprgen_term thy algbr funcgr thm t
haftmann@24918
   488
        #>> (fn (ty, t) => (v, ty) `|-> t)
haftmann@24918
   489
      end
haftmann@26972
   490
  | exprgen_term thy algbr funcgr thm (t as _ $ _) =
haftmann@24918
   491
      case strip_comb t
haftmann@24918
   492
       of (Const (c, ty), ts) =>
haftmann@26972
   493
            exprgen_app thy algbr funcgr thm ((c, ty), ts)
haftmann@24918
   494
        | (t', ts) =>
haftmann@26972
   495
            exprgen_term thy algbr funcgr thm t'
haftmann@26972
   496
            ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
haftmann@24918
   497
            #>> (fn (t, ts) => t `$$ ts)
haftmann@26972
   498
and exprgen_const thy algbr funcgr thm (c, ty) =
haftmann@26972
   499
  let
haftmann@26972
   500
    val tys = Sign.const_typargs thy (c, ty);
haftmann@26972
   501
    val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c;
haftmann@26972
   502
    val tys_args = (fst o Term.strip_type) ty;
haftmann@26972
   503
  in
haftmann@26972
   504
    ensure_const thy algbr funcgr c
haftmann@26972
   505
    ##>> fold_map (exprgen_dicts thy algbr funcgr thm) (tys ~~ sorts)
haftmann@26972
   506
    ##>> fold_map (exprgen_typ thy algbr funcgr) tys_args
haftmann@26972
   507
    #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
haftmann@26972
   508
  end
haftmann@26972
   509
and exprgen_app_default thy algbr funcgr thm (c_ty, ts) =
haftmann@26972
   510
  exprgen_const thy algbr funcgr thm c_ty
haftmann@26972
   511
  ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
haftmann@24918
   512
  #>> (fn (t, ts) => t `$$ ts)
haftmann@26972
   513
and exprgen_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
haftmann@24918
   514
  let
haftmann@24918
   515
    val (tys, _) =
haftmann@24918
   516
      (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
haftmann@24918
   517
    val dt = nth ts n;
haftmann@24918
   518
    val dty = nth tys n;
haftmann@24918
   519
    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
haftmann@24918
   520
      | is_undefined _ = false;
haftmann@24918
   521
    fun mk_case (co, n) t =
haftmann@24918
   522
      let
haftmann@24918
   523
        val (vs, body) = Term.strip_abs_eta n t;
haftmann@24918
   524
        val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
haftmann@24918
   525
      in if is_undefined body then NONE else SOME (selector, body) end;
haftmann@24918
   526
    fun mk_ds [] =
haftmann@24918
   527
          let
haftmann@24918
   528
            val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
haftmann@24918
   529
          in [(Free v_ty, body)] end
haftmann@24918
   530
      | mk_ds cases = map_filter (uncurry mk_case)
haftmann@24918
   531
          (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
haftmann@24918
   532
  in
haftmann@26972
   533
    exprgen_term thy algbr funcgr thm dt
haftmann@24918
   534
    ##>> exprgen_typ thy algbr funcgr dty
haftmann@26972
   535
    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr thm pat
haftmann@26972
   536
          ##>> exprgen_term thy algbr funcgr thm body) (mk_ds cases)
haftmann@26972
   537
    ##>> exprgen_app_default thy algbr funcgr thm app
haftmann@24918
   538
    #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
haftmann@24918
   539
  end
haftmann@26972
   540
and exprgen_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
haftmann@24918
   541
 of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
haftmann@24918
   542
      if length ts < i then
haftmann@24918
   543
        let
haftmann@24918
   544
          val k = length ts;
haftmann@24918
   545
          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
haftmann@24918
   546
          val ctxt = (fold o fold_aterms)
haftmann@24918
   547
            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
haftmann@24918
   548
          val vs = Name.names ctxt "a" tys;
haftmann@24918
   549
        in
haftmann@24918
   550
          fold_map (exprgen_typ thy algbr funcgr) tys
haftmann@26972
   551
          ##>> exprgen_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
haftmann@24918
   552
          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
haftmann@24918
   553
        end
haftmann@24918
   554
      else if length ts > i then
haftmann@26972
   555
        exprgen_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
haftmann@26972
   556
        ##>> fold_map (exprgen_term thy algbr funcgr thm) (Library.drop (i, ts))
haftmann@24918
   557
        #>> (fn (t, ts) => t `$$ ts)
haftmann@24918
   558
      else
haftmann@26972
   559
        exprgen_case thy algbr funcgr thm n cases ((c, ty), ts)
haftmann@24918
   560
      end
haftmann@26972
   561
  | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts);
haftmann@24918
   562
haftmann@25969
   563
haftmann@27103
   564
(** generated programs **)
haftmann@27103
   565
haftmann@27103
   566
(* store *)
haftmann@27103
   567
haftmann@27103
   568
structure Program = CodeDataFun
haftmann@27103
   569
(
haftmann@27103
   570
  type T = program;
haftmann@27103
   571
  val empty = Graph.empty;
haftmann@27103
   572
  fun merge _ = Graph.merge (K true);
haftmann@27103
   573
  fun purge _ NONE _ = Graph.empty
haftmann@27103
   574
    | purge NONE _ _ = Graph.empty
haftmann@27103
   575
    | purge (SOME thy) (SOME cs) program =
haftmann@27103
   576
        let
haftmann@27103
   577
          val cs_exisiting =
haftmann@27103
   578
            map_filter (CodeName.const_rev thy) (Graph.keys program);
haftmann@27103
   579
          val dels = (Graph.all_preds program
haftmann@27103
   580
              o map (CodeName.const thy)
haftmann@27103
   581
              o filter (member (op =) cs_exisiting)
haftmann@27103
   582
            ) cs;
haftmann@27103
   583
        in Graph.del_nodes dels program end;
haftmann@27103
   584
);
haftmann@27103
   585
haftmann@27103
   586
val cached_program = Program.get;
haftmann@25969
   587
haftmann@27103
   588
fun transact f program =
haftmann@27103
   589
  (NONE, program)
haftmann@27103
   590
  |> f
haftmann@27103
   591
  |-> (fn x => fn (_, program) => (x, program));
haftmann@27103
   592
haftmann@27103
   593
fun generate thy funcgr f x =
haftmann@27103
   594
  Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x));
haftmann@27103
   595
haftmann@27103
   596
haftmann@27103
   597
(* program generation *)
haftmann@27103
   598
haftmann@27103
   599
fun consts_program thy cs =
haftmann@27103
   600
  let
haftmann@27103
   601
    fun project_consts cs program =
haftmann@27103
   602
      let
haftmann@27103
   603
        val cs_all = Graph.all_succs program cs;
haftmann@27103
   604
      in (cs, Graph.subgraph (member (op =) cs_all) program) end;
haftmann@27103
   605
    fun generate_consts thy algebra funcgr =
haftmann@27103
   606
      fold_map (ensure_const thy algebra funcgr);
haftmann@27103
   607
  in
haftmann@27103
   608
    generate thy (CodeFuncgr.make thy cs) generate_consts cs
haftmann@27103
   609
    |-> project_consts
haftmann@27103
   610
  end;
haftmann@27103
   611
haftmann@27103
   612
haftmann@27103
   613
(* value evaluation *)
haftmann@25969
   614
haftmann@24918
   615
fun ensure_value thy algbr funcgr t = 
haftmann@24918
   616
  let
haftmann@24918
   617
    val ty = fastype_of t;
haftmann@24918
   618
    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
haftmann@24918
   619
      o dest_TFree))) t [];
haftmann@24918
   620
    val stmt_value =
haftmann@24918
   621
      fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
haftmann@24918
   622
      ##>> exprgen_typ thy algbr funcgr ty
haftmann@26972
   623
      ##>> exprgen_term thy algbr funcgr NONE t
haftmann@24918
   624
      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
haftmann@27103
   625
    fun term_value (dep, program1) =
haftmann@25969
   626
      let
haftmann@25969
   627
        val Fun ((vs, ty), [(([], t), _)]) =
haftmann@27103
   628
          Graph.get_node program1 CodeName.value_name;
haftmann@27103
   629
        val deps = Graph.imm_succs program1 CodeName.value_name;
haftmann@27103
   630
        val program2 = Graph.del_nodes [CodeName.value_name] program1;
haftmann@27103
   631
        val deps_all = Graph.all_succs program2 deps;
haftmann@27103
   632
        val program3 = Graph.subgraph (member (op =) deps_all) program2;
haftmann@27103
   633
      in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
haftmann@26011
   634
  in
haftmann@26011
   635
    ensure_stmt stmt_value CodeName.value_name
haftmann@26011
   636
    #> snd
haftmann@26011
   637
    #> term_value
haftmann@26011
   638
  end;
haftmann@24219
   639
haftmann@27103
   640
fun eval eval_kind thy evaluator =
haftmann@27103
   641
  let
haftmann@27103
   642
    fun evaluator'' evaluator''' funcgr t =
haftmann@27103
   643
      let
haftmann@27103
   644
        val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
haftmann@27103
   645
      in evaluator''' program vs_ty_t deps end;
haftmann@27103
   646
    fun evaluator' t =
haftmann@27103
   647
      let
haftmann@27103
   648
        val (t', evaluator''') = evaluator t;
haftmann@27103
   649
      in (t', evaluator'' evaluator''') end;
haftmann@27103
   650
  in eval_kind thy evaluator' end
haftmann@27103
   651
haftmann@27103
   652
fun eval_conv thy = eval CodeFuncgr.eval_conv thy;
haftmann@27103
   653
fun eval_term thy = eval CodeFuncgr.eval_term thy;
haftmann@27103
   654
haftmann@24219
   655
end; (*struct*)
haftmann@24219
   656
haftmann@24219
   657
haftmann@24219
   658
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;