4 Basic functions for nominal. |
4 Basic functions for nominal. |
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
|
9 val dest_listT: typ -> typ |
|
10 |
9 val mk_minus: term -> term |
11 val mk_minus: term -> term |
10 val mk_plus: term -> term -> term |
12 val mk_plus: term -> term -> term |
11 |
13 |
12 val perm_ty: typ -> typ |
14 val perm_ty: typ -> typ |
13 val mk_perm_ty: typ -> term -> term -> term |
15 val mk_perm_ty: typ -> term -> term -> term |
23 val mk_supp_ty: typ -> term -> term |
25 val mk_supp_ty: typ -> term -> term |
24 val mk_supp: term -> term |
26 val mk_supp: term -> term |
25 |
27 |
26 val mk_equiv: thm -> thm |
28 val mk_equiv: thm -> thm |
27 val safe_mk_equiv: thm -> thm |
29 val safe_mk_equiv: thm -> thm |
|
30 |
|
31 (* datatype operations *) |
|
32 val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ |
|
33 val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> |
|
34 (term * typ * typ list) list list |
|
35 val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> |
|
36 (term * typ * typ list) list |
|
37 val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list |
|
38 |
28 end |
39 end |
29 |
40 |
30 |
41 |
31 structure Nominal_Library: NOMINAL_LIBRARY = |
42 structure Nominal_Library: NOMINAL_LIBRARY = |
32 struct |
43 struct |
|
44 |
|
45 (* this function should be in hologic.ML *) |
|
46 fun dest_listT (Type (@{type_name list}, [T])) = T |
|
47 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
33 |
48 |
34 fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
49 fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
35 |
50 |
36 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; |
51 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; |
37 |
52 |
57 |
72 |
58 fun mk_equiv r = r RS @{thm eq_reflection}; |
73 fun mk_equiv r = r RS @{thm eq_reflection}; |
59 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
74 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
60 |
75 |
61 |
76 |
|
77 (** datatypes **) |
|
78 |
|
79 |
|
80 (* returns the type of the nth datatype *) |
|
81 fun nth_dtyp descr sorts n = |
|
82 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); |
|
83 |
|
84 (* returns info about constructors in a datatype *) |
|
85 fun all_dtyp_constrs_info descr = |
|
86 map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr |
|
87 |
|
88 (* returns the constants of the constructors plus the |
|
89 corresponding type and types of arguments *) |
|
90 fun all_dtyp_constrs_types descr sorts = |
|
91 let |
|
92 fun aux ((ty_name, vs), (cname, args)) = |
|
93 let |
|
94 val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs |
|
95 val ty = Type (ty_name, vs_tys) |
|
96 val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args |
|
97 in |
|
98 (Const (cname, arg_tys ---> ty), ty, arg_tys) |
|
99 end |
|
100 in |
|
101 map (map aux) (all_dtyp_constrs_info descr) |
|
102 end |
|
103 |
|
104 fun nth_dtyp_constrs_types descr sorts n = |
|
105 nth (all_dtyp_constrs_types descr sorts) n |
|
106 |
|
107 |
|
108 (* generates for every datatype a name str ^ dt_name |
|
109 plus and index for multiple occurences of a string *) |
|
110 fun prefix_dt_names descr sorts str = |
|
111 let |
|
112 fun get_nth_name (i, _) = |
|
113 Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) |
|
114 in |
|
115 Datatype_Prop.indexify_names |
|
116 (map (prefix str o get_nth_name) descr) |
|
117 end |
|
118 |
|
119 |
62 end (* structure *) |
120 end (* structure *) |
63 |
121 |
64 open Nominal_Library; |
122 open Nominal_Library; |