src/Tools/Code/code_thingol.ML
author bulwahn
Wed, 07 Sep 2011 13:51:34 +0200
changeset 44790 c13fdf710a40
parent 44789 5a062c23c7db
child 44791 7ecb4124a3a3
permissions -rw-r--r--
adding type inference for disambiguation annotations in code equation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 37705
diff changeset
     1
(*  Title:      Tools/Code/code_thingol.ML
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     3
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     4
Intermediate language ("Thin-gol") representing executable code.
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
     5
Representation and translation.
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     6
*)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     7
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     8
infix 8 `%%;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
     9
infix 4 `$;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    10
infix 4 `$$;
31724
9b5a128cdb5c more appropriate syntax for IML abstraction
haftmann
parents: 31156
diff changeset
    11
infixr 3 `|=>;
9b5a128cdb5c more appropriate syntax for IML abstraction
haftmann
parents: 31156
diff changeset
    12
infixr 3 `|==>;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    13
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    14
signature BASIC_CODE_THINGOL =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    15
sig
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    16
  type vname = string;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    17
  datatype dict =
41782
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
    18
      Dict of string list * plain_dict
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
    19
  and plain_dict = 
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
    20
      Dict_Const of string * dict list list
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
    21
    | Dict_Var of vname * (int * int)
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    22
  datatype itype =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    23
      `%% of string * itype list
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    24
    | ITyVar of vname;
44789
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
    25
  type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
41782
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
    26
    (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
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
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
    29
    | IVar of vname option
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    30
    | `$ of iterm * iterm
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
    31
    | `|=> of (vname option * itype) * iterm
24219
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 `$$ : iterm * iterm list -> iterm;
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
    35
  val `|==> : (vname option * itype) list * iterm -> iterm;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    36
  type typscheme = (vname * sort) list * itype;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    37
end;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    38
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    39
signature CODE_THINGOL =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    40
sig
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    41
  include BASIC_CODE_THINGOL
34084
05cb31ca48ae explicit name for function space
haftmann
parents: 34013
diff changeset
    42
  val fun_tyco: string
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    43
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    44
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    45
  val unfold_fun: itype -> itype list * itype
37640
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
    46
  val unfold_fun_n: int -> itype -> itype list * itype
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    47
  val unfold_app: iterm -> iterm * iterm list
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
    48
  val unfold_abs: iterm -> (vname option * itype) list * iterm
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    49
  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    50
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
    51
  val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
    52
  val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
31049
396d4d6a1594 explicit type arguments in constants
haftmann
parents: 31036
diff changeset
    53
  val unfold_const_app: iterm -> (const * iterm list) option
32909
bd72e72c3ee3 added is_IVar
haftmann
parents: 32895
diff changeset
    54
  val is_IVar: iterm -> bool
41782
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
    55
  val is_IAbs: iterm -> bool
31049
396d4d6a1594 explicit type arguments in constants
haftmann
parents: 31036
diff changeset
    56
  val eta_expand: int -> const * iterm list -> iterm
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
    57
  val contains_dict_var: iterm -> bool
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    58
  val locally_monomorphic: iterm -> bool
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
    59
  val add_constnames: iterm -> string list -> string list
32917
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
    60
  val add_tyconames: iterm -> string list -> string list
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    61
  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    62
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    63
  type naming
28706
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
    64
  val empty_naming: naming
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    65
  val lookup_class: naming -> class -> string option
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    66
  val lookup_classrel: naming -> class * class -> string option
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    67
  val lookup_tyco: naming -> string -> string option
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    68
  val lookup_instance: naming -> class * string -> string option
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    69
  val lookup_const: naming -> string -> string option
31054
841c9f67f9e7 explicit type arguments in constants
haftmann
parents: 31049
diff changeset
    70
  val ensure_declared_const: theory -> string -> naming -> string * naming
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    71
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
    72
  datatype stmt =
27024
fcab2dd46872 various code streamlining
haftmann
parents: 26972
diff changeset
    73
      NoStmt
37437
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
    74
    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
    75
    | Datatype of string * ((vname * sort) list *
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
    76
        ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    77
    | Datatypecons of string * string
37447
ad3e04f289b6 transitive superclasses were also only a misunderstanding
haftmann
parents: 37446
diff changeset
    78
    | Class of class * (vname * ((class * string) list * (string * itype) list))
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    79
    | Classrel of class * class
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    80
    | Classparam of string * class
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
    81
    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
37445
e372fa3c7239 dropped obscure type argument weakening mapping -- was only a misunderstanding
haftmann
parents: 37440
diff changeset
    82
          * ((class * (string * (string * dict list list))) list (*super instances*)
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
    83
        * (((string * const) * (thm * bool)) list (*class parameter instances*)
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
    84
          * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    85
  type program = stmt Graph.T
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    86
  val empty_funs: program -> string list
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    87
  val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    88
  val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    89
  val is_cons: program -> string -> bool
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
    90
  val is_case: stmt -> bool
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
    91
  val contr_classparam_typs: program -> string -> itype option list
32895
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
    92
  val labelled_name: theory -> program -> string -> string
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
    93
  val group_stmts: theory -> program
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
    94
    -> ((string * stmt) list * (string * stmt) list
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
    95
      * ((string * stmt) list * (string * stmt) list)) list
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
    96
31036
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
    97
  val read_const_exprs: theory -> string list -> string list * string list
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
    98
  val consts_program: theory -> bool -> string list -> string list * (naming * program)
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
    99
  val dynamic_conv: theory -> (naming -> program
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   100
    -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
38672
f1f64375f662 preliminary versions of static_eval_conv(_simple)
haftmann
parents: 38669
diff changeset
   101
    -> conv
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   102
  val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   103
    -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   104
    -> term -> 'a
41346
6673f6fa94ca canonical handling of theory context argument
haftmann
parents: 41184
diff changeset
   105
  val static_conv: theory -> string list -> (naming -> program -> string list
6673f6fa94ca canonical handling of theory context argument
haftmann
parents: 41184
diff changeset
   106
    -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
38672
f1f64375f662 preliminary versions of static_eval_conv(_simple)
haftmann
parents: 38669
diff changeset
   107
    -> conv
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   108
  val static_conv_simple: theory -> string list
41346
6673f6fa94ca canonical handling of theory context argument
haftmann
parents: 41184
diff changeset
   109
    -> (program -> (string * sort) list -> term -> conv) -> conv
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   110
  val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
41346
6673f6fa94ca canonical handling of theory context argument
haftmann
parents: 41184
diff changeset
   111
    (naming -> program -> string list
6673f6fa94ca canonical handling of theory context argument
haftmann
parents: 41184
diff changeset
   112
      -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
39475
9cc1ba3c5706 separation of static and dynamic thy context
haftmann
parents: 39397
diff changeset
   113
    -> term -> 'a
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   114
end;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   115
28054
2b84d34c5d02 restructured and split code serializer module
haftmann
parents: 27711
diff changeset
   116
structure Code_Thingol: CODE_THINGOL =
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   117
struct
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   118
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   119
(** auxiliary **)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   120
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   121
fun unfoldl dest x =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   122
  case dest x
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   123
   of NONE => (x, [])
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   124
    | SOME (x1, x2) =>
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   125
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   126
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   127
fun unfoldr dest x =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   128
  case dest x
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   129
   of NONE => ([], x)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   130
    | SOME (x1, x2) =>
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   131
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   132
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   133
29962
bd4dc7fa742d tuned comments, stripped ID, deleted superfluous code
haftmann
parents: 29952
diff changeset
   134
(** language core - types, terms **)
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   135
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   136
type vname = string;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   137
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   138
datatype dict =
41782
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
   139
    Dict of string list * plain_dict
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   140
and plain_dict = 
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   141
    Dict_Const of string * dict list list
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   142
  | Dict_Var of vname * (int * int)
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   143
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   144
datatype itype =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   145
    `%% of string * itype list
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   146
  | ITyVar of vname;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   147
44789
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   148
type const = string * (((itype list * dict list list) *
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   149
  (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
24591
6509626eb2c9 added explicit theorems
haftmann
parents: 24381
diff changeset
   150
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   151
datatype iterm =
24591
6509626eb2c9 added explicit theorems
haftmann
parents: 24381
diff changeset
   152
    IConst of const
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   153
  | IVar of vname option
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   154
  | `$ of iterm * iterm
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
   155
  | `|=> of (vname option * itype) * iterm
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   156
  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   157
    (*see also signature*)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   158
32909
bd72e72c3ee3 added is_IVar
haftmann
parents: 32895
diff changeset
   159
fun is_IVar (IVar _) = true
bd72e72c3ee3 added is_IVar
haftmann
parents: 32895
diff changeset
   160
  | is_IVar _ = false;
bd72e72c3ee3 added is_IVar
haftmann
parents: 32895
diff changeset
   161
41782
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
   162
fun is_IAbs (_ `|=> _) = true
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
   163
  | is_IAbs _ = false;
ffcc3137b1ad added is_IAbs; tuned brackets and comments
haftmann
parents: 41365
diff changeset
   164
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   165
val op `$$ = Library.foldl (op `$);
31724
9b5a128cdb5c more appropriate syntax for IML abstraction
haftmann
parents: 31156
diff changeset
   166
val op `|==> = Library.foldr (op `|=>);
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   167
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   168
val unfold_app = unfoldl
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   169
  (fn op `$ t => SOME t
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   170
    | _ => NONE);
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   171
31874
f172346ba805 simplified binding concept
haftmann
parents: 31775
diff changeset
   172
val unfold_abs = unfoldr
f172346ba805 simplified binding concept
haftmann
parents: 31775
diff changeset
   173
  (fn op `|=> t => SOME t
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   174
    | _ => NONE);
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   175
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   176
val split_let = 
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   177
  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   178
    | _ => NONE);
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   179
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   180
val unfold_let = unfoldr split_let;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   181
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   182
fun unfold_const_app t =
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   183
 case unfold_app t
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   184
  of (IConst c, ts) => SOME (c, ts)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   185
   | _ => NONE;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   186
32917
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   187
fun fold_constexprs f =
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   188
  let
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   189
    fun fold' (IConst c) = f c
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   190
      | fold' (IVar _) = I
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   191
      | fold' (t1 `$ t2) = fold' t1 #> fold' t2
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   192
      | fold' (_ `|=> t) = fold' t
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   193
      | fold' (ICase (((t, _), ds), _)) = fold' t
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   194
          #> fold (fn (pat, body) => fold' pat #> fold' body) ds
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   195
  in fold' end;
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   196
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   197
val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   198
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   199
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   200
  | add_tycos (ITyVar _) = I;
84a5c684a22e added add_tyconames; tuned
haftmann
parents: 32909
diff changeset
   201
44788
8b935f1b3cf8 changing const type to pass along if typing annotations are necessary for disambigous terms
bulwahn
parents: 44338
diff changeset
   202
val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
24219
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
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   206
    fun fold_aux add f =
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   207
      let
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   208
        fun fold_term _ (IConst _) = I
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   209
          | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   210
          | fold_term _ (IVar NONE) = I
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   211
          | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   212
          | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   213
          | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   214
          | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   215
        and fold_case vs (p, t) = fold_term (add p vs) t;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   216
      in fold_term [] end;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   217
    fun add t = fold_aux add (insert (op =)) t;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   218
  in fold_aux add f end;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   219
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   220
fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
31874
f172346ba805 simplified binding concept
haftmann
parents: 31775
diff changeset
   221
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   222
fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
   223
  | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   224
     of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
   225
          if v = w andalso (exists_var p v orelse not (exists_var t' v))
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   226
          then ((p, ty), t')
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   227
          else ((IVar (SOME v), ty), t)
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   228
      | _ => ((IVar (SOME v), ty), t))
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
   229
  | split_pat_abs _ = NONE;
31874
f172346ba805 simplified binding concept
haftmann
parents: 31775
diff changeset
   230
f172346ba805 simplified binding concept
haftmann
parents: 31775
diff changeset
   231
val unfold_pat_abs = unfoldr split_pat_abs;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   232
31890
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   233
fun unfold_abs_eta [] t = ([], t)
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   234
  | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   235
      let
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   236
        val (vs_tys, t') = unfold_abs_eta tys t;
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   237
      in (v_ty :: vs_tys, t') end
31892
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   238
  | unfold_abs_eta tys t =
31890
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   239
      let
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   240
        val ctxt = fold_varnames Name.declare t Name.context;
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   241
        val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
31890
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   242
      in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
e943b039f0ac an intermediate step towards a refined translation of cases
haftmann
parents: 31889
diff changeset
   243
44789
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   244
fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   245
  let
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   246
    val j = length ts;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   247
    val l = k - j;
37841
ff1c9cb6dc5d don't fail gracefully
haftmann
parents: 37744
diff changeset
   248
    val _ = if l > length tys
ff1c9cb6dc5d don't fail gracefully
haftmann
parents: 37744
diff changeset
   249
      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   250
    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   251
    val vs_tys = (map o apfst) SOME
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   252
      (Name.invent_names ctxt "a" ((take l o drop j) tys));
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   253
  in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   254
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   255
fun contains_dict_var t =
24662
f79f6061525c more precise treatment of free dictionary parameters for evaluation
haftmann
parents: 24591
diff changeset
   256
  let
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   257
    fun cont_dict (Dict (_, d)) = cont_plain_dict d
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   258
    and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   259
      | cont_plain_dict (Dict_Var _) = true;
44788
8b935f1b3cf8 changing const type to pass along if typing annotations are necessary for disambigous terms
bulwahn
parents: 44338
diff changeset
   260
    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   261
      | cont_term (IVar _) = false
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   262
      | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   263
      | cont_term (_ `|=> t) = cont_term t
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   264
      | cont_term (ICase (_, t)) = cont_term t;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   265
  in cont_term t end;
24662
f79f6061525c more precise treatment of free dictionary parameters for evaluation
haftmann
parents: 24591
diff changeset
   266
  
25621
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   267
fun locally_monomorphic (IConst _) = false
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   268
  | locally_monomorphic (IVar _) = true
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   269
  | locally_monomorphic (t `$ _) = locally_monomorphic t
31724
9b5a128cdb5c more appropriate syntax for IML abstraction
haftmann
parents: 31156
diff changeset
   270
  | locally_monomorphic (_ `|=> t) = locally_monomorphic t
25621
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   271
  | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   272
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   273
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   274
(** namings **)
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   275
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   276
(* policies *)
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   277
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   278
local
33172
61ee96bc9895 maintain theory name via name space, not tags;
wenzelm
parents: 33029
diff changeset
   279
  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
61ee96bc9895 maintain theory name via name space, not tags;
wenzelm
parents: 33029
diff changeset
   280
  fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
61ee96bc9895 maintain theory name via name space, not tags;
wenzelm
parents: 33029
diff changeset
   281
   of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   282
    | thyname :: _ => thyname;
28706
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   283
  fun thyname_of_const thy c = case AxClass.class_of_param thy c
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   284
   of SOME class => thyname_of_class thy class
35299
4f4d5bf4ea08 proper distinction of code datatypes and abstypes
haftmann
parents: 35226
diff changeset
   285
    | NONE => (case Code.get_type_of_constr_or_abstr thy c
35226
b987b803616d a simple concept for datatype invariants
haftmann
parents: 34895
diff changeset
   286
       of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
33172
61ee96bc9895 maintain theory name via name space, not tags;
wenzelm
parents: 33029
diff changeset
   287
        | NONE => Codegen.thyname_of_const thy c);
33420
17b7095ad463 pretty name for ==>
haftmann
parents: 33187
diff changeset
   288
  fun purify_base "==>" = "follows"
39566
87a5704673f0 Pure equality is a regular cpde operation
haftmann
parents: 39487
diff changeset
   289
    | purify_base "==" = "meta_eq"
31036
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
   290
    | purify_base s = Name.desymbolize false s;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   291
  fun namify thy get_basename get_thyname name =
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   292
    let
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   293
      val prefix = get_thyname thy name;
31036
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
   294
      val base = (purify_base o get_basename) name;
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   295
    in Long_Name.append prefix base end;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   296
in
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   297
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   298
fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   299
fun namify_classrel thy = namify thy (fn (sub_class, super_class) => 
37431
e9004a3e0d94 teaked naming of superclass projections
haftmann
parents: 37384
diff changeset
   300
    Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class)
33172
61ee96bc9895 maintain theory name via name space, not tags;
wenzelm
parents: 33029
diff changeset
   301
  (fn thy => thyname_of_class thy o fst);
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   302
  (*order fits nicely with composed projections*)
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   303
fun namify_tyco thy "fun" = "Pure.fun"
33172
61ee96bc9895 maintain theory name via name space, not tags;
wenzelm
parents: 33029
diff changeset
   304
  | namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   305
fun namify_instance thy = namify thy (fn (class, tyco) => 
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   306
  Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   307
fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   308
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   309
end; (* local *)
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   310
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   311
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   312
(* data *)
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   313
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   314
datatype naming = Naming of {
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   315
  class: class Symtab.table * Name.context,
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   316
  classrel: string Symreltab.table * Name.context,
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   317
  tyco: string Symtab.table * Name.context,
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   318
  instance: string Symreltab.table * Name.context,
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   319
  const: string Symtab.table * Name.context
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   320
}
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   321
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   322
fun dest_Naming (Naming naming) = naming;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   323
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   324
val empty_naming = Naming {
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   325
  class = (Symtab.empty, Name.context),
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   326
  classrel = (Symreltab.empty, Name.context),
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   327
  tyco = (Symtab.empty, Name.context),
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   328
  instance = (Symreltab.empty, Name.context),
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   329
  const = (Symtab.empty, Name.context)
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   330
};
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   331
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   332
local
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   333
  fun mk_naming (class, classrel, tyco, instance, const) =
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   334
    Naming { class = class, classrel = classrel,
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   335
      tyco = tyco, instance = instance, const = const };
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   336
  fun map_naming f (Naming { class, classrel, tyco, instance, const }) =
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   337
    mk_naming (f (class, classrel, tyco, instance, const));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   338
in
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   339
  fun map_class f = map_naming
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   340
    (fn (class, classrel, tyco, inst, const) =>
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   341
      (f class, classrel, tyco, inst, const));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   342
  fun map_classrel f = map_naming
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   343
    (fn (class, classrel, tyco, inst, const) =>
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   344
      (class, f classrel, tyco, inst, const));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   345
  fun map_tyco f = map_naming
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   346
    (fn (class, classrel, tyco, inst, const) =>
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   347
      (class, classrel, f tyco, inst, const));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   348
  fun map_instance f = map_naming
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   349
    (fn (class, classrel, tyco, inst, const) =>
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   350
      (class, classrel, tyco, f inst, const));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   351
  fun map_const f = map_naming
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   352
    (fn (class, classrel, tyco, inst, const) =>
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   353
      (class, classrel, tyco, inst, f const));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   354
end; (*local*)
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   355
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   356
fun add_variant update (thing, name) (tab, used) =
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   357
  let
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 43048
diff changeset
   358
    val (name', used') = Name.variant name used;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   359
    val tab' = update (thing, name') tab;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   360
  in (tab', used') end;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   361
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   362
fun declare thy mapp lookup update namify thing =
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   363
  mapp (add_variant update (thing, namify thy thing))
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   364
  #> `(fn naming => the (lookup naming thing));
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   365
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   366
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   367
(* lookup and declare *)
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   368
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   369
local
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   370
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   371
val suffix_class = "class";
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   372
val suffix_classrel = "classrel"
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   373
val suffix_tyco = "tyco";
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   374
val suffix_instance = "inst";
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   375
val suffix_const = "const";
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   376
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   377
fun add_suffix nsp NONE = NONE
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   378
  | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   379
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   380
in
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   381
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   382
val lookup_class = add_suffix suffix_class
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   383
  oo Symtab.lookup o fst o #class o dest_Naming;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   384
val lookup_classrel = add_suffix suffix_classrel
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   385
  oo Symreltab.lookup o fst o #classrel o dest_Naming;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   386
val lookup_tyco = add_suffix suffix_tyco
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   387
  oo Symtab.lookup o fst o #tyco o dest_Naming;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   388
val lookup_instance = add_suffix suffix_instance
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   389
  oo Symreltab.lookup o fst o #instance o dest_Naming;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   390
val lookup_const = add_suffix suffix_const
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   391
  oo Symtab.lookup o fst o #const o dest_Naming;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   392
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   393
fun declare_class thy = declare thy map_class
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   394
  lookup_class Symtab.update_new namify_class;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   395
fun declare_classrel thy = declare thy map_classrel
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   396
  lookup_classrel Symreltab.update_new namify_classrel;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   397
fun declare_tyco thy = declare thy map_tyco
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   398
  lookup_tyco Symtab.update_new namify_tyco;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   399
fun declare_instance thy = declare thy map_instance
30648
17365ef082f3 clarified relationship of modules Code_Name and Code_Printer
haftmann
parents: 30364
diff changeset
   400
  lookup_instance Symreltab.update_new namify_instance;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   401
fun declare_const thy = declare thy map_const
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   402
  lookup_const Symtab.update_new namify_const;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   403
31054
841c9f67f9e7 explicit type arguments in constants
haftmann
parents: 31049
diff changeset
   404
fun ensure_declared_const thy const naming =
841c9f67f9e7 explicit type arguments in constants
haftmann
parents: 31049
diff changeset
   405
  case lookup_const naming const
841c9f67f9e7 explicit type arguments in constants
haftmann
parents: 31049
diff changeset
   406
   of SOME const' => (const', naming)
841c9f67f9e7 explicit type arguments in constants
haftmann
parents: 31049
diff changeset
   407
    | NONE => declare_const thy const naming;
841c9f67f9e7 explicit type arguments in constants
haftmann
parents: 31049
diff changeset
   408
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   409
val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   410
  (*depends on add_suffix*);
34084
05cb31ca48ae explicit name for function space
haftmann
parents: 34013
diff changeset
   411
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   412
val unfold_fun = unfoldr
34084
05cb31ca48ae explicit name for function space
haftmann
parents: 34013
diff changeset
   413
  (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   414
    | _ => NONE);
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   415
37640
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   416
fun unfold_fun_n n ty =
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   417
  let
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   418
    val (tys1, ty1) = unfold_fun ty;
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   419
    val (tys3, tys2) = chop n tys1;
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   420
    val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   421
  in (tys3, ty3) end;
fc27be4c6b1c unfold_fun_n
haftmann
parents: 37448
diff changeset
   422
28688
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   423
end; (* local *)
1a9fabb515cd "fun" gained a more uniform status
haftmann
parents: 28663
diff changeset
   424
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   425
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   426
(** statements, abstract programs **)
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   427
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   428
type typscheme = (vname * sort) list * itype;
37447
ad3e04f289b6 transitive superclasses were also only a misunderstanding
haftmann
parents: 37446
diff changeset
   429
datatype stmt =
27024
fcab2dd46872 various code streamlining
haftmann
parents: 26972
diff changeset
   430
    NoStmt
37437
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
   431
  | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   432
  | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   433
  | Datatypecons of string * string
37447
ad3e04f289b6 transitive superclasses were also only a misunderstanding
haftmann
parents: 37446
diff changeset
   434
  | Class of class * (vname * ((class * string) list * (string * itype) list))
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   435
  | Classrel of class * class
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   436
  | Classparam of string * class
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   437
  | Classinst of (class * (string * (vname * sort) list))
37445
e372fa3c7239 dropped obscure type argument weakening mapping -- was only a misunderstanding
haftmann
parents: 37440
diff changeset
   438
        * ((class * (string * (string * dict list list))) list
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   439
      * (((string * const) * (thm * bool)) list
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   440
        * ((string * const) * (thm * bool)) list))
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   441
      (*see also signature*);
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   442
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   443
type program = stmt Graph.T;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   444
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   445
fun empty_funs program =
37437
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
   446
  Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   447
               | _ => I) program [];
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   448
27711
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   449
fun map_terms_bottom_up f (t as IConst _) = f t
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   450
  | map_terms_bottom_up f (t as IVar _) = f t
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   451
  | map_terms_bottom_up f (t1 `$ t2) = f
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   452
      (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
31724
9b5a128cdb5c more appropriate syntax for IML abstraction
haftmann
parents: 31156
diff changeset
   453
  | map_terms_bottom_up f ((v, ty) `|=> t) = f
9b5a128cdb5c more appropriate syntax for IML abstraction
haftmann
parents: 31156
diff changeset
   454
      ((v, ty) `|=> map_terms_bottom_up f t)
27711
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   455
  | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   456
      (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   457
        (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   458
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   459
fun map_classparam_instances_as_term f =
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   460
  (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   461
27711
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   462
fun map_terms_stmt f NoStmt = NoStmt
37437
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
   463
  | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
   464
      (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
27711
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   465
  | map_terms_stmt f (stmt as Datatype _) = stmt
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   466
  | map_terms_stmt f (stmt as Datatypecons _) = stmt
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   467
  | map_terms_stmt f (stmt as Class _) = stmt
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   468
  | map_terms_stmt f (stmt as Classrel _) = stmt
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   469
  | map_terms_stmt f (stmt as Classparam _) = stmt
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   470
  | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   471
      Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
27711
5052736b8bcc simple lifters
haftmann
parents: 27609
diff changeset
   472
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   473
fun is_cons program name = case Graph.get_node program name
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   474
 of Datatypecons _ => true
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   475
  | _ => false;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   476
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   477
fun is_case (Fun (_, (_, SOME _))) = true
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   478
  | is_case _ = false;
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   479
43048
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   480
fun lookup_classparam_instance program name = program |> Graph.get_first
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   481
  (fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   482
    Option.map (fn ((const, _), _) => (class, const))
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   483
      (find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   484
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   485
fun contr_classparam_typs program name = 
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   486
  let
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   487
    fun contr_classparam_typs' (class, name) =
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   488
      let
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   489
        val Class (_, (_, (_, params))) = Graph.get_node program class;
25621
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   490
        val SOME ty = AList.lookup (op =) params name;
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   491
        val (tys, res_ty) = unfold_fun ty;
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   492
        fun no_tyvar (_ `%% tys) = forall no_tyvar tys
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   493
          | no_tyvar (ITyVar _) = false;
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   494
      in if no_tyvar res_ty
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   495
        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
   496
        else []
97ebdbdb0299 heutistics for type annotations in Haskell
haftmann
parents: 25597
diff changeset
   497
      end
43048
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   498
 in 
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   499
   case Graph.get_node program name
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   500
   of Classparam (_, class) => contr_classparam_typs' (class, name)
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   501
    | Fun (c, _) => (case lookup_classparam_instance program name
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   502
      of NONE => []
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   503
       | SOME (class, name) => the_default [] (try contr_classparam_typs' (class, name)))
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   504
    | _ => []
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   505
  end;
c62bed03fbce improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents: 42385
diff changeset
   506
  
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   507
fun labelled_name thy program name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   508
  let val ctxt = Proof_Context.init_global thy in
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   509
    case Graph.get_node program name of
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   510
      Fun (c, _) => quote (Code.string_of_const thy c)
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   511
    | Datatype (tyco, _) => "type " ^ quote (Proof_Context.extern_type ctxt tyco)
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   512
    | Datatypecons (c, _) => quote (Code.string_of_const thy c)
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   513
    | Class (class, _) => "class " ^ quote (Proof_Context.extern_class ctxt class)
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   514
    | Classrel (sub, super) =>
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   515
        let
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   516
          val Class (sub, _) = Graph.get_node program sub;
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   517
          val Class (super, _) = Graph.get_node program super;
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   518
        in
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   519
          quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   520
        end
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   521
    | Classparam (c, _) => quote (Code.string_of_const thy c)
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   522
    | Classinst ((class, (tyco, _)), _) =>
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   523
        let
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   524
          val Class (class, _) = Graph.get_node program class;
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   525
          val Datatype (tyco, _) = Graph.get_node program tyco;
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   526
        in
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   527
          quote (Proof_Context.extern_type ctxt tyco ^ " :: " ^ Proof_Context.extern_class ctxt class)
42359
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   528
        end
6ca5407863ed prefer local name spaces;
wenzelm
parents: 42284
diff changeset
   529
  end;
32895
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   530
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   531
fun linear_stmts program =
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   532
  rev (Graph.strong_conn program)
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   533
  |> map (AList.make (Graph.get_node program));
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   534
32895
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   535
fun group_stmts thy program =
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   536
  let
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   537
    fun is_fun (_, Fun _) = true | is_fun _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   538
    fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   539
    fun is_datatype (_, Datatype _) = true | is_datatype _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   540
    fun is_class (_, Class _) = true | is_class _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   541
    fun is_classrel (_, Classrel _) = true | is_classrel _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   542
    fun is_classparam (_, Classparam _) = true | is_classparam _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   543
    fun is_classinst (_, Classinst _) = true | is_classinst _ = false;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   544
    fun group stmts =
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   545
      if forall (is_datatypecons orf is_datatype) stmts
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   546
      then (filter is_datatype stmts, [], ([], []))
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   547
      else if forall (is_class orf is_classrel orf is_classparam) stmts
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   548
      then ([], filter is_class stmts, ([], []))
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   549
      else if forall (is_fun orf is_classinst) stmts
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   550
      then ([], [], List.partition is_fun stmts)
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   551
      else error ("Illegal mutual dependencies: " ^
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   552
        (commas o map (labelled_name thy program o fst)) stmts)
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   553
  in
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   554
    linear_stmts program
32895
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   555
    |> map group
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   556
  end;
6f3cdb4a9e11 added group_stmts
haftmann
parents: 32873
diff changeset
   557
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   558
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   559
(** translation kernel **)
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   560
28724
haftmann
parents: 28708
diff changeset
   561
(* generic mechanisms *)
haftmann
parents: 28708
diff changeset
   562
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   563
fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   564
  let
28706
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   565
    fun add_dep name = case dep of NONE => I
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   566
      | SOME dep => Graph.add_edge (dep, name);
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   567
    val (name, naming') = case lookup naming thing
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   568
     of SOME name => (name, naming)
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   569
      | NONE => declare thing naming;
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   570
  in case try (Graph.get_node program) name
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   571
   of SOME stmt => program
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   572
        |> add_dep name
28706
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   573
        |> pair naming'
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   574
        |> pair dep
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   575
        |> pair name
28706
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   576
    | NONE => program
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   577
        |> Graph.default_node (name, NoStmt)
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   578
        |> add_dep name
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   579
        |> pair naming'
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   580
        |> curry generate (SOME name)
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   581
        ||> snd
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   582
        |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   583
        |> pair dep
3fef773ae6b1 restored incremental code generation
haftmann
parents: 28688
diff changeset
   584
        |> pair name
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   585
  end;
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   586
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   587
exception PERMISSIVE of unit;
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   588
37698
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   589
fun translation_error thy permissive some_thm msg sub_msg =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   590
  if permissive
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   591
  then raise PERMISSIVE ()
42385
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   592
  else
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   593
    let
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   594
      val err_thm =
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   595
        (case some_thm of
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   596
          SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   597
        | NONE => "");
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   598
    in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
37698
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   599
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   600
fun not_wellsorted thy permissive some_thm ty sort e =
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   601
  let
42385
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   602
    val ctxt = Syntax.init_pretty_global thy;
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   603
    val err_class = Sorts.class_error ctxt e;
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   604
    val err_typ =
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   605
      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   606
        Syntax.string_of_sort_global thy sort;
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   607
  in
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   608
    translation_error thy permissive some_thm "Wellsortedness error"
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   609
      (err_typ ^ "\n" ^ err_class)
b46b47775cbe simplified Sorts.class_error: plain Proof.context;
wenzelm
parents: 42383
diff changeset
   610
  end;
26972
haftmann
parents: 26939
diff changeset
   611
44790
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   612
(* inference of type annotations for disambiguation with type classes *)
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   613
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   614
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   615
fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   616
    let
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   617
      val tvar_names' = Term.add_tvar_namesT T' tvar_names
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   618
    in
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   619
      (Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names')
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   620
    end
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   621
  | annotate_term (t1 $ u1, t $ u) tvar_names =
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   622
    let
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   623
      val (u', tvar_names') = annotate_term (u1, u) tvar_names
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   624
      val (t', tvar_names'') = annotate_term (t1, t) tvar_names'    
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   625
    in
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   626
      (t' $ u', tvar_names'')
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   627
    end
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   628
  | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   629
    apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   630
  | annotate_term (_, t) tvar_names = (t, tvar_names)
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   631
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   632
fun annotate_eqns thy eqns = 
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   633
  let
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   634
    val ctxt = ProofContext.init_global thy
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   635
    val erase = map_types (fn _ => Type_Infer.anyT [])
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   636
    val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   637
    fun add_annotations ((args, (rhs, some_abs)), (SOME th, proper)) =
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   638
      let
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   639
        val (lhs, drhs) = Logic.dest_equals (prop_of (Thm.unvarify_global th))
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   640
        val drhs' = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase drhs))))
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   641
        val (rhs', _) = annotate_term (drhs', rhs) []
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   642
     in
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   643
        ((args, (rhs', some_abs)), (SOME th, proper))
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   644
     end
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   645
     | add_annotations eqn = eqn
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   646
  in
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   647
    map add_annotations eqns
c13fdf710a40 adding type inference for disambiguation annotations in code equation
bulwahn
parents: 44789
diff changeset
   648
  end;
28724
haftmann
parents: 28708
diff changeset
   649
haftmann
parents: 28708
diff changeset
   650
(* translation *)
haftmann
parents: 28708
diff changeset
   651
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   652
fun ensure_tyco thy algbr eqngr permissive tyco =
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   653
  let
40726
16dcfedc4eb7 keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents: 40711
diff changeset
   654
    val ((vs, cos), _) = Code.get_type thy tyco;
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   655
    val stmt_datatype =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   656
      fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
40726
16dcfedc4eb7 keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents: 40711
diff changeset
   657
      ##>> fold_map (fn (c, (vs, tys)) =>
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   658
        ensure_const thy algbr eqngr permissive c
40726
16dcfedc4eb7 keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents: 40711
diff changeset
   659
        ##>> pair (map (unprefix "'" o fst) vs)
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   660
        ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   661
      #>> (fn info => Datatype (tyco, info));
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   662
  in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   663
and ensure_const thy algbr eqngr permissive c =
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   664
  let
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   665
    fun stmt_datatypecons tyco =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   666
      ensure_tyco thy algbr eqngr permissive tyco
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   667
      #>> (fn tyco => Datatypecons (c, tyco));
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   668
    fun stmt_classparam class =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   669
      ensure_class thy algbr eqngr permissive class
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   670
      #>> (fn class => Classparam (c, class));
34891
99b9a6290446 code certificates as integral part of code generation
haftmann
parents: 34251
diff changeset
   671
    fun stmt_fun cert =
32872
019201eb7e07 variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents: 32795
diff changeset
   672
      let
35226
b987b803616d a simple concept for datatype invariants
haftmann
parents: 34895
diff changeset
   673
        val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   674
        val some_case_cong = Code.get_case_cong thy c;
32872
019201eb7e07 variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents: 32795
diff changeset
   675
      in
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   676
        fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   677
        ##>> translate_typ thy algbr eqngr permissive ty
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   678
        ##>> translate_eqns thy algbr eqngr permissive eqns
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   679
        #>> (fn info => Fun (c, (info, some_case_cong)))
32872
019201eb7e07 variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents: 32795
diff changeset
   680
      end;
35299
4f4d5bf4ea08 proper distinction of code datatypes and abstypes
haftmann
parents: 35226
diff changeset
   681
    val stmt_const = case Code.get_type_of_constr_or_abstr thy c
35226
b987b803616d a simple concept for datatype invariants
haftmann
parents: 34895
diff changeset
   682
     of SOME (tyco, _) => stmt_datatypecons tyco
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   683
      | NONE => (case AxClass.class_of_param thy c
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   684
         of SOME class => stmt_classparam class
34891
99b9a6290446 code certificates as integral part of code generation
haftmann
parents: 34251
diff changeset
   685
          | NONE => stmt_fun (Code_Preproc.cert eqngr c))
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   686
  in ensure_stmt lookup_const (declare_const thy) stmt_const c end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   687
and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   688
  let
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   689
    val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
24969
b38527eefb3b removed obsolete AxClass.params_of_class;
wenzelm
parents: 24918
diff changeset
   690
    val cs = #params (AxClass.get_info thy class);
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   691
    val stmt_class =
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   692
      fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   693
        ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   694
      ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   695
        ##>> translate_typ thy algbr eqngr permissive ty) cs
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   696
      #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   697
  in ensure_stmt lookup_class (declare_class thy) stmt_class class end
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   698
and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   699
  let
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   700
    val stmt_classrel =
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   701
      ensure_class thy algbr eqngr permissive sub_class
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   702
      ##>> ensure_class thy algbr eqngr permissive super_class
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   703
      #>> Classrel;
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   704
  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   705
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   706
  let
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   707
    val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   708
    val these_classparams = these o try (#params o AxClass.get_info thy);
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   709
    val classparams = these_classparams class;
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   710
    val further_classparams = maps these_classparams
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   711
      ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   712
    val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   713
    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   714
    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   715
      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   716
    val arity_typ = Type (tyco, map TFree vs);
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   717
    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   718
    fun translate_super_instance super_class =
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   719
      ensure_class thy algbr eqngr permissive super_class
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   720
      ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   721
      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   722
      #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   723
            (super_class, (classrel, (inst, dss))));
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   724
    fun translate_classparam_instance (c, ty) =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   725
      let
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   726
        val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   727
        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   728
        val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   729
          o Logic.dest_equals o Thm.prop_of) thm;
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   730
      in
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   731
        ensure_const thy algbr eqngr permissive c
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   732
        ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   733
        #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   734
      end;
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   735
    val stmt_inst =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   736
      ensure_class thy algbr eqngr permissive class
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   737
      ##>> ensure_tyco thy algbr eqngr permissive tyco
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   738
      ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
37384
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   739
      ##>> fold_map translate_super_instance super_classes
5aba26803073 more consistent naming aroud type classes and instances
haftmann
parents: 37216
diff changeset
   740
      ##>> fold_map translate_classparam_instance classparams
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   741
      ##>> fold_map translate_classparam_instance further_classparams
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   742
      #>> (fn (((((class, tyco), arity_args), super_instances),
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   743
        classparam_instances), further_classparam_instances) =>
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   744
          Classinst ((class, (tyco, arity_args)), (super_instances,
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   745
            (classparam_instances, further_classparam_instances))));
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   746
  in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   747
and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   748
      pair (ITyVar (unprefix "'" v))
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   749
  | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   750
      ensure_tyco thy algbr eqngr permissive tyco
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   751
      ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   752
      #>> (fn (tyco, tys) => tyco `%% tys)
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   753
and translate_term thy algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   754
      translate_app thy algbr eqngr permissive some_thm (((c, ty), []), some_abs)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   755
  | translate_term thy algbr eqngr permissive some_thm (Free (v, _), some_abs) =
31889
fb2c8a687529 all variable names are optional
haftmann
parents: 31888
diff changeset
   756
      pair (IVar (SOME v))
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   757
  | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   758
      let
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 41782
diff changeset
   759
        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
32273
3c395fc7ec5e abstractions: desymbolize name hint
haftmann
parents: 32131
diff changeset
   760
        val v'' = if member (op =) (Term.add_free_names t' []) v'
3c395fc7ec5e abstractions: desymbolize name hint
haftmann
parents: 32131
diff changeset
   761
          then SOME v' else NONE
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   762
      in
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   763
        translate_typ thy algbr eqngr permissive ty
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   764
        ##>> translate_term thy algbr eqngr permissive some_thm (t', some_abs)
32273
3c395fc7ec5e abstractions: desymbolize name hint
haftmann
parents: 32131
diff changeset
   765
        #>> (fn (ty, t) => (v'', ty) `|=> t)
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   766
      end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   767
  | translate_term thy algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   768
      case strip_comb t
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   769
       of (Const (c, ty), ts) =>
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   770
            translate_app thy algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   771
        | (t', ts) =>
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   772
            translate_term thy algbr eqngr permissive some_thm (t', some_abs)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   773
            ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   774
            #>> (fn (t, ts) => t `$$ ts)
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   775
and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   776
  fold_map (translate_term thy algbr eqngr permissive some_thm) args
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   777
  ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
35226
b987b803616d a simple concept for datatype invariants
haftmann
parents: 34895
diff changeset
   778
  #>> rpair (some_thm, proper)
37440
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   779
and translate_eqns thy algbr eqngr permissive eqns prgrm =
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   780
  prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns
a5d44161ba2a maintain cong rules for case combinators; more precise permissiveness
haftmann
parents: 37437
diff changeset
   781
    handle PERMISSIVE () => ([], prgrm)
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   782
and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   783
  let
37698
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   784
    val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
35226
b987b803616d a simple concept for datatype invariants
haftmann
parents: 34895
diff changeset
   785
        andalso Code.is_abstr thy c
37698
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   786
        then translation_error thy permissive some_thm
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   787
          "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   788
      else ()
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   789
    val arg_typs = Sign.const_typargs thy (c, ty);
32873
333945c9ac6a tuned handling of type variable names further
haftmann
parents: 32872
diff changeset
   790
    val sorts = Code_Preproc.sortargs eqngr c;
44789
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   791
    val (function_typs, body_typ) = Term.strip_type ty;
26972
haftmann
parents: 26939
diff changeset
   792
  in
37698
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   793
    ensure_const thy algbr eqngr permissive c
37448
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   794
    ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
3bd4b3809bee explicit type variable arguments for constructors
haftmann
parents: 37447
diff changeset
   795
    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
44789
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   796
    ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   797
    #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   798
      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *)
26972
haftmann
parents: 26939
diff changeset
   799
  end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   800
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   801
  translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   802
  ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   803
  #>> (fn (t, ts) => t `$$ ts)
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   804
and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   805
  let
40844
5895c525739d more direct use of binder_types/body_type;
wenzelm
parents: 40726
diff changeset
   806
    fun arg_types num_args ty = fst (chop num_args (binder_types ty));
31892
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   807
    val tys = arg_types num_args (snd c_ty);
29952
9aed85067721 unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents: 29277
diff changeset
   808
    val ty = nth tys t_pos;
31957
a9742afd403e tuned interface of structure Code
haftmann
parents: 31935
diff changeset
   809
    fun mk_constr c t = let val n = Code.args_number thy c
a9742afd403e tuned interface of structure Code
haftmann
parents: 31935
diff changeset
   810
      in ((c, arg_types n (fastype_of t) ---> ty), n) end;
31892
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   811
    val constrs = if null case_pats then []
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   812
      else map2 mk_constr case_pats (nth_drop t_pos ts);
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   813
    fun casify naming constrs ty ts =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   814
      let
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   815
        val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   816
        fun collapse_clause vs_map ts body =
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   817
          let
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   818
          in case body
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   819
           of IConst (c, _) => if member (op =) undefineds c
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   820
                then []
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   821
                else [(ts, body)]
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   822
            | ICase (((IVar (SOME v), _), subclauses), _) =>
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   823
                if forall (fn (pat', body') => exists_var pat' v
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   824
                  orelse not (exists_var body' v)) subclauses
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   825
                then case AList.lookup (op =) vs_map v
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   826
                 of SOME i => maps (fn (pat', body') =>
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   827
                      collapse_clause (AList.delete (op =) v vs_map)
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   828
                        (nth_map i (K pat') ts) body') subclauses
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   829
                  | NONE => [(ts, body)]
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   830
                else [(ts, body)]
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   831
            | _ => [(ts, body)]
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   832
          end;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   833
        fun mk_clause mk tys t =
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   834
          let
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   835
            val (vs, body) = unfold_abs_eta tys t;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   836
            val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   837
            val ts = map (IVar o fst) vs;
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   838
          in map mk (collapse_clause vs_map ts body) end;
31892
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   839
        val t = nth ts t_pos;
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   840
        val ts_clause = nth_drop t_pos ts;
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   841
        val clauses = if null case_pats
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   842
          then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
44789
5a062c23c7db adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents: 44788
diff changeset
   843
          else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   844
            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
31935
3896169e6ff9 cleaned up fundamental iml term functions; nested patterns
haftmann
parents: 31892
diff changeset
   845
              (constrs ~~ ts_clause);
31892
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   846
      in ((t, ty), clauses) end;
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   847
  in
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   848
    translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   849
    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   850
      #>> rpair n) constrs
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   851
    ##>> translate_typ thy algbr eqngr permissive ty
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   852
    ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
31892
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   853
    #-> (fn (((t, constrs), ty), ts) =>
a2139b503981 improved treatment of case patterns
haftmann
parents: 31890
diff changeset
   854
      `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   855
  end
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   856
and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
29973
haftmann
parents: 29962
diff changeset
   857
  if length ts < num_args then
haftmann
parents: 29962
diff changeset
   858
    let
haftmann
parents: 29962
diff changeset
   859
      val k = length ts;
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   860
      val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
29973
haftmann
parents: 29962
diff changeset
   861
      val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   862
      val vs = Name.invent_names ctxt "a" tys;
29973
haftmann
parents: 29962
diff changeset
   863
    in
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   864
      fold_map (translate_typ thy algbr eqngr permissive) tys
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   865
      ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
31888
626c075fd457 variable names in abstractions are optional
haftmann
parents: 31874
diff changeset
   866
      #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
29973
haftmann
parents: 29962
diff changeset
   867
    end
haftmann
parents: 29962
diff changeset
   868
  else if length ts > num_args then
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   869
    translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   870
    ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
29973
haftmann
parents: 29962
diff changeset
   871
    #>> (fn (t, ts) => t `$$ ts)
haftmann
parents: 29962
diff changeset
   872
  else
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   873
    translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   874
and translate_app thy algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
29973
haftmann
parents: 29962
diff changeset
   875
  case Code.get_case_scheme thy c
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   876
   of SOME case_scheme => translate_app_case thy algbr eqngr permissive some_thm case_scheme c_ty_ts
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   877
    | NONE => translate_app_const thy algbr eqngr permissive some_thm (c_ty_ts, some_abs)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   878
and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   879
  fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   880
  #>> (fn sort => (unprefix "'" v, sort))
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   881
and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   882
  let
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   883
    datatype typarg_witness =
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   884
        Weakening of (class * class) list * plain_typarg_witness
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   885
    and plain_typarg_witness =
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   886
        Global of (class * string) * typarg_witness list list
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   887
      | Local of string * (int * sort);
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   888
    fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   889
      Weakening ((sub_class, super_class) :: classrels, x);
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   890
    fun type_constructor (tyco, _) dss class =
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   891
      Weakening ([], Global ((class, tyco), (map o map) fst dss));
30932
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   892
    fun type_variable (TFree (v, sort)) =
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   893
      let
35f255987e18 tuned order of functions
haftmann
parents: 30648
diff changeset
   894
        val sort' = proj_sort sort;
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   895
      in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   896
    val typarg_witnesses = Sorts.of_sort_derivation algebra
36102
a51d1d154c71 of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
wenzelm
parents: 35961
diff changeset
   897
      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
35961
00e48e1d9afd Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents: 35845
diff changeset
   898
       type_constructor = type_constructor,
37698
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   899
       type_variable = type_variable} (ty, proj_sort sort)
e38abf437c20 reverted to verion from fc27be4c6b1c
haftmann
parents: 37697
diff changeset
   900
      handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   901
    fun mk_dict (Weakening (classrels, x)) =
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   902
          fold_map (ensure_classrel thy algbr eqngr permissive) classrels
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   903
          ##>> mk_plain_dict x
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   904
          #>> Dict 
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   905
    and mk_plain_dict (Global (inst, dss)) =
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   906
          ensure_inst thy algbr eqngr permissive inst
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   907
          ##>> (fold_map o fold_map) mk_dict dss
41118
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   908
          #>> (fn (inst, dss) => Dict_Const (inst, dss))
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   909
      | mk_plain_dict (Local (v, (n, sort))) =
b290841cd3b0 separated dictionary weakning into separate type
haftmann
parents: 41100
diff changeset
   910
          pair (Dict_Var (unprefix "'" v, (n, length sort)))
41100
6c0940392fb4 dictionary constants must permit explicit weakening of classes;
haftmann
parents: 40844
diff changeset
   911
  in fold_map mk_dict typarg_witnesses end;
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   912
25969
haftmann
parents: 25621
diff changeset
   913
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   914
(* store *)
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   915
34173
458ced35abb8 reduced code generator cache to the baremost minimum
haftmann
parents: 34084
diff changeset
   916
structure Program = Code_Data
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   917
(
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   918
  type T = naming * program;
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   919
  val empty = (empty_naming, Graph.empty);
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   920
);
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   921
39397
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
   922
fun invoke_generation ignore_cache thy (algebra, eqngr) f name =
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
   923
  Program.change_yield (if ignore_cache then NONE else SOME thy)
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
   924
    (fn naming_program => (NONE, naming_program)
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
   925
      |> f thy algebra eqngr name
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
   926
      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   927
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   928
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   929
(* program generation *)
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   930
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   931
fun consts_program thy permissive consts =
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   932
  let
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   933
    fun project_consts consts (naming, program) =
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   934
      if permissive then (consts, (naming, program))
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   935
      else (consts, (naming, Graph.subgraph
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   936
        (member (op =) (Graph.all_succs program consts)) program));
32873
333945c9ac6a tuned handling of type variable names further
haftmann
parents: 32872
diff changeset
   937
    fun generate_consts thy algebra eqngr =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   938
      fold_map (ensure_const thy algebra eqngr permissive);
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   939
  in
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   940
    invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   941
      generate_consts consts
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   942
    |-> project_consts
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   943
  end;
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   944
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   945
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   946
(* value evaluation *)
25969
haftmann
parents: 25621
diff changeset
   947
32873
333945c9ac6a tuned handling of type variable names further
haftmann
parents: 32872
diff changeset
   948
fun ensure_value thy algbr eqngr t =
24918
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   949
  let
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   950
    val ty = fastype_of t;
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   951
    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   952
      o dest_TFree))) t [];
22013215eece moved translation kernel to CodeThingol
haftmann
parents: 24837
diff changeset
   953
    val stmt_value =
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   954
      fold_map (translate_tyvar_sort thy algbr eqngr false) vs
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   955
      ##>> translate_typ thy algbr eqngr false ty
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
   956
      ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   957
      #>> (fn ((vs, ty), t) => Fun
37437
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
   958
        (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
31063
88aaab83b6fc dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents: 31054
diff changeset
   959
    fun term_value (dep, (naming, program1)) =
25969
haftmann
parents: 25621
diff changeset
   960
      let
37437
4202e11ae7dc formal introduction of case cong
haftmann
parents: 37431
diff changeset
   961
        val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   962
          Graph.get_node program1 Term.dummy_patternN;
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43329
diff changeset
   963
        val deps = Graph.immediate_succs program1 Term.dummy_patternN;
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   964
        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   965
        val deps_all = Graph.all_succs program2 deps;
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
   966
        val program3 = Graph.subgraph (member (op =) deps_all) program2;
31063
88aaab83b6fc dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents: 31054
diff changeset
   967
      in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
26011
d55224947082 cleaned up evaluation interfaces
haftmann
parents: 25969
diff changeset
   968
  in
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28423
diff changeset
   969
    ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
26011
d55224947082 cleaned up evaluation interfaces
haftmann
parents: 25969
diff changeset
   970
    #> snd
31063
88aaab83b6fc dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents: 31054
diff changeset
   971
    #> term_value
26011
d55224947082 cleaned up evaluation interfaces
haftmann
parents: 25969
diff changeset
   972
  end;
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
   973
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   974
fun original_sorts vs =
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   975
  map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   976
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   977
fun dynamic_evaluator thy evaluator algebra eqngr vs t =
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
   978
  let
31063
88aaab83b6fc dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents: 31054
diff changeset
   979
    val (((naming, program), (((vs', ty'), t'), deps)), _) =
39397
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
   980
      invoke_generation false thy (algebra, eqngr) ensure_value t;
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   981
  in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
   982
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   983
fun dynamic_conv thy evaluator =
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   984
  Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
39475
9cc1ba3c5706 separation of static and dynamic thy context
haftmann
parents: 39397
diff changeset
   985
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   986
fun dynamic_value thy postproc evaluator =
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
   987
  Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
   988
41365
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   989
fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   990
  let
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   991
    val (((_, program'), (((vs', ty'), t'), deps)), _) =
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
   992
      ensure_value thy algebra eqngr t (NONE, (naming, program));
41365
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   993
  in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   994
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   995
fun lift_evaluator thy evaluator' consts algebra eqngr =
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   996
  let
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   997
    fun generate_consts thy algebra eqngr =
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   998
      fold_map (ensure_const thy algebra eqngr false);
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
   999
    val (consts', (naming, program)) =
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1000
      invoke_generation true thy (algebra, eqngr) generate_consts consts;
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1001
    val evaluation' = evaluator' naming program consts';
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1002
  in lift_evaluation thy evaluation' algebra eqngr naming program end;
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1003
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1004
fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1005
  let
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1006
    fun generate_consts thy algebra eqngr =
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1007
      fold_map (ensure_const thy algebra eqngr false);
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1008
    val (consts', (naming, program)) =
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1009
      invoke_generation true thy (algebra, eqngr) generate_consts consts;
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1010
  in evaluator' program end;
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
  1011
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
  1012
fun static_conv thy consts conv =
41365
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1013
  Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
38672
f1f64375f662 preliminary versions of static_eval_conv(_simple)
haftmann
parents: 38669
diff changeset
  1014
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
  1015
fun static_conv_simple thy consts conv =
41365
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1016
  Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
38672
f1f64375f662 preliminary versions of static_eval_conv(_simple)
haftmann
parents: 38669
diff changeset
  1017
41184
5c6f44d22f51 simplified evaluation function names
haftmann
parents: 41118
diff changeset
  1018
fun static_value thy postproc consts evaluator =
41365
54dfe5c584e8 proper static closures
haftmann
parents: 41346
diff changeset
  1019
  Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
39487
80b2cf3b0779 proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents: 39475
diff changeset
  1020
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1021
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1022
(** diagnostic commands **)
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1023
31036
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
  1024
fun read_const_exprs thy =
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
  1025
  let
36272
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
  1026
    fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
  1027
      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
  1028
    fun belongs_here thy' c = forall
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
  1029
      (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
4d358c582ffb optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents: 36210
diff changeset
  1030
    fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
40711
81bc73585eec globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents: 39566
diff changeset
  1031
    fun read_const_expr "_" = ([], consts_of thy)
81bc73585eec globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents: 39566
diff changeset
  1032
      | read_const_expr s = if String.isSuffix "._" s
81bc73585eec globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents: 39566
diff changeset
  1033
          then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
31156
90fed3d4430f merged module code_unit.ML into code.ML
haftmann
parents: 31125
diff changeset
  1034
          else ([Code.read_const thy s], []);
31036
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
  1035
  in pairself flat o split_list o map read_const_expr end;
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
  1036
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1037
fun code_depgr thy consts =
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1038
  let
39397
9b0a8d72edc8 ignore code cache optionally
haftmann
parents: 39205
diff changeset
  1039
    val (_, eqngr) = Code_Preproc.obtain true thy consts [];
34173
458ced35abb8 reduced code generator cache to the baremost minimum
haftmann
parents: 34084
diff changeset
  1040
    val all_consts = Graph.all_succs eqngr consts;
34891
99b9a6290446 code certificates as integral part of code generation
haftmann
parents: 34251
diff changeset
  1041
  in Graph.subgraph (member (op =) all_consts) eqngr end;
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1042
31125
80218ee73167 transferred code generator preprocessor into separate module
haftmann
parents: 31088
diff changeset
  1043
fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1044
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1045
fun code_deps thy consts =
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
  1046
  let
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1047
    val eqngr = code_depgr thy consts;
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1048
    val constss = Graph.strong_conn eqngr;
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1049
    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1050
      Symtab.update (const, consts)) consts) constss;
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1051
    fun succs consts = consts
44338
700008399ee5 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents: 43329
diff changeset
  1052
      |> maps (Graph.immediate_succs eqngr)
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1053
      |> subtract (op =) consts
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1054
      |> map (the o Symtab.lookup mapping)
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1055
      |> distinct (op =);
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1056
    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
31156
90fed3d4430f merged module code_unit.ML into code.ML
haftmann
parents: 31125
diff changeset
  1057
    fun namify consts = map (Code.string_of_const thy) consts
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1058
      |> commas;
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1059
    val prgr = map (fn (consts, constss) =>
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1060
      { name = namify consts, ID = namify consts, dir = "", unfold = true,
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1061
        path = "", parents = map namify constss }) conn;
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1062
  in Present.display_graph prgr end;
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1063
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1064
local
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
  1065
31036
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
  1066
fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
64ff53fc0c0c removed code_name module
haftmann
parents: 30970
diff changeset
  1067
fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1068
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1069
in
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1070
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1071
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36272
diff changeset
  1072
  Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36272
diff changeset
  1073
    (Scan.repeat1 Parse.term_group
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1074
      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1075
        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1076
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1077
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36272
diff changeset
  1078
  Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36272
diff changeset
  1079
    Keyword.diag
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36272
diff changeset
  1080
    (Scan.repeat1 Parse.term_group
30942
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1081
      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1082
        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1083
1e246776f876 diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents: 30932
diff changeset
  1084
end;
27103
d8549f4d900b major refactorings in code generator modules
haftmann
parents: 27024
diff changeset
  1085
24219
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
  1086
end; (*struct*)
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
  1087
e558fe311376 new structure for code generator modules
haftmann
parents:
diff changeset
  1088
28054
2b84d34c5d02 restructured and split code serializer module
haftmann
parents: 27711
diff changeset
  1089
structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;