1(*  Title:      Tools/Argo/argo_expr.ML
2    Author:     Sascha Boehme
3
4The input language of the Argo solver.
5*)
6
7signature ARGO_EXPR =
8sig
9  (* data types *)
10  datatype typ = Bool | Real | Func of typ * typ | Type of string
11  datatype kind =
12    True | False | Not | And | Or | Imp | Iff | Ite | Eq | App | Con of string * typ |
13    Le | Lt | Num of Rat.rat | Neg | Add | Sub | Mul | Div | Min | Max | Abs
14  datatype expr = E of kind * expr list
15
16  (* indices, equalities, orders *)
17  val int_of_kind: kind -> int
18  val con_ord: (string * typ) ord
19  val eq_kind: kind * kind -> bool
20  val kind_ord: kind ord
21  val eq_expr: expr * expr -> bool
22  val expr_ord: expr ord
23  val dual_expr: expr -> expr -> bool
24
25  (* constructors *)
26  val kind_of_string: string -> kind
27  val true_expr: expr
28  val false_expr: expr
29  val mk_not: expr -> expr
30  val mk_and: expr list -> expr
31  val mk_and2: expr -> expr -> expr
32  val mk_or: expr list -> expr
33  val mk_or2: expr -> expr -> expr
34  val mk_imp: expr -> expr -> expr
35  val mk_iff: expr -> expr -> expr
36  val mk_ite: expr -> expr -> expr -> expr
37  val mk_eq: expr -> expr -> expr
38  val mk_app: expr -> expr -> expr
39  val mk_con: string * typ -> expr
40  val mk_le: expr -> expr -> expr
41  val mk_lt: expr -> expr -> expr
42  val mk_num: Rat.rat -> expr
43  val mk_neg: expr -> expr
44  val mk_add: expr list -> expr
45  val mk_add2: expr -> expr -> expr
46  val mk_sub: expr -> expr -> expr
47  val mk_mul: expr -> expr -> expr
48  val mk_div: expr -> expr -> expr
49  val mk_min: expr -> expr -> expr
50  val mk_max: expr -> expr -> expr
51  val mk_abs: expr -> expr
52
53  (* type checking *)
54  exception TYPE of expr
55  exception EXPR of expr
56  val type_of: expr -> typ (* raises EXPR *)
57  val check: expr -> bool (* raises TYPE and EXPR *)
58
59  (* testers *)
60  val is_nary: kind -> bool
61
62  (* string representations *)
63  val string_of_kind: kind -> string
64end
65
66structure Argo_Expr: ARGO_EXPR =
67struct
68
69(* data types *)
70
71datatype typ = Bool | Real | Func of typ * typ | Type of string
72
73datatype kind =
74  True | False | Not | And | Or | Imp | Iff | Ite | Eq | App | Con of string * typ |
75  Le | Lt | Num of Rat.rat | Neg | Add | Sub | Mul | Div | Min | Max | Abs
76
77datatype expr = E of kind * expr list
78
79
80(* indices, equalities, orders *)
81
82fun int_of_type Bool = 0
83  | int_of_type Real = 1
84  | int_of_type (Func _) = 2
85  | int_of_type (Type _) = 3
86
87fun int_of_kind True = 0
88  | int_of_kind False = 1
89  | int_of_kind Not = 2
90  | int_of_kind And = 3
91  | int_of_kind Or = 4
92  | int_of_kind Imp = 5
93  | int_of_kind Iff = 6
94  | int_of_kind Ite = 7
95  | int_of_kind Eq = 8
96  | int_of_kind App = 9
97  | int_of_kind (Con _) = 10
98  | int_of_kind Le = 11
99  | int_of_kind Lt = 12
100  | int_of_kind (Num _) = 13
101  | int_of_kind Neg = 14
102  | int_of_kind Add = 15
103  | int_of_kind Sub = 16
104  | int_of_kind Mul = 17
105  | int_of_kind Div = 18
106  | int_of_kind Min = 19
107  | int_of_kind Max = 20
108  | int_of_kind Abs = 21
109
110fun eq_type (Bool, Bool) = true
111  | eq_type (Real, Real) = true
112  | eq_type (Func tys1, Func tys2) = eq_pair eq_type eq_type (tys1, tys2)
113  | eq_type (Type n1, Type n2) = (n1 = n2)
114  | eq_type _ = false
115
116fun type_ord (Bool, Bool) = EQUAL
117  | type_ord (Real, Real) = EQUAL
118  | type_ord (Type n1, Type n2) = fast_string_ord (n1, n2)
119  | type_ord (Func tys1, Func tys2) = prod_ord type_ord type_ord (tys1, tys2)
120  | type_ord (ty1, ty2) = int_ord (int_of_type ty1, int_of_type ty2)
121
122fun eq_con cp = eq_pair (op =) eq_type cp
123fun con_ord cp = prod_ord fast_string_ord type_ord cp
124
125fun eq_kind (Con c1, Con c2) = eq_con (c1, c2)
126  | eq_kind (Num n1, Num n2) = n1 = n2
127  | eq_kind (k1, k2) = (k1 = k2)
128
129fun kind_ord (Con c1, Con c2) = con_ord (c1, c2)
130  | kind_ord (Num n1, Num n2) = Rat.ord (n1, n2)
131  | kind_ord (k1, k2) = int_ord (int_of_kind k1, int_of_kind k2)
132
133fun eq_expr (E e1, E e2) = eq_pair eq_kind (eq_list eq_expr) (e1, e2)
134fun expr_ord (E e1, E e2) = prod_ord kind_ord (list_ord expr_ord) (e1, e2)
135
136fun dual_expr (E (Not, [e1])) e2 = eq_expr (e1, e2)
137  | dual_expr e1 (E (Not, [e2])) = eq_expr (e1, e2)
138  | dual_expr _ _ = false
139
140
141(* constructors *)
142
143val string_kinds = [
144  ("true", True),("false", False), ("not", Not), ("and", And), ("or", Or), ("imp", Imp),
145  ("iff", Iff), ("ite", Ite), ("eq", Eq), ("app", App), ("le", Le), ("lt", Lt), ("neg", Neg),
146  ("add", Add), ("sub", Sub), ("mul", Mul), ("div", Div), ("min", Min), ("max", Max), ("abs", Abs)]
147
148val kind_of_string = the o Symtab.lookup (Symtab.make string_kinds)
149
150val true_expr = E (True, [])
151val false_expr = E (False, [])
152fun mk_not e = E (Not, [e])
153fun mk_and es = E (And, es)
154fun mk_and2 e1 e2 = mk_and [e1, e2]
155fun mk_or es = E (Or, es)
156fun mk_or2 e1 e2 = mk_or [e1, e2]
157fun mk_imp e1 e2 = E (Imp, [e1, e2])
158fun mk_iff e1 e2 = E (Iff, [e1, e2])
159fun mk_ite e1 e2 e3 = E (Ite, [e1, e2, e3])
160fun mk_eq e1 e2 = E (Eq, [e1, e2])
161fun mk_app e1 e2 = E (App, [e1, e2])
162fun mk_con n = E (Con n, [])
163fun mk_le e1 e2 = E (Le, [e1, e2])
164fun mk_lt e1 e2 = E (Lt, [e1, e2])
165fun mk_num r = E (Num r, [])
166fun mk_neg e = E (Neg, [e])
167fun mk_add es = E (Add, es)
168fun mk_add2 e1 e2 = mk_add [e1, e2]
169fun mk_sub e1 e2 = E (Sub, [e1, e2])
170fun mk_mul e1 e2 = E (Mul, [e1, e2])
171fun mk_div e1 e2 = E (Div, [e1, e2])
172fun mk_min e1 e2 = E (Min, [e1, e2])
173fun mk_max e1 e2 = E (Max, [e1, e2])
174fun mk_abs e = E (Abs, [e])
175
176
177(* type checking *)
178
179exception TYPE of expr
180exception EXPR of expr
181
182fun dest_func_type _ (Func tys) = tys
183  | dest_func_type e _ = raise TYPE e
184
185fun type_of (E (True, _)) = Bool
186  | type_of (E (False, _)) = Bool
187  | type_of (E (Not, _)) = Bool
188  | type_of (E (And, _)) = Bool
189  | type_of (E (Or, _)) = Bool
190  | type_of (E (Imp, _)) = Bool
191  | type_of (E (Iff, _)) = Bool
192  | type_of (E (Ite, [_, e, _])) = type_of e
193  | type_of (E (Eq, _)) = Bool
194  | type_of (E (App, [e, _])) = snd (dest_func_type e (type_of e))
195  | type_of (E (Con (_, ty), _)) = ty
196  | type_of (E (Le, _)) = Bool
197  | type_of (E (Lt, _)) = Bool
198  | type_of (E (Num _, _)) = Real
199  | type_of (E (Neg, _)) = Real
200  | type_of (E (Add, _)) = Real
201  | type_of (E (Sub, _)) = Real
202  | type_of (E (Mul, _)) = Real
203  | type_of (E (Div, _)) = Real
204  | type_of (E (Min, _)) = Real
205  | type_of (E (Max, _)) = Real
206  | type_of (E (Abs, _)) = Real
207  | type_of e = raise EXPR e
208
209fun all_type ty (E (_, es)) = forall (curry eq_type ty o type_of) es
210val all_bool = all_type Bool
211val all_real = all_type Real
212
213(*
214  Types as well as proper arities are checked.
215  Exception TYPE is raised for invalid types.
216  Exception EXPR is raised for invalid expressions and invalid arities.
217*)
218
219fun check (e as E (_, es)) = (forall check es andalso raw_check e) orelse raise TYPE e
220
221and raw_check (E (True, [])) = true
222  | raw_check (E (False, [])) = true
223  | raw_check (e as E (Not, [_])) = all_bool e
224  | raw_check (e as E (And, _ :: _)) = all_bool e
225  | raw_check (e as E (Or, _ :: _)) = all_bool e
226  | raw_check (e as E (Imp, [_, _])) = all_bool e
227  | raw_check (e as E (Iff, [_, _])) = all_bool e
228  | raw_check (E (Ite, [e1, e2, e3])) =
229      let val ty1 = type_of e1 and ty2 = type_of e2 and ty3 = type_of e3
230      in eq_type (ty1, Bool) andalso eq_type (ty2, ty3) end
231  | raw_check (E (Eq, [e1, e2])) =
232      let val ty1 = type_of e1 and ty2 = type_of e2
233      in eq_type (ty1, ty2) andalso not (eq_type (ty1, Bool)) end
234  | raw_check (E (App, [e1, e2])) =
235      eq_type (fst (dest_func_type e1 (type_of e1)), type_of e2)
236  | raw_check (E (Con _, [])) = true
237  | raw_check (E (Num _, [])) = true
238  | raw_check (e as E (Le, [_, _])) = all_real e
239  | raw_check (e as E (Lt, [_, _])) = all_real e
240  | raw_check (e as E (Neg, [_])) = all_real e
241  | raw_check (e as E (Add, _)) = all_real e
242  | raw_check (e as E (Sub, [_, _])) = all_real e
243  | raw_check (e as E (Mul, [_, _])) = all_real e
244  | raw_check (e as E (Div, [_, _])) = all_real e
245  | raw_check (e as E (Min, [_, _])) = all_real e
246  | raw_check (e as E (Max, [_, _])) = all_real e
247  | raw_check (e as E (Abs, [_])) = all_real e
248  | raw_check e = raise EXPR e
249
250
251(* testers *)
252
253fun is_nary k = member (op =) [And, Or, Add] k
254
255
256(* string representations *)
257
258val kind_strings = map swap string_kinds
259
260fun string_of_kind (Con (n, _)) = n
261  | string_of_kind (Num n) = Rat.string_of_rat n
262  | string_of_kind k = the (AList.lookup (op =) kind_strings k)
263
264end
265
266structure Argo_Exprtab = Table(type key = Argo_Expr.expr val ord = Argo_Expr.expr_ord)
267