14 val satisfies: theory -> term -> string list -> bool; |
14 val satisfies: theory -> term -> string list -> bool; |
15 val codegen_command: theory -> string -> unit; |
15 val codegen_command: theory -> string -> unit; |
16 |
16 |
17 type appgen; |
17 type appgen; |
18 val add_appconst: string * appgen -> theory -> theory; |
18 val add_appconst: string * appgen -> theory -> theory; |
19 val appgen_numeral: (term -> IntInf.int option) -> appgen; |
|
20 val appgen_char: (term -> int option) -> appgen; |
|
21 val appgen_case: (theory -> term |
19 val appgen_case: (theory -> term |
22 -> ((string * typ) list * ((term * typ) * (term * term) list)) option) |
20 -> ((string * typ) list * ((term * typ) * (term * term) list)) option) |
23 -> appgen; |
21 -> appgen; |
24 val appgen_let: appgen; |
22 val appgen_let: appgen; |
25 |
23 |
430 |
428 |
431 |
429 |
432 (* parametrized application generators, for instantiation in object logic *) |
430 (* parametrized application generators, for instantiation in object logic *) |
433 (* (axiomatic extensions of extraction kernel *) |
431 (* (axiomatic extensions of extraction kernel *) |
434 |
432 |
435 fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns = |
|
436 case int_of_numeral (list_comb (Const c, ts)) |
|
437 of SOME i => |
|
438 trns |
|
439 |> pair (CodegenThingol.INum i) |
|
440 | NONE => |
|
441 trns |
|
442 |> appgen_default thy algbr funcgr strct app; |
|
443 |
|
444 fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns = |
|
445 case (char_to_index o list_comb o apfst Const) app |
|
446 of SOME i => |
|
447 trns |
|
448 |> exprgen_type thy algbr funcgr strct ty |
|
449 |>> (fn _ => IChar (chr i)) |
|
450 | NONE => |
|
451 trns |
|
452 |> appgen_default thy algbr funcgr strct app; |
|
453 |
|
454 val debug_term = ref (Bound 0); |
|
455 |
|
456 fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns = |
433 fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns = |
457 let |
434 let |
458 val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts)); |
435 val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts)); |
459 fun clausegen (dt, bt) trns = |
436 fun clausegen (dt, bt) trns = |
460 trns |
437 trns |