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