|
82379
|
1 |
(* Author: Pascal Stoop, ETH Zurich
|
|
|
2 |
Author: Andreas Lochbihler, Digital Asset *)
|
|
|
3 |
|
|
|
4 |
module Termify_Lazy : sig
|
|
|
5 |
val termify_lazy :
|
|
|
6 |
(string -> 'typerep -> 'term) ->
|
|
|
7 |
('term -> 'term -> 'term) ->
|
|
|
8 |
(string -> 'typerep -> 'term -> 'term) ->
|
|
|
9 |
'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
|
|
|
10 |
('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term
|
|
|
11 |
end = struct
|
|
|
12 |
|
|
|
13 |
let termify_lazy const app abs unitT funT lazyT term_of ty x _ =
|
|
|
14 |
app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty)))
|
|
|
15 |
(if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x))
|
|
|
16 |
else const "Pure.dummy_pattern" (funT unitT ty));;
|
|
|
17 |
|
|
|
18 |
end;;
|