src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
author haftmann
Fri Feb 15 08:31:31 2013 +0100 (2013-02-15)
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 55437 3fd63b92ea3b
permissions -rw-r--r--
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
bulwahn@36046
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
bulwahn@36046
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@36046
     3
wenzelm@41941
     4
Structures for different compilations of the predicate compiler.
bulwahn@36046
     5
*)
bulwahn@36046
     6
bulwahn@45450
     7
structure Predicate_Comp_Funs =
bulwahn@36046
     8
struct
bulwahn@36046
     9
bulwahn@45461
    10
fun mk_monadT T = Type (@{type_name Predicate.pred}, [T])
bulwahn@36046
    11
bulwahn@45461
    12
fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T
bulwahn@45461
    13
  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
bulwahn@36046
    14
bulwahn@45461
    15
fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T);
bulwahn@36046
    16
bulwahn@36046
    17
fun mk_single t =
bulwahn@36046
    18
  let val T = fastype_of t
bulwahn@45461
    19
  in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end;
bulwahn@36046
    20
bulwahn@36046
    21
fun mk_bind (x, f) =
bulwahn@36046
    22
  let val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@36046
    23
  in
bulwahn@36046
    24
    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@36046
    25
  end;
bulwahn@36046
    26
bulwahn@45461
    27
val mk_plus = HOLogic.mk_binop @{const_name sup};
bulwahn@36046
    28
bulwahn@36046
    29
fun mk_if cond = Const (@{const_name Predicate.if_pred},
bulwahn@45461
    30
  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
bulwahn@36046
    31
bulwahn@36049
    32
fun mk_iterate_upto T (f, from, to) =
haftmann@46664
    33
  list_comb (Const (@{const_name Predicate.iterate_upto},
haftmann@51143
    34
      [@{typ natural} --> T, @{typ natural}, @{typ natural}] ---> mk_monadT T),
bulwahn@36049
    35
    [f, from, to])
bulwahn@36049
    36
bulwahn@36046
    37
fun mk_not t =
bulwahn@36046
    38
  let
bulwahn@45461
    39
    val T = mk_monadT HOLogic.unitT
bulwahn@36046
    40
  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
bulwahn@36046
    41
bulwahn@36046
    42
fun mk_Enum f =
bulwahn@36046
    43
  let val T as Type ("fun", [T', _]) = fastype_of f
bulwahn@36046
    44
  in
bulwahn@45461
    45
    Const (@{const_name Predicate.Pred}, T --> mk_monadT T') $ f    
bulwahn@36046
    46
  end;
bulwahn@36046
    47
bulwahn@36046
    48
fun mk_Eval (f, x) =
bulwahn@36046
    49
  let
bulwahn@45461
    50
    val T = dest_monadT (fastype_of f)
bulwahn@36046
    51
  in
bulwahn@45461
    52
    Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
bulwahn@36046
    53
  end;
bulwahn@36046
    54
bulwahn@36046
    55
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
bulwahn@36046
    56
bulwahn@36046
    57
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
bulwahn@45461
    58
  (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp;
bulwahn@36046
    59
bulwahn@36046
    60
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
    61
    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
bulwahn@45461
    62
    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@36049
    63
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
bulwahn@36046
    64
bulwahn@36046
    65
end;
bulwahn@36046
    66
bulwahn@45450
    67
structure CPS_Comp_Funs =
bulwahn@45450
    68
struct
bulwahn@45450
    69
bulwahn@45461
    70
fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
bulwahn@45450
    71
bulwahn@45461
    72
fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
bulwahn@45461
    73
  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
bulwahn@45450
    74
bulwahn@45461
    75
fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T);
bulwahn@45450
    76
bulwahn@45450
    77
fun mk_single t =
bulwahn@45450
    78
  let val T = fastype_of t
bulwahn@45461
    79
  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end;
bulwahn@45450
    80
bulwahn@45450
    81
fun mk_bind (x, f) =
bulwahn@45450
    82
  let val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@45450
    83
  in
bulwahn@45450
    84
    Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@45450
    85
  end;
bulwahn@45450
    86
bulwahn@45461
    87
val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
bulwahn@45450
    88
bulwahn@45450
    89
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
bulwahn@45461
    90
  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
bulwahn@45450
    91
haftmann@50056
    92
fun mk_iterate_upto _ _ = error "not implemented yet"
bulwahn@45450
    93
bulwahn@45450
    94
fun mk_not t =
bulwahn@45450
    95
  let
bulwahn@45461
    96
    val T = mk_monadT HOLogic.unitT
bulwahn@45450
    97
  in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
bulwahn@45450
    98
haftmann@50056
    99
fun mk_Enum _ = error "not implemented"
bulwahn@45450
   100
haftmann@50056
   101
fun mk_Eval _ = error "not implemented"
bulwahn@45450
   102
haftmann@50056
   103
fun dest_Eval _ = error "not implemented"
bulwahn@45450
   104
haftmann@50056
   105
fun mk_map _ _ _ _ = error "not implemented"
bulwahn@45450
   106
bulwahn@45450
   107
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   108
    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
bulwahn@45461
   109
    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@45450
   110
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
bulwahn@45450
   111
bulwahn@45450
   112
end;
bulwahn@45450
   113
bulwahn@45450
   114
structure Pos_Bounded_CPS_Comp_Funs =
bulwahn@45450
   115
struct
bulwahn@45450
   116
bulwahn@45750
   117
val resultT = @{typ "(bool * Code_Evaluation.term list) option"}
haftmann@51143
   118
fun mk_monadT T = (T --> resultT) --> @{typ "natural"} --> resultT
bulwahn@45450
   119
bulwahn@45750
   120
fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]),
haftmann@51143
   121
  @{typ "natural => (bool * term list) option"}])) = T
bulwahn@45461
   122
  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
bulwahn@45450
   123
bulwahn@45461
   124
fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
bulwahn@45450
   125
bulwahn@45450
   126
fun mk_single t =
bulwahn@45450
   127
  let val T = fastype_of t
bulwahn@45461
   128
  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end;
bulwahn@45450
   129
bulwahn@45450
   130
fun mk_bind (x, f) =
bulwahn@45450
   131
  let val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@45450
   132
  in
bulwahn@45450
   133
    Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@45450
   134
  end;
bulwahn@45450
   135
bulwahn@45461
   136
val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
bulwahn@45450
   137
bulwahn@45450
   138
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
bulwahn@45461
   139
  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
bulwahn@45450
   140
haftmann@50056
   141
fun mk_iterate_upto _ _ = error "not implemented yet"
bulwahn@45450
   142
bulwahn@45450
   143
fun mk_not t =
bulwahn@45450
   144
  let
bulwahn@45450
   145
    val nT = @{typ "(unit Quickcheck_Exhaustive.unknown =>
haftmann@51143
   146
      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => natural =>
bulwahn@45450
   147
      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
bulwahn@45461
   148
    val T = mk_monadT HOLogic.unitT
bulwahn@45450
   149
  in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
bulwahn@45450
   150
haftmann@50056
   151
fun mk_Enum _ = error "not implemented"
bulwahn@45450
   152
haftmann@50056
   153
fun mk_Eval _ = error "not implemented"
bulwahn@45450
   154
haftmann@50056
   155
fun dest_Eval _ = error "not implemented"
bulwahn@45450
   156
haftmann@50056
   157
fun mk_map _ _ _ _ = error "not implemented"
bulwahn@45450
   158
bulwahn@45450
   159
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   160
    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
bulwahn@45461
   161
    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@45450
   162
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
bulwahn@45450
   163
bulwahn@45450
   164
end;
bulwahn@45450
   165
bulwahn@45450
   166
structure Neg_Bounded_CPS_Comp_Funs =
bulwahn@45450
   167
struct
bulwahn@45450
   168
bulwahn@45461
   169
fun mk_monadT T =
bulwahn@45450
   170
  (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T])
bulwahn@45450
   171
    --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
haftmann@51143
   172
    --> @{typ "natural => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
bulwahn@45450
   173
bulwahn@45461
   174
fun dest_monadT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
bulwahn@45450
   175
    @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
haftmann@51143
   176
    @{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = T
bulwahn@45461
   177
  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
bulwahn@45450
   178
bulwahn@45461
   179
fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T);
bulwahn@45450
   180
bulwahn@45450
   181
fun mk_single t =
bulwahn@45450
   182
  let val T = fastype_of t
bulwahn@45461
   183
  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end;
bulwahn@45450
   184
bulwahn@45450
   185
fun mk_bind (x, f) =
bulwahn@45450
   186
  let val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@45450
   187
  in
bulwahn@45450
   188
    Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@45450
   189
  end;
bulwahn@45450
   190
bulwahn@45461
   191
val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
bulwahn@45450
   192
bulwahn@45450
   193
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
bulwahn@45461
   194
  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
bulwahn@45450
   195
haftmann@50056
   196
fun mk_iterate_upto _ _ = error "not implemented"
bulwahn@45450
   197
bulwahn@45450
   198
fun mk_not t =
bulwahn@45450
   199
  let
bulwahn@45461
   200
    val T = mk_monadT HOLogic.unitT
bulwahn@45750
   201
    val pT = @{typ "(unit => (bool * Code_Evaluation.term list) option)"}
haftmann@51143
   202
      --> @{typ "natural => (bool * Code_Evaluation.term list) option"}
bulwahn@45450
   203
  in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
bulwahn@45450
   204
haftmann@50056
   205
fun mk_Enum _ = error "not implemented"
bulwahn@45450
   206
haftmann@50056
   207
fun mk_Eval _ = error "not implemented"
bulwahn@45450
   208
haftmann@50056
   209
fun dest_Eval _ = error "not implemented"
bulwahn@45450
   210
haftmann@50056
   211
fun mk_map _ _ _ _  = error "not implemented"
bulwahn@45450
   212
bulwahn@45450
   213
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   214
    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
bulwahn@45461
   215
    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@45450
   216
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
bulwahn@45450
   217
bulwahn@45450
   218
end;
bulwahn@45450
   219
bulwahn@45450
   220
bulwahn@36046
   221
structure RandomPredCompFuns =
bulwahn@36046
   222
struct
bulwahn@36046
   223
bulwahn@36046
   224
fun mk_randompredT T =
bulwahn@45461
   225
  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
bulwahn@36046
   226
haftmann@37678
   227
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
haftmann@51126
   228
  [Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
bulwahn@36046
   229
  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
bulwahn@36046
   230
haftmann@51126
   231
fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
bulwahn@36046
   232
bulwahn@36046
   233
fun mk_single t =
bulwahn@36046
   234
  let               
bulwahn@36046
   235
    val T = fastype_of t
bulwahn@36046
   236
  in
haftmann@51126
   237
    Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
bulwahn@36046
   238
  end;
bulwahn@36046
   239
bulwahn@36046
   240
fun mk_bind (x, f) =
bulwahn@36046
   241
  let
bulwahn@36046
   242
    val T as (Type ("fun", [_, U])) = fastype_of f
bulwahn@36046
   243
  in
haftmann@51126
   244
    Const (@{const_name Random_Pred.bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@36046
   245
  end
bulwahn@36046
   246
haftmann@51126
   247
val mk_plus = HOLogic.mk_binop @{const_name Random_Pred.union}
bulwahn@36046
   248
haftmann@51126
   249
fun mk_if cond = Const (@{const_name Random_Pred.if_randompred},
bulwahn@36046
   250
  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
bulwahn@36046
   251
bulwahn@36049
   252
fun mk_iterate_upto T (f, from, to) =
haftmann@51126
   253
  list_comb (Const (@{const_name Random_Pred.iterate_upto},
haftmann@51143
   254
      [@{typ natural} --> T, @{typ natural}, @{typ natural}] ---> mk_randompredT T),
bulwahn@36049
   255
    [f, from, to])
bulwahn@36049
   256
bulwahn@36046
   257
fun mk_not t =
bulwahn@36046
   258
  let
bulwahn@36046
   259
    val T = mk_randompredT HOLogic.unitT
haftmann@51126
   260
  in Const (@{const_name Random_Pred.not_randompred}, T --> T) $ t end
bulwahn@36046
   261
haftmann@51126
   262
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
bulwahn@36046
   263
  (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
bulwahn@36046
   264
bulwahn@36046
   265
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   266
    {mk_monadT = mk_randompredT, dest_monadT = dest_randompredT,
bulwahn@45461
   267
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@36049
   268
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
bulwahn@36046
   269
bulwahn@36046
   270
end;
bulwahn@36046
   271
bulwahn@36046
   272
structure DSequence_CompFuns =
bulwahn@36046
   273
struct
bulwahn@36046
   274
haftmann@51143
   275
fun mk_dseqT T = Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool},
bulwahn@36046
   276
  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
bulwahn@36046
   277
haftmann@51143
   278
fun dest_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool},
bulwahn@36046
   279
  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
bulwahn@36046
   280
  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
bulwahn@36046
   281
haftmann@51126
   282
fun mk_empty T = Const (@{const_name Limited_Sequence.empty}, mk_dseqT T);
bulwahn@36046
   283
bulwahn@36046
   284
fun mk_single t =
bulwahn@36046
   285
  let val T = fastype_of t
haftmann@51126
   286
  in Const(@{const_name Limited_Sequence.single}, T --> mk_dseqT T) $ t end;
bulwahn@36046
   287
bulwahn@36046
   288
fun mk_bind (x, f) =
bulwahn@36046
   289
  let val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@36046
   290
  in
haftmann@51126
   291
    Const (@{const_name Limited_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@36046
   292
  end;
bulwahn@36046
   293
haftmann@51126
   294
val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.union};
bulwahn@36046
   295
haftmann@51126
   296
fun mk_if cond = Const (@{const_name Limited_Sequence.if_seq},
bulwahn@36046
   297
  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
bulwahn@36046
   298
haftmann@50056
   299
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
bulwahn@36049
   300
bulwahn@36046
   301
fun mk_not t = let val T = mk_dseqT HOLogic.unitT
haftmann@51126
   302
  in Const (@{const_name Limited_Sequence.not_seq}, T --> T) $ t end
bulwahn@36046
   303
haftmann@51126
   304
fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
bulwahn@36046
   305
  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
bulwahn@36046
   306
bulwahn@36046
   307
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   308
    {mk_monadT = mk_dseqT, dest_monadT = dest_dseqT,
bulwahn@45461
   309
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@36049
   310
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@36046
   311
bulwahn@36046
   312
end;
bulwahn@36046
   313
bulwahn@40051
   314
structure New_Pos_DSequence_CompFuns =
bulwahn@40051
   315
struct
bulwahn@40051
   316
bulwahn@40051
   317
fun mk_pos_dseqT T =
haftmann@51143
   318
    @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
bulwahn@40051
   319
haftmann@51143
   320
fun dest_pos_dseqT (Type ("fun", [@{typ natural},
bulwahn@40051
   321
    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
bulwahn@40051
   322
  | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
bulwahn@40051
   323
haftmann@51126
   324
fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T);
bulwahn@40051
   325
bulwahn@40051
   326
fun mk_single t =
bulwahn@40051
   327
  let
bulwahn@40051
   328
    val T = fastype_of t
haftmann@51126
   329
  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
bulwahn@40051
   330
bulwahn@40051
   331
fun mk_bind (x, f) =
bulwahn@40051
   332
  let
bulwahn@40051
   333
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@40051
   334
  in
haftmann@51126
   335
    Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@40051
   336
  end;
bulwahn@40051
   337
  
bulwahn@40051
   338
fun mk_decr_bind (x, f) =
bulwahn@40051
   339
  let
bulwahn@40051
   340
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@40051
   341
  in
haftmann@51126
   342
    Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@40051
   343
  end;
bulwahn@40051
   344
haftmann@51126
   345
val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union};
bulwahn@40051
   346
haftmann@51126
   347
fun mk_if cond = Const (@{const_name Limited_Sequence.pos_if_seq},
bulwahn@40051
   348
  HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
bulwahn@40051
   349
haftmann@50056
   350
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
bulwahn@40051
   351
bulwahn@40051
   352
fun mk_not t =
bulwahn@40051
   353
  let
bulwahn@40051
   354
    val pT = mk_pos_dseqT HOLogic.unitT
bulwahn@40051
   355
    val nT =
haftmann@51143
   356
      @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
bulwahn@40051
   357
        [Type (@{type_name Option.option}, [@{typ unit}])])
haftmann@51126
   358
  in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
bulwahn@40051
   359
haftmann@51126
   360
fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.pos_map},
bulwahn@40051
   361
  (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
bulwahn@40051
   362
bulwahn@40051
   363
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   364
    {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
bulwahn@45461
   365
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@40051
   366
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@40051
   367
bulwahn@40051
   368
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   369
    {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
bulwahn@45461
   370
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@40051
   371
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@40051
   372
bulwahn@40051
   373
end;
bulwahn@40051
   374
bulwahn@40051
   375
structure New_Neg_DSequence_CompFuns =
bulwahn@40051
   376
struct
bulwahn@40051
   377
haftmann@51143
   378
fun mk_neg_dseqT T = @{typ natural} -->
bulwahn@40051
   379
  Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
bulwahn@40051
   380
haftmann@51143
   381
fun dest_neg_dseqT (Type ("fun", [@{typ natural},
bulwahn@40051
   382
    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
bulwahn@40051
   383
  | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
bulwahn@40051
   384
haftmann@51126
   385
fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T);
bulwahn@40051
   386
bulwahn@40051
   387
fun mk_single t =
bulwahn@40051
   388
  let
bulwahn@40051
   389
    val T = fastype_of t
haftmann@51126
   390
  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
bulwahn@40051
   391
bulwahn@40051
   392
fun mk_bind (x, f) =
bulwahn@40051
   393
  let
bulwahn@40051
   394
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@40051
   395
  in
haftmann@51126
   396
    Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@40051
   397
  end;
bulwahn@40051
   398
  
bulwahn@40051
   399
fun mk_decr_bind (x, f) =
bulwahn@40051
   400
  let
bulwahn@40051
   401
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@40051
   402
  in
haftmann@51126
   403
    Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@40051
   404
  end;
bulwahn@40051
   405
haftmann@51126
   406
val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union};
bulwahn@40051
   407
haftmann@51126
   408
fun mk_if cond = Const (@{const_name Limited_Sequence.neg_if_seq},
bulwahn@40051
   409
  HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
bulwahn@40051
   410
haftmann@50056
   411
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
bulwahn@40051
   412
bulwahn@40051
   413
fun mk_not t =
bulwahn@40051
   414
  let
bulwahn@40051
   415
    val nT = mk_neg_dseqT HOLogic.unitT
bulwahn@40051
   416
    val pT =
haftmann@51143
   417
      @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
bulwahn@40051
   418
        [@{typ unit}])
haftmann@51126
   419
  in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
bulwahn@40051
   420
haftmann@51126
   421
fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.neg_map},
bulwahn@40051
   422
  (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
bulwahn@40051
   423
bulwahn@40051
   424
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   425
    {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
bulwahn@45461
   426
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@40051
   427
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@40051
   428
bulwahn@40051
   429
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   430
    {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
bulwahn@45461
   431
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@40051
   432
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@40051
   433
bulwahn@40051
   434
end;
bulwahn@40051
   435
bulwahn@36046
   436
structure New_Pos_Random_Sequence_CompFuns =
bulwahn@36046
   437
struct
bulwahn@36046
   438
bulwahn@36046
   439
fun mk_pos_random_dseqT T =
haftmann@51143
   440
  @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
haftmann@51143
   441
    @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
bulwahn@36046
   442
haftmann@51143
   443
fun dest_pos_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
haftmann@51143
   444
    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
bulwahn@36046
   445
    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
bulwahn@36046
   446
  | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
bulwahn@36046
   447
haftmann@51126
   448
fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
bulwahn@36046
   449
bulwahn@36046
   450
fun mk_single t =
bulwahn@36046
   451
  let
bulwahn@36046
   452
    val T = fastype_of t
haftmann@51126
   453
  in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
bulwahn@36046
   454
bulwahn@36046
   455
fun mk_bind (x, f) =
bulwahn@36046
   456
  let
bulwahn@36046
   457
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@36046
   458
  in
haftmann@51126
   459
    Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@36046
   460
  end;
bulwahn@40051
   461
bulwahn@40049
   462
fun mk_decr_bind (x, f) =
bulwahn@40049
   463
  let
bulwahn@40049
   464
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@40049
   465
  in
haftmann@51126
   466
    Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@40049
   467
  end;
bulwahn@36046
   468
haftmann@51126
   469
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
bulwahn@36046
   470
haftmann@51126
   471
fun mk_if cond = Const (@{const_name Random_Sequence.pos_if_random_dseq},
bulwahn@36046
   472
  HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
bulwahn@36046
   473
bulwahn@36049
   474
fun mk_iterate_upto T (f, from, to) =
haftmann@51126
   475
  list_comb (Const (@{const_name Random_Sequence.pos_iterate_upto},
haftmann@51143
   476
      [@{typ natural} --> T, @{typ natural}, @{typ natural}]
bulwahn@36049
   477
        ---> mk_pos_random_dseqT T),
bulwahn@36049
   478
    [f, from, to])
bulwahn@36049
   479
bulwahn@36046
   480
fun mk_not t =
bulwahn@36046
   481
  let
bulwahn@36046
   482
    val pT = mk_pos_random_dseqT HOLogic.unitT
haftmann@51143
   483
    val nT = @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
haftmann@51143
   484
      @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
bulwahn@36046
   485
        [Type (@{type_name Option.option}, [@{typ unit}])])
bulwahn@36046
   486
haftmann@51126
   487
  in Const (@{const_name Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
bulwahn@36046
   488
haftmann@51126
   489
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.pos_map},
bulwahn@36046
   490
  (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
bulwahn@36046
   491
bulwahn@40049
   492
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   493
    {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
bulwahn@45461
   494
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@40049
   495
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@40049
   496
bulwahn@40049
   497
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   498
    {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
bulwahn@45461
   499
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@36049
   500
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@36046
   501
end;
bulwahn@36046
   502
bulwahn@36046
   503
structure New_Neg_Random_Sequence_CompFuns =
bulwahn@36046
   504
struct
bulwahn@36046
   505
bulwahn@36046
   506
fun mk_neg_random_dseqT T =
haftmann@51143
   507
   @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
haftmann@51143
   508
    @{typ natural} --> 
bulwahn@36046
   509
    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
bulwahn@36046
   510
haftmann@51143
   511
fun dest_neg_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
haftmann@51143
   512
    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
bulwahn@36046
   513
      Type (@{type_name Lazy_Sequence.lazy_sequence},
bulwahn@36046
   514
        [Type (@{type_name Option.option}, [T])])])])])])) = T
bulwahn@36046
   515
  | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
bulwahn@36046
   516
haftmann@51126
   517
fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
bulwahn@36046
   518
bulwahn@36046
   519
fun mk_single t =
bulwahn@36046
   520
  let
bulwahn@36046
   521
    val T = fastype_of t
haftmann@51126
   522
  in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
bulwahn@36046
   523
bulwahn@36046
   524
fun mk_bind (x, f) =
bulwahn@36046
   525
  let
bulwahn@36046
   526
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@36046
   527
  in
haftmann@51126
   528
    Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@36046
   529
  end;
bulwahn@36046
   530
bulwahn@40049
   531
fun mk_decr_bind (x, f) =
bulwahn@40049
   532
  let
bulwahn@40049
   533
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@40049
   534
  in
haftmann@51126
   535
    Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@40049
   536
  end;
bulwahn@40049
   537
haftmann@51126
   538
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union};
bulwahn@36046
   539
haftmann@51126
   540
fun mk_if cond = Const (@{const_name Random_Sequence.neg_if_random_dseq},
bulwahn@36046
   541
  HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
bulwahn@36046
   542
bulwahn@36049
   543
fun mk_iterate_upto T (f, from, to) =
haftmann@51126
   544
  list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
haftmann@51143
   545
      [@{typ natural} --> T, @{typ natural}, @{typ natural}]
bulwahn@36049
   546
        ---> mk_neg_random_dseqT T),
bulwahn@36049
   547
    [f, from, to])
bulwahn@36049
   548
bulwahn@36046
   549
fun mk_not t =
bulwahn@36046
   550
  let
bulwahn@36046
   551
    val nT = mk_neg_random_dseqT HOLogic.unitT
haftmann@51143
   552
    val pT = @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
haftmann@51143
   553
    @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
haftmann@51126
   554
  in Const (@{const_name Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
bulwahn@36046
   555
haftmann@51126
   556
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.neg_map},
bulwahn@36046
   557
  (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
bulwahn@36046
   558
bulwahn@40049
   559
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   560
    {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
bulwahn@45461
   561
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@40049
   562
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@40049
   563
bulwahn@40049
   564
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   565
    {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
bulwahn@45461
   566
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@36049
   567
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@36046
   568
bulwahn@36046
   569
end;
bulwahn@36046
   570
bulwahn@36046
   571
structure Random_Sequence_CompFuns =
bulwahn@36046
   572
struct
bulwahn@36046
   573
bulwahn@36046
   574
fun mk_random_dseqT T =
haftmann@51143
   575
  @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
bulwahn@36046
   576
    HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
bulwahn@36046
   577
haftmann@51143
   578
fun dest_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
bulwahn@36046
   579
  Type ("fun", [@{typ Random.seed},
haftmann@37678
   580
  Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
bulwahn@36046
   581
  | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
bulwahn@36046
   582
bulwahn@45461
   583
fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
bulwahn@36046
   584
bulwahn@36046
   585
fun mk_single t =
bulwahn@36046
   586
  let
bulwahn@36046
   587
    val T = fastype_of t
bulwahn@36046
   588
  in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
bulwahn@36046
   589
bulwahn@36046
   590
fun mk_bind (x, f) =
bulwahn@36046
   591
  let
bulwahn@36046
   592
    val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@36046
   593
  in
bulwahn@36046
   594
    Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@36046
   595
  end;
bulwahn@36046
   596
bulwahn@45461
   597
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union};
bulwahn@36046
   598
bulwahn@36046
   599
fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
bulwahn@36046
   600
  HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
bulwahn@36046
   601
haftmann@50056
   602
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
bulwahn@36049
   603
bulwahn@36046
   604
fun mk_not t =
bulwahn@36046
   605
  let
bulwahn@36046
   606
    val T = mk_random_dseqT HOLogic.unitT
bulwahn@36046
   607
  in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
bulwahn@36046
   608
bulwahn@36046
   609
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
bulwahn@36046
   610
  (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
bulwahn@36046
   611
bulwahn@36046
   612
val compfuns = Predicate_Compile_Aux.CompilationFuns
bulwahn@45461
   613
    {mk_monadT = mk_random_dseqT, dest_monadT = dest_random_dseqT,
bulwahn@45461
   614
    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
bulwahn@36049
   615
    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
bulwahn@36046
   616
bulwahn@36046
   617
end;
bulwahn@36046
   618