|
1 signature USyntax_sig = |
|
2 sig |
|
3 structure Utils : Utils_sig |
|
4 |
|
5 type Type |
|
6 type Term |
|
7 type Preterm |
|
8 type 'a binding |
|
9 |
|
10 datatype lambda = VAR of {Name : string, Ty : Type} |
|
11 | CONST of {Name : string, Ty : Type} |
|
12 | COMB of {Rator: Preterm, Rand : Preterm} |
|
13 | LAMB of {Bvar : Preterm, Body : Preterm} |
|
14 |
|
15 val alpha : Type |
|
16 val bool : Type |
|
17 val mk_preterm : Term -> Preterm |
|
18 val drop_Trueprop : Preterm -> Preterm |
|
19 |
|
20 (* Types *) |
|
21 val type_vars : Type -> Type list |
|
22 val type_varsl : Type list -> Type list |
|
23 val mk_type : {Tyop: string, Args:Type list} -> Type |
|
24 val dest_type : Type -> {Tyop : string, Args : Type list} |
|
25 val mk_vartype : string -> Type |
|
26 val is_vartype : Type -> bool |
|
27 val --> : Type * Type -> Type |
|
28 val strip_type : Type -> Type list * Type |
|
29 val strip_prod_type : Type -> Type list |
|
30 val match_type: Type -> Type -> Type binding list |
|
31 |
|
32 (* Terms *) |
|
33 val free_vars : Preterm -> Preterm list |
|
34 val free_varsl : Preterm list -> Preterm list |
|
35 val free_vars_lr : Preterm -> Preterm list |
|
36 val all_vars : Preterm -> Preterm list |
|
37 val all_varsl : Preterm list -> Preterm list |
|
38 val variant : Preterm list -> Preterm -> Preterm |
|
39 val type_of : Preterm -> Type |
|
40 val type_vars_in_term : Preterm -> Type list |
|
41 val dest_term : Preterm -> lambda |
|
42 |
|
43 (* Prelogic *) |
|
44 val aconv : Preterm -> Preterm -> bool |
|
45 val subst : Preterm binding list -> Preterm -> Preterm |
|
46 val inst : Type binding list -> Preterm -> Preterm |
|
47 val beta_conv : Preterm -> Preterm |
|
48 |
|
49 (* Construction routines *) |
|
50 val mk_prop :Preterm -> Preterm |
|
51 val mk_var :{Name : string, Ty : Type} -> Preterm |
|
52 val mk_const :{Name : string, Ty : Type} -> Preterm |
|
53 val mk_comb :{Rator : Preterm, Rand : Preterm} -> Preterm |
|
54 val mk_abs :{Bvar : Preterm, Body : Preterm} -> Preterm |
|
55 |
|
56 val mk_eq :{lhs : Preterm, rhs : Preterm} -> Preterm |
|
57 val mk_imp :{ant : Preterm, conseq : Preterm} -> Preterm |
|
58 val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm |
|
59 val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm |
|
60 val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm |
|
61 val mk_conj :{conj1 : Preterm, conj2 : Preterm} -> Preterm |
|
62 val mk_disj :{disj1 : Preterm, disj2 : Preterm} -> Preterm |
|
63 val mk_pabs :{varstruct : Preterm, body : Preterm} -> Preterm |
|
64 |
|
65 (* Destruction routines *) |
|
66 val dest_var : Preterm -> {Name : string, Ty : Type} |
|
67 val dest_const: Preterm -> {Name : string, Ty : Type} |
|
68 val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm} |
|
69 val dest_abs : Preterm -> {Bvar : Preterm, Body : Preterm} |
|
70 val dest_eq : Preterm -> {lhs : Preterm, rhs : Preterm} |
|
71 val dest_imp : Preterm -> {ant : Preterm, conseq : Preterm} |
|
72 val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm} |
|
73 val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm} |
|
74 val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm} |
|
75 val dest_neg : Preterm -> Preterm |
|
76 val dest_conj : Preterm -> {conj1 : Preterm, conj2 : Preterm} |
|
77 val dest_disj : Preterm -> {disj1 : Preterm, disj2 : Preterm} |
|
78 val dest_pair : Preterm -> {fst : Preterm, snd : Preterm} |
|
79 val dest_pabs : Preterm -> {varstruct : Preterm, body : Preterm} |
|
80 |
|
81 val lhs : Preterm -> Preterm |
|
82 val rhs : Preterm -> Preterm |
|
83 val rator : Preterm -> Preterm |
|
84 val rand : Preterm -> Preterm |
|
85 val bvar : Preterm -> Preterm |
|
86 val body : Preterm -> Preterm |
|
87 |
|
88 |
|
89 (* Query routines *) |
|
90 val is_var : Preterm -> bool |
|
91 val is_const: Preterm -> bool |
|
92 val is_comb : Preterm -> bool |
|
93 val is_abs : Preterm -> bool |
|
94 val is_eq : Preterm -> bool |
|
95 val is_imp : Preterm -> bool |
|
96 val is_forall : Preterm -> bool |
|
97 val is_exists : Preterm -> bool |
|
98 val is_neg : Preterm -> bool |
|
99 val is_conj : Preterm -> bool |
|
100 val is_disj : Preterm -> bool |
|
101 val is_pair : Preterm -> bool |
|
102 val is_pabs : Preterm -> bool |
|
103 |
|
104 (* Construction of a Preterm from a list of Preterms *) |
|
105 val list_mk_comb : (Preterm * Preterm list) -> Preterm |
|
106 val list_mk_abs : (Preterm list * Preterm) -> Preterm |
|
107 val list_mk_imp : (Preterm list * Preterm) -> Preterm |
|
108 val list_mk_forall : (Preterm list * Preterm) -> Preterm |
|
109 val list_mk_exists : (Preterm list * Preterm) -> Preterm |
|
110 val list_mk_conj : Preterm list -> Preterm |
|
111 val list_mk_disj : Preterm list -> Preterm |
|
112 |
|
113 (* Destructing a Preterm to a list of Preterms *) |
|
114 val strip_comb : Preterm -> (Preterm * Preterm list) |
|
115 val strip_abs : Preterm -> (Preterm list * Preterm) |
|
116 val strip_imp : Preterm -> (Preterm list * Preterm) |
|
117 val strip_forall : Preterm -> (Preterm list * Preterm) |
|
118 val strip_exists : Preterm -> (Preterm list * Preterm) |
|
119 val strip_conj : Preterm -> Preterm list |
|
120 val strip_disj : Preterm -> Preterm list |
|
121 val strip_pair : Preterm -> Preterm list |
|
122 |
|
123 (* Miscellaneous *) |
|
124 val mk_vstruct : Type -> Preterm list -> Preterm |
|
125 val gen_all : Preterm -> Preterm |
|
126 val find_term : (Preterm -> bool) -> Preterm -> Preterm |
|
127 val find_terms : (Preterm -> bool) -> Preterm -> Preterm list |
|
128 val dest_relation : Preterm -> Preterm * Preterm * Preterm |
|
129 val is_WFR : Preterm -> bool |
|
130 val ARB : Type -> Preterm |
|
131 |
|
132 (* Prettyprinting *) |
|
133 val Term_to_string : Term -> string |
|
134 end; |