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