1(* ========================================================================= *) 2(* THE MESON PROOF PROCEDURE *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load 8 ["mlibUseful", "mlibStream", "Mosml", "mlibTerm", "mlibThm", "mlibCanon", "mlibMatch", 9 "mlibSolver", "mlibMeter", "mlibUnits"]; 10*) 11 12(* 13*) 14structure mlibMeson :> mlibMeson = 15struct 16 17open mlibUseful mlibTerm mlibMatch mlibThm mlibCanon mlibMeter mlibSolver; 18 19structure S = mlibStream; local open mlibStream in end; 20structure N = mlibLiteralnet; local open mlibLiteralnet in end; 21structure U = mlibUnits; local open mlibUnits in end; 22 23val |<>| = mlibSubst.|<>|; 24val formula_subst = mlibSubst.formula_subst; 25 26(* ------------------------------------------------------------------------- *) 27(* Chatting. *) 28(* ------------------------------------------------------------------------- *) 29 30val module = "mlibMeson"; 31val () = add_trace {module = module, alignment = I} 32fun chatting l = tracing {module = module, level = l}; 33fun chat s = (trace s; true) 34 35(* ------------------------------------------------------------------------- *) 36(* Tuning parameters. *) 37(* ------------------------------------------------------------------------- *) 38 39type parameters = 40 {ancestor_pruning : bool, 41 ancestor_cutting : bool, 42 state_simplify : bool, 43 cache_cutting : bool, 44 divide_conquer : bool, 45 unit_lemmaizing : bool, 46 sort_literals : int, 47 sort_rules : bool}; 48 49val defaults = 50 {ancestor_pruning = true, 51 ancestor_cutting = true, 52 state_simplify = true, 53 cache_cutting = false, 54 divide_conquer = false, 55 unit_lemmaizing = true, 56 sort_literals = 1, 57 sort_rules = true}; 58 59type 'a Parmupdate = ('a -> 'a) -> parameters -> parameters 60 61fun update_ancestor_pruning f (parm : parameters) : parameters = 62 let 63 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 64 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 65 sort_literals = l, sort_rules = r} = parm 66 in 67 {ancestor_pruning = f a, ancestor_cutting = b, state_simplify = s, 68 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 69 sort_literals = l, sort_rules = r} 70 end; 71 72fun update_ancestor_cutting f (parm : parameters) : parameters = 73 let 74 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 75 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 76 sort_literals = l, sort_rules = r} = parm 77 in 78 {ancestor_pruning = a, ancestor_cutting = f b, state_simplify = s, 79 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 80 sort_literals = l, sort_rules = r} 81 end; 82 83fun update_state_simplify f (parm : parameters) : parameters = 84 let 85 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 86 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 87 sort_literals = l, sort_rules = r} = parm 88 in 89 {ancestor_pruning = a, ancestor_cutting = b, state_simplify = f s, 90 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 91 sort_literals = l, sort_rules = r} 92 end; 93 94fun update_cache_cutting f (parm : parameters) : parameters = 95 let 96 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 97 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 98 sort_literals = l, sort_rules = r} = parm 99 in 100 {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 101 cache_cutting = f c, divide_conquer = d, unit_lemmaizing = u, 102 sort_literals = l, sort_rules = r} 103 end; 104 105fun update_divide_conquer f (parm : parameters) : parameters = 106 let 107 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 108 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 109 sort_literals = l, sort_rules = r} = parm 110 in 111 {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 112 cache_cutting = c, divide_conquer = f d, unit_lemmaizing = u, 113 sort_literals = l, sort_rules = r} 114 end; 115 116fun update_unit_lemmaizing f (parm : parameters) : parameters = 117 let 118 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 119 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 120 sort_literals = l, sort_rules = r} = parm 121 in 122 {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 123 cache_cutting = c, divide_conquer = d, unit_lemmaizing = f u, 124 sort_literals = l, sort_rules = r} 125 end; 126 127fun update_sort_literals f (parm : parameters) : parameters = 128 let 129 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 130 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 131 sort_literals = l, sort_rules = r} = parm 132 in 133 {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 134 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 135 sort_literals = f l, sort_rules = r} 136 end; 137 138fun update_sort_rules f (parm : parameters) : parameters = 139 let 140 val {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 141 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 142 sort_literals = l, sort_rules = r} = parm 143 in 144 {ancestor_pruning = a, ancestor_cutting = b, state_simplify = s, 145 cache_cutting = c, divide_conquer = d, unit_lemmaizing = u, 146 sort_literals = l, sort_rules = f r} 147 end; 148 149(* ------------------------------------------------------------------------- *) 150(* Helper functions. *) 151(* ------------------------------------------------------------------------- *) 152 153fun halves n = let val n1 = n div 2 in (n1, n - n1) end; 154 155fun divisible [] = false 156 | divisible [_] = false 157 | divisible _ = true; 158 159local 160 val prefix = "_m"; 161in 162 val mk_mvar = mk_prefix prefix o int_to_string; 163 fun mk_mvars n i = map (Var o mk_mvar) (interval n i); 164 val dest_mvar = string_to_int o dest_prefix prefix; 165end; 166 167local 168 fun sz n [] = n 169 | sz n (Fn (":", [tm, _]) :: tms) = sz n (tm :: tms) 170 | sz n (Var _ :: tms) = sz (n + 1) tms 171 | sz n (Fn (_,l) :: tms) = sz (n + 1) (l @ tms); 172in 173 fun literal_size False = 0 174 | literal_size lit = sz 0 [dest_atom (literal_atom lit)]; 175end; 176 177datatype 'a choice = CHOICE of unit -> 'a * 'a choice; 178 179fun dest_choice (CHOICE c) = c; 180 181val no_choice = (fn () => raise Error "no_choice: always fails"); 182 183fun binary_choice f g = 184 (fn () => 185 let val (a, c) = f () in (a, CHOICE (binary_choice (dest_choice c) g)) end 186 handle Error _ => g ()); 187 188fun first_choice [] = no_choice 189 | first_choice [f] = f 190 | first_choice (f :: fs) = binary_choice f (first_choice fs); 191 192fun choice_stream f = 193 let val (a, CHOICE c) = f () in S.CONS (a, fn () => choice_stream c) end 194 handle Error _ => S.NIL; 195 196fun swivel m n l = 197 let 198 val (l1, l') = divide l m 199 val (l2, l3) = divide l' n 200 in 201 l2 @ l1 @ l3 202 end; 203 204fun thm_proves th False = is_contradiction th 205 | thm_proves th goal = 206 case clause th of [lit] => lit = goal | [] => true | _ => false; 207 208fun filter_meter meter = 209 S.filter (fn a => Option.isSome a orelse not (check_meter (!meter))); 210 211(* ------------------------------------------------------------------------- *) 212(* mlibMeson rules. *) 213(* ------------------------------------------------------------------------- *) 214 215type rule = {asms : formula list, c : formula, thm : thm, asmn : int}; 216 217datatype rules = Rules of rule N.literalnet; 218 219fun dest_rules (Rules r) = r; 220val empty_rules = Rules (N.empty {fifo = true}); 221fun add_rule r (Rules n) = Rules (N.insert r n); 222val num_all_rules = N.size o dest_rules; 223val num_initial_rules = #f o N.size_profile o dest_rules; 224fun num_rules r = num_all_rules r - num_initial_rules r; 225fun rules_unify r = N.unify (dest_rules r); 226 227local fun dest ({asms, c, ...} : rule) = (asms,c); 228in val pp_rule = pp_map dest (pp_binop " ==>" (pp_list pp_formula) pp_formula); 229end; 230 231fun rule_to_string r = PP.pp_to_string (!LINE_LENGTH) pp_rule r; 232 233val pp_rules = 234 pp_map (map (fn _ |-> x => x) o N.to_maplets o dest_rules) 235 (pp_list pp_rule); 236 237(* ------------------------------------------------------------------------- *) 238(* Sorting literals within rules. *) 239(* ------------------------------------------------------------------------- *) 240 241val sort_lits = sort_map literal_size (rev_order Int.compare); 242 243(* ------------------------------------------------------------------------- *) 244(* Sorting rules. *) 245(* ------------------------------------------------------------------------- *) 246 247local 248 fun quality (_ |-> ({asmn, c, ...} : rule)) = (asmn, literal_size c); 249 val qualitywise = lex_order Int.compare (rev_order Int.compare); 250in 251 val sort_ruls = sort_map quality qualitywise; 252end; 253 254(* ------------------------------------------------------------------------- *) 255(* Compiling the rule set used by meson. *) 256(* ------------------------------------------------------------------------- *) 257 258fun mk_contrapositives chosen opt sos th = 259 let 260 val th = FRESH_VARS th 261 val lits = clause th 262 val lits' = map negate lits 263 fun g l = (List.filter (not o equal (negate l)) lits', l) 264 val base = map g (chosen lits) 265 val contrs = if sos then (lits', False) :: base else base 266 fun f (a,c) = c |-> {asms = opt a, c = c, thm = th, asmn = length a} 267 in 268 map f contrs 269 end; 270 271fun thms_to_rules parm chosen thms hyps = 272 let 273 val {sort_literals, sort_rules, ...} : parameters = parm 274 val opt = if 1 <= sort_literals then sort_lits else I 275 fun f sos (th,l) = mk_contrapositives chosen opt sos th @ l 276 val contrs = rev (foldl (f true) (foldl (f false) [] thms) hyps) 277 val contrs = if sort_rules then sort_ruls contrs else contrs 278 in 279 foldl (fn (h,t) => add_rule h t) empty_rules contrs 280 end; 281 282fun meson_rules parm = thms_to_rules parm I; 283 284local 285 fun only_one (l as [_]) = l | only_one _ = []; 286 val chosen = only_one o List.filter positive; 287in 288 fun prolog_rules parm = thms_to_rules parm chosen; 289end; 290 291(* ------------------------------------------------------------------------- *) 292(* Creating the delta goals. *) 293(* ------------------------------------------------------------------------- *) 294 295val thms_to_delta_goals = 296 List.concat o 297 map (fn (f,n) => [Atom (Fn (f,new_vars n)), Not (Atom (Fn (f,new_vars n)))]) o 298 foldl (uncurry union) [] o 299 map relations o 300 List.concat o 301 map clause; 302 303(* ------------------------------------------------------------------------- *) 304(* The state passed around by meson. *) 305(* ------------------------------------------------------------------------- *) 306 307type state = {env : subst, depth : int, proof : thm list, offset : int}; 308 309fun update_env f ({env, depth, proof, offset} : state) = 310 {env = f env, depth = depth, proof = proof, offset = offset}; 311 312fun update_depth f ({env, depth, proof, offset} : state) = 313 {env = env, depth = f depth, proof = proof, offset = offset}; 314 315fun update_proof f ({env, depth, proof, offset} : state) = 316 {env = env, depth = depth, proof = f proof, offset = offset}; 317 318fun update_offset f ({env, depth, proof, offset} : state) = 319 {env = env, depth = depth, proof = proof, offset = f offset}; 320 321(* ------------------------------------------------------------------------- *) 322(* Ancestor pruning. *) 323(* ------------------------------------------------------------------------- *) 324 325fun ancestor_prune false _ _ = K false 326 | ancestor_prune true env g = 327 let 328 val g' = formula_subst env g 329 fun check a' = a' = g' 330 in 331 List.exists (check o formula_subst env) 332 end; 333 334(* ------------------------------------------------------------------------- *) 335(* Ancestor cutting. *) 336(* ------------------------------------------------------------------------- *) 337 338fun ancestor_cut false _ _ = K false 339 | ancestor_cut true env g = 340 let 341 val g' = negate (formula_subst env g) 342 fun check a' = a' = g' 343 in 344 List.exists (check o formula_subst env) 345 end; 346 347(* ------------------------------------------------------------------------- *) 348(* Cache cutting. *) 349(* ------------------------------------------------------------------------- *) 350 351fun cache_cont c ({offset, ...} : state) = 352 let 353 fun f v = case total dest_mvar v of NONE => true | SOME n => n < offset 354 val listify = mlibSubst.foldr (fn m as v |-> _ => if f v then cons m else I) [] 355 val mem = ref [] 356 fun purify (s as {env, depth = n, ...} : state) = 357 let 358 val l = listify env 359 fun p (n', l') = n <= n' andalso l = l' 360 in 361 if List.exists p (!mem) then raise Error "cache_cut: repetition" 362 else ( 363 mem := (n, l) :: (!mem); (* OK *) 364 update_env (K (mlibSubst.from_maplets l)) s 365 ) 366 end 367 in 368 c o purify 369 end; 370 371fun cache_cut false = I 372 | cache_cut true = 373 fn f => fn a => fn g => fn c => fn s => f a g (cache_cont c s) s; 374 375(* ------------------------------------------------------------------------- *) 376(* Unit clause shortcut. *) 377(* ------------------------------------------------------------------------- *) 378 379fun grab_unit units (s as {proof = th :: _, ...} : state) = 380 let 381 val u = !units 382 val th = U.demod u th 383 val () = units := U.add th u (* OK *) 384 in 385 update_proof (cons th o tl) s 386 end 387 | grab_unit _ {proof = [], ...} = raise Bug "grab_unit: no thms"; 388 389fun use_unit units g c (s as {env, ...}) = 390 let 391 val prove = partial (Error "use_unit: NONE") (U.prove (!units)) 392 in 393 c (update_proof (cons (hd (prove [formula_subst env g]))) s) 394 end; 395 396fun unit_cut false _ = I 397 | unit_cut true units = 398 fn f => fn a => fn g => fn c => fn s => 399 use_unit units g c s handle Error _ => f a g (c o grab_unit units) s; 400 401(* ------------------------------------------------------------------------- *) 402(* The core of meson: ancestor unification or Prolog-style extension. *) 403(* ------------------------------------------------------------------------- *) 404 405local 406 (* Only check the meter every CHECK_PERIOD inferences to save time *) 407 val CHECK_PERIOD = 100; 408in 409 fun meter_expired m = 410 read_infs m mod CHECK_PERIOD = 0 andalso not (check_meter m); 411end; 412 413fun freshen_rule ({thm, asms, c, asmn} : rule) i = 414 let 415 val fvs = FVL [] (c :: asms) 416 val fvn = length fvs 417 val mvs = mk_mvars i fvn 418 val sub = mlibSubst.from_maplets (zipwith (curry op|->) fvs mvs) 419 in 420 ({thm = INST sub thm, asms = map (formula_subst sub) asms, 421 c = formula_subst sub c, asmn = asmn}, i + fvn) 422 end; 423 424fun reward r = update_depth (fn n => n + r); 425 426fun spend m f c (s as {depth = n, ...} : state) = 427 let 428 val low = n - m 429 val () = assert (0 <= low) (Error "meson: impossible divide and conquer") 430 fun check (s' as {depth = n', ...} : state) = 431 if n' <= low then s' else raise Error "meson: divide and conquer" 432 in 433 f (c o check) s 434 end; 435 436local 437 fun unify env ({thm,asms,c,...} : rule) g = 438 (thm, asms, unify_literals env c g); 439 440 fun match env ({thm,asms,c,...} : rule) g = 441 let val sub = match_literals c g 442 in (INST sub thm, map (formula_subst sub) asms, env) 443 end; 444in 445 fun next_state false env r g = unify env r g 446 | next_state true env r g = 447 match env r g handle Error _ => unify env r g; 448end; 449 450local 451 fun mp _ th [] p = FACTOR th :: p 452 | mp env th (g :: gs) (th1 :: p) = 453 mp env (RESOLVE (formula_subst env g) (INST env th1) th) gs p 454 | mp _ _ (_ :: _) [] = raise Bug "modus_ponens: fresh out of thms" 455in 456 fun modus_ponens th gs (state as {env, ...}) = 457 update_proof (mp env (INST env th) (rev gs)) state; 458end; 459 460fun swivelp m n = update_proof (swivel m n); 461 462fun meson_expand {parm : parameters, rules, cut, meter, saturated} = 463 let 464 val {ancestor_pruning, ancestor_cutting, state_simplify, 465 divide_conquer, sort_literals, ...} = parm 466 fun expand ancestors g cont (state as {env, ...}) = 467 (chatting 5 andalso 468 chat ("meson: "^formula_to_string (formula_subst env g)^".\n"); 469 if meter_expired (!meter) then 470 (NONE, CHOICE (fn () => expand ancestors g cont state)) 471 else if ancestor_prune ancestor_pruning env g ancestors then 472 raise Error "meson: ancestor pruning" 473 else if ancestor_cut ancestor_cutting env g ancestors then 474 cont (update_proof (cons (ASSUME g)) state) 475 else 476 let 477 fun reduction a () = 478 let 479 val state = update_env (K(unify_literals env g (negate a)))state 480 val state = update_proof (cons (ASSUME g)) state 481 in 482 cont state 483 end 484 val expansion = expand_rule ancestors g cont state 485 in 486 first_choice 487 (map reduction ancestors @ 488 map expansion (rules_unify rules (formula_subst env g))) () 489 end) 490 and expand_rule ancestors g cont {env, depth, proof, offset} r () = 491 let 492 val depth = depth - #asmn r 493 val () = 494 if 0 <= depth then () 495 else (saturated := false; raise Error "meson: too deep") (* OK *) 496 val (r',offset) = freshen_rule r offset 497 val (th,asms,env) = next_state state_simplify env r' g 498 val asms = if 2 <= sort_literals then sort_lits asms else asms 499 val () = record_infs (!meter) 1 500 val _ = chatting 6 andalso chat ("meson rule: "^rule_to_string r^"\n") 501 in 502 expands (g :: ancestors) asms (cont o modus_ponens th asms) 503 {env = env, depth = depth, proof = proof, offset = offset} 504 end 505 and expands ancestors g c (s as {depth = n, ...}) = 506 if divide_conquer andalso divisible g then 507 let 508 val (l1, l2) = halves (length g) 509 val (g1, g2) = divide g l1 510 val (f1, f2) = Df (expands ancestors) (g1, g2) 511 val (n1, n2) = halves n 512 val s = update_depth (K n1) s 513 in 514 binary_choice 515 (fn () => f1 (f2 c o reward n2) s) 516 (fn () => f2 (spend (n1 + 1) f1 (c o swivelp l1 l2) o reward n2) s) () 517 end 518 else foldl (uncurry (cut expand ancestors)) c (rev g) s 519 in 520 cut expand [] 521 end; 522 523(* ------------------------------------------------------------------------- *) 524(* Full meson procedure. *) 525(* ------------------------------------------------------------------------- *) 526 527fun meson_finally g ({env, proof, ...} : state) = 528 let 529 val () = assert (length proof = length g) (Bug "meson: bad final state") 530 val g' = map (formula_subst env) g 531 val proof' = map (INST env) (rev proof) 532 val _ = chatting 4 andalso chat 533 (foldl (fn (h,t)=>t^" "^thm_to_string h^"\n") "meson_finally:\n" proof') 534 val () = 535 assert (List.all (uncurry thm_proves) (zip proof' g')) 536 (Bug "meson: did not prove goal list") 537 in 538 (SOME (FRESH_VARSL proof'), CHOICE no_choice) 539 end; 540 541fun raw_meson system goals depth = 542 choice_stream 543 (fn () => 544 foldl (uncurry (meson_expand system)) (meson_finally goals) (rev goals) 545 {env = |<>|, depth = depth, proof = [], offset = 0}); 546 547(* ------------------------------------------------------------------------- *) 548(* Raw solvers. *) 549(* ------------------------------------------------------------------------- *) 550 551type 'a system = 552 {parm : parameters, rules : rules, meter : meter ref, saturated : bool ref, 553 cut : 554 (formula list -> formula -> (state -> 'a) -> state -> 'a) -> 555 formula list -> formula -> (state -> 'a) -> state -> 'a}; 556 557fun mk_system parm units meter rules : 'a system = 558 let 559 val {cache_cutting = caching, unit_lemmaizing = lemmaizing, ...} = parm 560 in 561 {parm = parm, 562 rules = rules, 563 meter = meter, 564 saturated = ref false, 565 cut = unit_cut lemmaizing units o cache_cut caching} 566 end; 567 568fun meson' (name,parm) = 569 mk_solver_node 570 {name = name, 571 solver_con = 572 fn {slice, units, thms, hyps} => 573 let 574 val ruls = meson_rules parm thms hyps 575 val _ = chatting 3 andalso chat 576 (name ^ "--initializing--#thms=" ^ int_to_string (length thms) ^ 577 "--#hyps=" ^ int_to_string (length hyps) ^ 578 "--#rules=" ^ int_to_string (num_rules ruls) ^ 579 "--#initial_rules=" ^ int_to_string (num_initial_rules ruls) ^ ".\n") 580 val system as {saturated = b, ...} = mk_system parm units slice ruls 581 fun d n = if !b then S.NIL 582 else (b := true; S.CONS (n, fn () => d (n + 1))) (* OK *) 583 fun f q d = 584 (chatting 1 andalso chat ("-" ^ int_to_string d); 585 raw_meson system q d) 586 fun unit_check goals NONE = U.prove (!units) goals | unit_check _ s = s 587 in 588 fn goals => 589 filter_meter slice 590 (S.map (unit_check goals) (S.flatten (S.map (f goals) (d 0)))) 591 end}; 592 593val meson = meson' ("meson",defaults); 594 595fun delta' (name,parm) = 596 mk_solver_node 597 {name = name, 598 solver_con = 599 fn {slice, units, thms, hyps} => 600 let 601 val ruls = meson_rules parm thms hyps 602 val dgoals = thms_to_delta_goals hyps 603 val _ = chatting 3 andalso chat 604 (name ^ "--initializing--#thms=" ^ int_to_string (length thms) ^ 605 "--#hyps=" ^ int_to_string (length hyps) ^ 606 "--#rules=" ^ int_to_string (num_rules ruls) ^ 607 "--#delta_goals=" ^ int_to_string (length dgoals) ^ ".\n") 608 val system as {saturated = b, ...} = mk_system parm units slice ruls 609 val delta_goals = S.from_list dgoals 610 fun d n = if !b then S.NIL 611 else (b := true; S.CONS (n, fn () => d (n + 1))) (* OK *) 612 fun f d g = 613 (chatting 1 andalso chat "+"; 614 S.map (K NONE) (raw_meson system [g] d)) 615 fun g d = 616 (chatting 1 andalso chat (int_to_string d); 617 S.flatten (S.map (f d) delta_goals)) 618 fun h () = S.flatten (S.map g (d 0)) 619 fun unit_check goals NONE = U.prove (!units) goals | unit_check _ s = s 620 in 621 case delta_goals of S.NIL => K S.NIL 622 | _ => fn goals => filter_meter slice (S.map (unit_check goals) (h ())) 623 end}; 624 625val delta = delta' ("delta",defaults); 626 627val prolog_depth = case Int.maxInt of NONE => 1000000 | SOME i => i; 628 629fun prolog' (name,parm) = 630 mk_solver_node 631 {name = name, 632 solver_con = 633 fn {slice, units, thms, hyps} => 634 let 635 val system = mk_system parm units slice (prolog_rules parm thms hyps) 636 fun comment S.NIL = "!\n" 637 | comment (S.CONS (NONE, _)) = "-" 638 | comment (S.CONS (SOME _, _)) = "$\n" 639 fun f S.NIL = S.NIL | f (S.CONS (x,xs)) = S.CONS (x, fn () => g (xs ())) 640 and g x = (chatting 1 andalso chat (comment x); f x) 641 in 642 fn goals => g (raw_meson system goals prolog_depth) 643 end}; 644 645local val p = update_sort_literals (K 0) (update_sort_rules (K false) defaults); 646in val prolog = prolog' ("prolog",p); 647end; 648 649end 650