15347
|
1 |
(* Author: Jia Meng, Cambridge University Computer Laboratory
|
|
2 |
ID: $Id$
|
|
3 |
Copyright 2004 University of Cambridge
|
|
4 |
|
16803
|
5 |
Generation of unique Skolem functions (with types) as term.
|
15347
|
6 |
*)
|
|
7 |
|
|
8 |
signature RES_SKOLEM_FUNCTION =
|
|
9 |
sig
|
16803
|
10 |
val gen_skolem: term list -> typ -> term
|
15347
|
11 |
end;
|
|
12 |
|
|
13 |
structure ResSkolemFunction: RES_SKOLEM_FUNCTION =
|
|
14 |
struct
|
|
15 |
|
|
16 |
val skolem_prefix = "sk_";
|
|
17 |
val skolem_id = ref 0;
|
|
18 |
|
16803
|
19 |
fun gen_skolem_name () =
|
|
20 |
let val sk_fun = skolem_prefix ^ string_of_int (! skolem_id);
|
|
21 |
in inc skolem_id; sk_fun end;
|
15347
|
22 |
|
16803
|
23 |
fun gen_skolem univ_vars tp =
|
|
24 |
let
|
|
25 |
val skolem_type = map Term.fastype_of univ_vars ---> tp
|
|
26 |
val skolem_term = Const (gen_skolem_name (), skolem_type)
|
|
27 |
in Term.list_comb (skolem_term, univ_vars) end;
|
15347
|
28 |
|
16803
|
29 |
end;
|