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