|
82379
|
1 |
(* Author: Pascal Stoop, ETH Zurich
|
|
|
2 |
Author: Andreas Lochbihler, Digital Asset *)
|
|
|
3 |
|
|
|
4 |
structure Termify_Lazy =
|
|
|
5 |
struct
|
|
|
6 |
|
|
|
7 |
fun termify_lazy
|
|
|
8 |
(_: string -> typ -> term) (_: term -> term -> term) (_: string -> typ -> term -> term)
|
|
|
9 |
(_: typ) (_: typ -> typ -> typ) (_: typ -> typ)
|
|
|
10 |
(term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) =
|
|
|
11 |
Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $
|
|
|
12 |
(case Lazy.peek x of
|
|
|
13 |
SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x)
|
|
|
14 |
| _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T));
|
|
|
15 |
|
|
|
16 |
end
|