1 (* Title: HOLCF/HOLCFLogic.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 |
|
5 Abstract syntax operations for HOLCF. |
|
6 *) |
|
7 |
|
8 infixr 6 ->>; |
|
9 |
|
10 signature HOLCFLOGIC = |
|
11 sig |
|
12 val mk_btyp: string -> typ * typ -> typ |
|
13 val mk_prodT: typ * typ -> typ |
|
14 val mk_not: term -> term |
|
15 |
|
16 val HOLCF_sg: Sign.sg |
|
17 val pcpoC: class |
|
18 val pcpoS: sort |
|
19 val mk_TFree: string -> typ |
|
20 val cfun_arrow: string |
|
21 val ->> : typ * typ -> typ |
|
22 val mk_ssumT : typ * typ -> typ |
|
23 val mk_sprodT: typ * typ -> typ |
|
24 val mk_uT: typ -> typ |
|
25 val trT: typ |
|
26 val oneT: typ |
|
27 |
|
28 end; |
|
29 |
|
30 |
|
31 structure HOLCFLogic: HOLCFLOGIC = |
|
32 struct |
|
33 |
|
34 local |
|
35 |
|
36 open HOLogic; |
|
37 |
|
38 in |
|
39 |
|
40 fun mk_btyp t (S,T) = Type (t,[S,T]); |
|
41 val mk_prodT = mk_btyp "*"; |
|
42 |
|
43 fun mk_not P = Const ("Not", boolT --> boolT) $ P; |
|
44 |
|
45 (* basics *) |
|
46 |
|
47 val HOLCF_sg = sign_of HOLCF.thy; |
|
48 val pcpoC = Sign.intern_class HOLCF_sg "pcpo"; |
|
49 val pcpoS = [pcpoC]; |
|
50 fun mk_TFree s = TFree ("'"^s, pcpoS); |
|
51 |
|
52 (*cfun, ssum, sprod, u, tr, one *) |
|
53 |
|
54 local val intern = Sign.intern_tycon HOLCF_sg; |
|
55 in |
|
56 val cfun_arrow = intern "->"; |
|
57 val op ->> = mk_btyp cfun_arrow; |
|
58 val mk_ssumT = mk_btyp (intern "++"); |
|
59 val mk_sprodT = mk_btyp (intern "**"); |
|
60 fun mk_uT T = Type (intern "u" ,[T]); |
|
61 val trT = Type (intern "tr" ,[ ]); |
|
62 val oneT = Type (intern "one",[ ]); |
|
63 end; |
|
64 |
|
65 end; (* local *) |
|
66 end; (* struct *) |
|