1(* ========================================================================= *) 2(* BASIC FIRST-ORDER LOGIC MANIPULATIONS *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6structure mlibTerm :> mlibTerm = 7struct 8 9open mlibParser mlibUseful; 10 11infixr 8 ++ 12infixr 7 >> 13infixr 6 || 14 15(* ------------------------------------------------------------------------- *) 16(* Datatypes for storing first-order terms and formulas. *) 17(* ------------------------------------------------------------------------- *) 18 19datatype term = 20 Var of string 21| Fn of string * term list; 22 23datatype formula = 24 True 25| False 26| Atom of term 27| Not of formula 28| And of formula * formula 29| Or of formula * formula 30| Imp of formula * formula 31| Iff of formula * formula 32| Forall of string * formula 33| Exists of string * formula; 34 35(* ------------------------------------------------------------------------- *) 36(* Constructors and destructors. *) 37(* ------------------------------------------------------------------------- *) 38 39(* Variables *) 40 41fun dest_var (Var v) = v 42 | dest_var (Fn _) = raise Error "dest_var"; 43 44val is_var = can dest_var; 45 46(* Functions *) 47 48fun dest_fn (Fn f) = f 49 | dest_fn (Var _) = raise Error "dest_fn"; 50 51val is_fn = can dest_fn; 52 53val fn_name = fst o dest_fn; 54 55val fn_args = snd o dest_fn; 56 57val fn_arity = length o fn_args; 58 59fun fn_function tm = (fn_name tm, fn_arity tm); 60 61(* Constants *) 62 63fun mk_const c = (Fn (c, [])); 64 65fun dest_const (Fn (c, [])) = c 66 | dest_const _ = raise Error "dest_const"; 67 68val is_const = can dest_const; 69 70(* Binary functions *) 71 72fun mk_binop f (a, b) = Fn (f, [a, b]); 73 74fun dest_binop f (Fn (x, [a, b])) = 75 if x = f then (a, b) else raise Error "dest_binop: wrong binop" 76 | dest_binop _ _ = raise Error "dest_binop: not a binop"; 77 78fun is_binop f = can (dest_binop f); 79 80(* Atoms *) 81 82fun dest_atom (Atom a) = a 83 | dest_atom _ = raise Error "dest_atom"; 84 85val is_atom = can dest_atom; 86 87(* Negations *) 88 89fun dest_neg (Not p) = p 90 | dest_neg _ = raise Error "dest_neg"; 91 92val is_neg = can dest_neg; 93 94(* Conjunctions *) 95 96fun list_mk_conj l = (case rev l of [] => True | h :: t => foldl And h t); 97 98local 99 fun conj cs (And (a, b)) = conj (a :: cs) b 100 | conj cs fm = rev (fm :: cs); 101in 102 fun strip_conj True = [] 103 | strip_conj fm = conj [] fm; 104end; 105 106val flatten_conj = 107 let 108 fun flat acc [] = acc 109 | flat acc (And (p, q) :: fms) = flat acc (q :: p :: fms) 110 | flat acc (True :: fms) = flat acc fms 111 | flat acc (fm :: fms) = flat (fm :: acc) fms 112 in 113 fn fm => flat [] [fm] 114 end; 115 116(* Disjunctions *) 117 118fun list_mk_disj l = (case rev l of [] => False | h :: t => foldl Or h t); 119 120local 121 fun disj cs (Or (a, b)) = disj (a :: cs) b 122 | disj cs fm = rev (fm :: cs); 123in 124 fun strip_disj False = [] 125 | strip_disj fm = disj [] fm; 126end; 127 128val flatten_disj = 129 let 130 fun flat acc [] = acc 131 | flat acc (Or (p, q) :: fms) = flat acc (q :: p :: fms) 132 | flat acc (False :: fms) = flat acc fms 133 | flat acc (fm :: fms) = flat (fm :: acc) fms 134 in 135 fn fm => flat [] [fm] 136 end; 137 138(* Universal quantifiers *) 139 140fun list_mk_forall ([], body) = body 141 | list_mk_forall (v :: vs, body) = Forall (v, list_mk_forall (vs, body)); 142 143local 144 fun dest vs (Forall (v, b)) = dest (v :: vs) b 145 | dest vs tm = (rev vs, tm); 146in 147 val strip_forall = dest []; 148end; 149 150(* Existential quantifiers *) 151 152fun list_mk_exists ([], body) = body 153 | list_mk_exists (v :: vs, body) = Exists (v, list_mk_exists (vs, body)); 154 155local 156 fun dest vs (Exists (v, b)) = dest (v :: vs) b 157 | dest vs tm = (rev vs, tm); 158in 159 val strip_exists = dest []; 160end; 161 162(* ------------------------------------------------------------------------- *) 163(* A datatype to antiquote both terms and formulas. *) 164(* ------------------------------------------------------------------------- *) 165 166datatype thing = mlibTerm of term | Formula of formula; 167 168(* ------------------------------------------------------------------------- *) 169(* Built-in infix operators and reserved symbols. *) 170(* ------------------------------------------------------------------------- *) 171 172val infixes : infixities ref = ref 173 [(* ML style *) 174 {tok = " / ", prec = 7, left_assoc = true}, 175 {tok = " div ", prec = 7, left_assoc = true}, 176 {tok = " mod ", prec = 7, left_assoc = true}, 177 {tok = " * ", prec = 7, left_assoc = true}, 178 {tok = " + ", prec = 6, left_assoc = true}, 179 {tok = " - ", prec = 6, left_assoc = true}, 180 {tok = " ^ ", prec = 6, left_assoc = true}, 181 {tok = " @ ", prec = 5, left_assoc = false}, 182 {tok = " :: ", prec = 5, left_assoc = false}, 183 {tok = " = ", prec = 4, left_assoc = true}, (* may be interpreted *) 184 {tok = " == ", prec = 4, left_assoc = true}, (* won't be interpreted *) 185 {tok = " <> ", prec = 4, left_assoc = true}, 186 {tok = " <= ", prec = 4, left_assoc = true}, 187 {tok = " < ", prec = 4, left_assoc = true}, 188 {tok = " >= ", prec = 4, left_assoc = true}, 189 {tok = " > ", prec = 4, left_assoc = true}, 190 {tok = " o ", prec = 8, left_assoc = true}, (* ML prec = 3 *) 191 (* HOL style *) 192 {tok = " % ", prec = 9, left_assoc = true}, (* function application *) 193 {tok = " -> ", prec = 2, left_assoc = false}, (* HOL ty prec = 50 *) 194 {tok = " : ", prec = 1, left_assoc = false}, (* not in HOL grammars *) 195 {tok = ", ", prec = 0, left_assoc = false}, (* HOL tm prec = 50 *) 196 (* Convenient alternative symbols *) 197 {tok = " ** ", prec = 7, left_assoc = true}, 198 {tok = " ++ ", prec = 6, left_assoc = true}, 199 {tok = " -- ", prec = 6, left_assoc = true}]; 200 201val connectives = 202 [{tok = " /\\ ", prec = ~1, left_assoc = false}, 203 {tok = " \\/ ", prec = ~2, left_assoc = false}, 204 {tok = " ==> ", prec = ~3, left_assoc = false}, 205 {tok = " <=> ", prec = ~4, left_assoc = false}]; 206 207val reserved = ["!", "?", "(", ")", ".", "~"]; 208 209(* ------------------------------------------------------------------------- *) 210(* Deciding whether a string denotes a variable or constant. *) 211(* ------------------------------------------------------------------------- *) 212 213local 214 val initials = explode "_vwxyz"; 215in 216 val var_string = ref (C mem initials o Char.toLower o hd o explode); 217end; 218 219(* ------------------------------------------------------------------------- *) 220(* Pretty-printing. *) 221(* ------------------------------------------------------------------------- *) 222 223(* Purely functional pretty-printing *) 224 225val pp_vname = 226 pp_map (fn s => if !var_string s then s else "var->" ^ s ^ "<-var") pp_string; 227 228fun pp_term' ops = 229 let 230 val ops = ops @ connectives 231 val iprinter = pp_infixes ops 232 val itoks = optoks ops 233 fun specialf s = mem s itoks orelse !var_string s 234 val pp_fname = pp_map (fn s=>if specialf s then "("^s^")" else s) pp_string 235 fun idest (Fn (f, [a, b])) = SOME (f, a, b) | idest _ = NONE 236 fun is_op t = case idest t of SOME (f, _, _) => mem f itoks | NONE => false 237 fun is_q (Fn ("!", _)) = true | is_q (Fn ("?", _)) = true | is_q _ = false 238 fun negs (Fn ("~", [a])) = (curry op+ 1 ## I) (negs a) | negs tm = (0, tm) 239 fun binds s (tm as Fn (n, [Var v, b])) = 240 if s = n then (cons v ## I) (binds s b) else ([], tm) 241 | binds _ tm = ([], tm) 242 open PP 243 fun basic (Var v) = pp_vname v 244 | basic (Fn (f, a)) = 245 block INCONSISTENT 0 246 (pp_fname f :: 247 List.concat (map (fn x => [add_break (1,0), argument x]) a)) 248 and argument tm = 249 if is_var tm orelse is_const tm then basic tm else pp_btm tm 250 and quant (tm, r) = 251 let 252 fun pr (Fn (q, [Var v, tm])) = 253 let 254 val (vs, body) = binds q tm 255 in 256 [add_string q, pp_vname v] @ 257 List.concat (map (fn a => [add_break (1, 0), pp_vname a]) vs) @ 258 [add_string ".", add_break (1, 0)] @ 259 (if is_q body then pr body else [pp_tm (body, false)]) 260 end 261 | pr tm = raise Bug "pp_term: not a quantifier" 262 fun pp_q t = block INCONSISTENT 2 (pr t) 263 in 264 (if is_q tm then (if r then pp_bracket "(" ")" else I) pp_q 265 else basic) tm 266 end 267 and molecule (tm, r) = 268 let 269 val (n, x) = negs tm 270 in 271 block INCONSISTENT n [ 272 add_string (CharVector.tabulate(n, fn _ => #"~")), 273 if is_op x then pp_btm x else quant (x, r) 274 ] 275 end 276 and pp_btm tm = pp_bracket "(" ")" pp_tm (tm, false) 277 and pp_tm tmr = iprinter idest molecule tmr 278 in 279 pp_map (C pair false) pp_tm 280 end; 281 282local 283 fun demote True = Fn ("T", [] ) 284 | demote False = Fn ("F", [] ) 285 | demote (Not a) = Fn ("~", [demote a] ) 286 | demote (And (a, b)) = Fn ("/\\", [demote a, demote b]) 287 | demote (Or (a, b)) = Fn ("\\/", [demote a, demote b]) 288 | demote (Imp (a, b)) = Fn ("==>", [demote a, demote b]) 289 | demote (Iff (a, b)) = Fn ("<=>", [demote a, demote b]) 290 | demote (Forall (v, b)) = Fn ("!", [Var v, demote b]) 291 | demote (Exists (v, b)) = Fn ("?", [Var v, demote b]) 292 | demote (Atom t) = t; 293in 294 fun pp_formula' ops = pp_map demote (pp_term' ops); 295end; 296 297fun term_to_string' ops len tm = PP.pp_to_string len (pp_term' ops) tm; 298fun formula_to_string' ops len fm = PP.pp_to_string len (pp_formula' ops) fm; 299 300(* Pretty-printing things is needed for parsing thing quotations *) 301 302fun pp_thing ops (mlibTerm tm) = pp_term' ops tm 303 | pp_thing ops (Formula fm) = pp_formula' ops fm; 304 305fun pp_bracketed_thing ops th = pp_bracket "(" ")" (pp_thing ops) th 306 307(* Pretty-printing using !infixes and !LINE_LENGTH *) 308 309fun pp_term tm = pp_term' (!infixes) tm; 310fun pp_formula fm = pp_formula' (!infixes) fm; 311fun term_to_string tm = term_to_string' (!infixes) (!LINE_LENGTH) tm; 312fun formula_to_string fm = formula_to_string' (!infixes) (!LINE_LENGTH) fm; 313 314(* ------------------------------------------------------------------------- *) 315(* Parsing. *) 316(* ------------------------------------------------------------------------- *) 317 318(* Lexing *) 319 320val lexer = 321 (fn ((_, (toks, _)), _) => toks) o 322 (many (some space) ++ 323 (many 324 ((((atleastone (some alphanum) || 325 (some (fn c => symbol c andalso c <> #"~") ++ many (some symbol)) >> 326 op ::) >> implode 327 || some (fn c => c = #"~" orelse punct c) >> str) ++ 328 many (some space)) >> fst)) ++ 329 finished); 330 331val lex_str = lexer o mlibStream.from_list o explode; 332 333(* Purely functional parsing *) 334 335val vname_parser = 336 some (fn tok => not (mem tok reserved) andalso !var_string tok); 337 338fun term_parser ops = 339 let 340 val ops = ops @ connectives 341 val iparser = parse_infixes ops 342 val itoks = optoks ops 343 val avoid = itoks @ reserved 344 fun fname tok = not (mem tok avoid) andalso not (!var_string tok) 345 val fname_parser = some fname || (exact "("++any++exact ")") >> (fst o snd) 346 fun bind s (v,t) = Fn (s, [Var v, t]) 347 fun basic inp = 348 (vname_parser >> Var || 349 fname_parser >> (fn f => Fn (f, [])) || 350 (exact "(" ++ tm_parser ++ exact ")") >> (fn (_, (t, _)) => t) || 351 (exact "!" ++ atleastone vname_parser ++ exact "." ++ tm_parser) >> 352 (fn (_, (vs, (_, body))) => foldr (bind "!") body vs) || 353 (exact "?" ++ atleastone vname_parser ++ exact "." ++ tm_parser) >> 354 (fn (_, (vs, (_, body))) => foldr (bind "?") body vs)) inp 355 and molecule inp = 356 ((many (exact "~") ++ ((fname_parser ++ many basic) >> Fn || basic)) >> 357 (fn (l, t) => funpow (length l) (fn x => Fn ("~", [x])) t)) inp 358 and tm_parser inp = iparser (fn (f, a, b) => Fn (f, [a, b])) molecule inp 359 in 360 tm_parser 361 end; 362 363local 364 fun promote (Fn ("T", [] )) = True 365 | promote (Fn ("F", [] )) = False 366 | promote (Fn ("~", [a] )) = Not (promote a) 367 | promote (Fn ("/\\", [a, b] )) = And (promote a, promote b) 368 | promote (Fn ("\\/", [a, b] )) = Or (promote a, promote b) 369 | promote (Fn ("==>", [a, b] )) = Imp (promote a, promote b) 370 | promote (Fn ("<=>", [a, b] )) = Iff (promote a, promote b) 371 | promote (Fn ("!", [Var v, b])) = Forall (v, promote b) 372 | promote (Fn ("?", [Var v, b])) = Exists (v, promote b) 373 | promote tm = Atom tm; 374in 375 fun formula_parser ops = term_parser ops >> promote; 376end; 377 378fun string_to_term' ops = 379 fst o ((term_parser ops ++ finished) >> fst) o mlibStream.from_list o lex_str; 380 381fun string_to_formula' ops = 382 fst o ((formula_parser ops ++ finished) >> fst) o mlibStream.from_list o lex_str; 383 384fun parse_term' ops = 385 quotation_parser (string_to_term' ops) (pp_bracketed_thing ops); 386 387fun parse_formula' ops = 388 quotation_parser (string_to_formula' ops) (pp_bracketed_thing ops); 389 390(* Parsing using !infixes *) 391 392fun string_to_term s = string_to_term' (!infixes) s; 393fun string_to_formula s = string_to_formula' (!infixes) s; 394fun parse_term q = parse_term' (!infixes) q; 395fun parse_formula q = parse_formula' (!infixes) q; 396 397(* ------------------------------------------------------------------------- *) 398(* New variables. *) 399(* ------------------------------------------------------------------------- *) 400 401local 402 val prefix = "_"; 403 val num_var = Var o mk_prefix prefix o int_to_string; 404in 405 val new_var = num_var o new_int; 406 val new_vars = map num_var o new_ints; 407end; 408 409(* ------------------------------------------------------------------------- *) 410(* Sizes of terms and formulas. *) 411(* ------------------------------------------------------------------------- *) 412 413local 414 fun szt n [] = n 415 | szt n (Var _ :: tms) = szt (n + 1) tms 416 | szt n (Fn (_, args) :: tms) = szt (n + 1) (args @ tms); 417 418 fun sz n [] = n 419 | sz n (True :: fms) = sz (n + 1) fms 420 | sz n (False :: fms) = sz (n + 1) fms 421 | sz n (Atom t :: fms) = sz (szt (n + 1) [t]) fms 422 | sz n (Not p :: fms) = sz (n + 1) (p :: fms) 423 | sz n (And (p, q) :: fms) = sz (n + 1) (p :: q :: fms) 424 | sz n (Or (p, q) :: fms) = sz (n + 1) (p :: q :: fms) 425 | sz n (Imp (p, q) :: fms) = sz (n + 1) (p :: q :: fms) 426 | sz n (Iff (p, q) :: fms) = sz (n + 1) (p :: q :: fms) 427 | sz n (Forall (_, p) :: fms) = sz (n + 1) (p :: fms) 428 | sz n (Exists (_, p) :: fms) = sz (n + 1) (p :: fms); 429in 430 val term_size = szt 0 o sing; 431 val formula_size = sz 0 o sing; 432end; 433 434(* ------------------------------------------------------------------------- *) 435(* Total comparison functions for terms and formulas. *) 436(* ------------------------------------------------------------------------- *) 437 438local 439 fun lex EQUAL f x = f x | lex x _ _ = x; 440 441 fun cmt [] = EQUAL 442 | cmt ((Var _, Fn _) :: _) = LESS 443 | cmt ((Fn _, Var _) :: _) = GREATER 444 | cmt ((Var v, Var w) :: l) = lex (String.compare (v, w)) cmt l 445 | cmt ((Fn (f, a), Fn (g, b)) :: l) = 446 (case lex (String.compare (f, g)) (Int.compare o Df length) (a, b) of EQUAL 447 => cmt (zip a b @ l) 448 | x => x); 449 450 fun cm [] = EQUAL 451 | cm ((True, True ) :: l) = cm l 452 | cm ((True, _ ) :: _) = LESS 453 | cm ((_, True ) :: _) = GREATER 454 | cm ((False, False ) :: l) = cm l 455 | cm ((False, _ ) :: _) = LESS 456 | cm ((_, False ) :: _) = GREATER 457 | cm ((Atom t, Atom u ) :: l) = lex (cmt [(t, u)]) cm l 458 | cm ((Atom _, _ ) :: _) = LESS 459 | cm ((_, Atom _ ) :: _) = GREATER 460 | cm ((Not p, Not q ) :: l) = cm ((p, q) :: l) 461 | cm ((Not _ , _ ) :: _) = LESS 462 | cm ((_, Not _ ) :: _) = GREATER 463 | cm ((And (p1, q1), And (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l) 464 | cm ((And _, _ ) :: _) = LESS 465 | cm ((_, And _ ) :: _) = GREATER 466 | cm ((Or (p1, q1), Or (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l) 467 | cm ((Or _, _ ) :: _) = LESS 468 | cm ((_, Or _ ) :: _) = GREATER 469 | cm ((Imp (p1, q1), Imp (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l) 470 | cm ((Imp _, _ ) :: _) = LESS 471 | cm ((_, Imp _ ) :: _) = GREATER 472 | cm ((Iff (p1, q1), Iff (p2, q2) ) :: l) = cm ((p1, p2) :: (q1, q2) :: l) 473 | cm ((Iff _, _ ) :: _) = LESS 474 | cm ((_, Iff _ ) :: _) = GREATER 475 | cm ((Forall (v, p), Forall (w, q)) :: l) = 476 lex (String.compare (v, w)) (cm o cons (p, q)) l 477 | cm ((Forall _, Exists _ ) :: _) = LESS 478 | cm ((Exists _, Forall _ ) :: _) = GREATER 479 | cm ((Exists (v, p), Exists (w, q)) :: l) = 480 lex (String.compare (v, w)) (cm o cons (p, q)) l; 481in 482 val term_compare = cmt o sing; 483 val formula_compare = cm o sing; 484end; 485 486(* ------------------------------------------------------------------------- *) 487(* Basic operations on literals. *) 488(* ------------------------------------------------------------------------- *) 489 490fun mk_literal (true, a) = a 491 | mk_literal (false, a) = Not a; 492 493fun dest_literal (a as Atom _) = (true, a) 494 | dest_literal (Not (a as Atom _)) = (false, a) 495 | dest_literal _ = raise Error "dest_literal"; 496 497val is_literal = can dest_literal; 498 499val literal_atom = snd o dest_literal; 500 501(* ------------------------------------------------------------------------- *) 502(* Dealing with formula negations. *) 503(* ------------------------------------------------------------------------- *) 504 505fun negative (Not p) = true 506 | negative _ = false; 507 508val positive = non negative; 509 510fun negate (Not p) = p 511 | negate p = Not p; 512 513(* ------------------------------------------------------------------------- *) 514(* Functions and relations in a formula. *) 515(* ------------------------------------------------------------------------- *) 516 517local 518 fun fnc fs [] = fs 519 | fnc fs (Var _ :: tms) = fnc fs tms 520 | fnc fs (Fn (n, a) :: tms) = fnc (insert (n, length a) fs) (a @ tms); 521 522 fun func fs [] = fs 523 | func fs (True :: fms) = func fs fms 524 | func fs (False :: fms) = func fs fms 525 | func fs (Atom (Var _) :: fms) = func fs fms 526 | func fs (Atom (Fn (_, tms)) :: fms) = func (fnc fs tms) fms 527 | func fs (Not p :: fms) = func fs (p :: fms) 528 | func fs (And (p, q) :: fms) = func fs (p :: q :: fms) 529 | func fs (Or (p, q) :: fms) = func fs (p :: q :: fms) 530 | func fs (Imp (p, q) :: fms) = func fs (p :: q :: fms) 531 | func fs (Iff (p, q) :: fms) = func fs (p :: q :: fms) 532 | func fs (Forall (_, p) :: fms) = func fs (p :: fms) 533 | func fs (Exists (_, p) :: fms) = func fs (p :: fms); 534in 535 val functions = func [] o sing; 536end; 537 538val function_names = map fst o functions; 539 540local 541 fun rel rs [] = rs 542 | rel rs (True :: fms) = rel rs fms 543 | rel rs (False :: fms) = rel rs fms 544 | rel rs (Atom (Var _) :: fms) = rel rs fms 545 | rel rs (Atom (f as Fn _) :: fms) = rel (insert (fn_function f) rs) fms 546 | rel rs (Not p :: fms) = rel rs (p :: fms) 547 | rel rs (And (p, q) :: fms) = rel rs (p :: q :: fms) 548 | rel rs (Or (p, q) :: fms) = rel rs (p :: q :: fms) 549 | rel rs (Imp (p, q) :: fms) = rel rs (p :: q :: fms) 550 | rel rs (Iff (p, q) :: fms) = rel rs (p :: q :: fms) 551 | rel rs (Forall (_, p) :: fms) = rel rs (p :: fms) 552 | rel rs (Exists (_, p) :: fms) = rel rs (p :: fms); 553in 554 val relations = rel [] o sing; 555end; 556 557val relation_names = map fst o relations; 558 559(* ------------------------------------------------------------------------- *) 560(* The equality relation has a special status. *) 561(* ------------------------------------------------------------------------- *) 562 563val eq_rel = ("=", 2); 564 565fun mk_eq (a, b) = Atom (Fn ("=", [a, b])); 566 567fun dest_eq (Atom (Fn ("=", [a, b]))) = (a, b) 568 | dest_eq _ = raise Error "dest_eq"; 569 570val is_eq = can dest_eq; 571 572val refl = mk_eq o D; 573 574val sym = mk_eq o swap o dest_eq; 575 576val lhs = fst o dest_eq; 577 578val rhs = snd o dest_eq; 579 580val eq_occurs = mem eq_rel o relations; 581 582(* ------------------------------------------------------------------------- *) 583(* Free variables in terms and formulas. *) 584(* ------------------------------------------------------------------------- *) 585 586local 587 fun fvt av = 588 let 589 val seen = 590 if null av then mem else (fn v => fn vs => mem v av orelse mem v vs) 591 fun f vs [] = vs 592 | f vs (Var v :: tms) = f (if seen v vs then vs else v :: vs) tms 593 | f vs (Fn (_, args) :: tms) = f vs (args @ tms) 594 in 595 f 596 end; 597 598 fun fv vs [] = vs 599 | fv vs ((_ , True ) :: fms) = fv vs fms 600 | fv vs ((_ , False ) :: fms) = fv vs fms 601 | fv vs ((av, Atom t ) :: fms) = fv (fvt av vs [t]) fms 602 | fv vs ((av, Not p ) :: fms) = fv vs ((av, p) :: fms) 603 | fv vs ((av, And (p, q) ) :: fms) = fv vs ((av, p) :: (av, q) :: fms) 604 | fv vs ((av, Or (p, q) ) :: fms) = fv vs ((av, p) :: (av, q) :: fms) 605 | fv vs ((av, Imp (p, q) ) :: fms) = fv vs ((av, p) :: (av, q) :: fms) 606 | fv vs ((av, Iff (p, q) ) :: fms) = fv vs ((av, p) :: (av, q) :: fms) 607 | fv vs ((av, Forall (x, p)) :: fms) = fv vs ((insert x av, p) :: fms) 608 | fv vs ((av, Exists (x, p)) :: fms) = fv vs ((insert x av, p) :: fms); 609in 610 fun FVT tm = rev (fvt [] [] [tm]); 611 fun FVTL l tms = fvt [] l tms; 612 fun FV fm = rev (fv [] [([], fm)]); 613 fun FVL l fms = fv l (map (pair []) fms); 614end; 615 616val specialize = snd o strip_forall; 617 618fun generalize fm = list_mk_forall (FV fm, fm); 619 620(* ------------------------------------------------------------------------- *) 621(* Subterms. *) 622(* ------------------------------------------------------------------------- *) 623 624fun subterm [] tm = tm 625 | subterm (_ :: _) (Var _) = raise Error "subterm: Var" 626 | subterm (h :: t) (Fn (_, args)) = 627 subterm t (List.nth (args, h)) 628 handle Subscript => raise Error "subterm: bad path"; 629 630fun literal_subterm p = subterm p o dest_atom o literal_atom; 631 632local 633 fun update _ _ [] = raise Error "rewrite: bad path" 634 | update f n (h :: t) = if n = 0 then f h :: t else h :: update f (n - 1) t; 635in 636 fun rewrite ([] |-> res) _ = res 637 | rewrite _ (Var _) = raise Error "rewrite: Var" 638 | rewrite ((h :: t) |-> res) (Fn (f, args)) = 639 Fn (f, update (rewrite (t |-> res)) h args); 640end; 641 642local 643 fun atom_rewrite r = Atom o rewrite r o dest_atom; 644in 645 fun literal_rewrite ([] |-> _) = raise Error "literal_rewrite: empty path" 646 | literal_rewrite r = mk_literal o (I ## atom_rewrite r) o dest_literal; 647end; 648 649local 650 fun f [] l = l | f ((p, t) :: w) l = g p t w ((rev p |-> t) :: l) 651 and g _ (Var _) w l = f w l 652 | g p (Fn (_, ts)) w l = 653 let val a = map (fn (x,y) => (x::p,y)) (enumerate 0 ts) in f (a @ w) l end; 654in 655 fun subterms p tm = f [(p, tm)] []; 656 fun literal_subterms lit = g [] (dest_atom (literal_atom lit)) [] []; 657end; 658 659end 660