1 (* Author: Jia Meng, Cambridge University Computer Laboratory |
1 (* Author: Jia Meng, Cambridge University Computer Laboratory |
2 ID: $Id$ |
2 ID: $Id$ |
3 Copyright 2004 University of Cambridge |
3 Copyright 2004 University of Cambridge |
4 |
4 |
5 Generation of unique Skolem functions (with types) as Term.term. |
5 Generation of unique Skolem functions (with types) as term. |
6 *) |
6 *) |
7 |
7 |
8 signature RES_SKOLEM_FUNCTION = |
8 signature RES_SKOLEM_FUNCTION = |
9 sig |
9 sig |
10 |
10 val gen_skolem: term list -> typ -> term |
11 val gen_skolem: Term.term list -> Term.typ -> Term.term |
|
12 |
|
13 end; |
11 end; |
14 |
12 |
15 structure ResSkolemFunction: RES_SKOLEM_FUNCTION = |
13 structure ResSkolemFunction: RES_SKOLEM_FUNCTION = |
16 |
|
17 struct |
14 struct |
18 |
15 |
19 val skolem_prefix = "sk_"; |
16 val skolem_prefix = "sk_"; |
20 |
|
21 (* internal reference starting from 0. *) |
|
22 val skolem_id = ref 0; |
17 val skolem_id = ref 0; |
23 |
18 |
|
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; |
24 |
22 |
25 fun gen_skolem_name () = |
23 fun gen_skolem univ_vars tp = |
26 let val new_id = !skolem_id |
24 let |
27 val sk_fun = skolem_prefix ^ (string_of_int new_id) |
25 val skolem_type = map Term.fastype_of univ_vars ---> tp |
28 in |
26 val skolem_term = Const (gen_skolem_name (), skolem_type) |
29 (skolem_id := new_id + 1; sk_fun) (* increment id by 1. *) |
27 in Term.list_comb (skolem_term, univ_vars) end; |
30 end; |
|
31 |
|
32 fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp]) |
|
33 | sk_type_of_aux (Var(_,tp1)::vars) tp = |
|
34 let val tp' = sk_type_of_aux vars tp |
|
35 in |
|
36 Type("fun",[tp1,tp']) |
|
37 end; |
|
38 |
|
39 |
|
40 fun sk_type_of [] tp = tp |
|
41 | sk_type_of vars tp = sk_type_of_aux vars tp; |
|
42 |
|
43 |
|
44 |
|
45 fun gen_skolem univ_vars tp = |
|
46 let val new_sk_name = gen_skolem_name () |
|
47 val new_sk_type = sk_type_of univ_vars tp |
|
48 val skolem_term = Const(new_sk_name,new_sk_type) |
|
49 fun app [] sf = sf |
|
50 | app (var::vars) sf= app vars (sf $ var) |
|
51 in |
|
52 app univ_vars skolem_term |
|
53 end; |
|
54 |
|
55 |
28 |
56 end; |
29 end; |