1(* ========================================================================= *) 2(* FINITE MODELS *) 3(* Copyright (c) 2003-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load ["mlibHeap", "mlibTerm", "mlibSubst", "mlibMatch", "mlibThm", "mlibTermorder"]; 8*) 9 10(* 11*) 12structure mlibModel :> mlibModel = 13struct 14 15open mlibUseful mlibTerm; 16 17structure W = Word; local open Word in end; 18 19(* ------------------------------------------------------------------------- *) 20(* Chatting. *) 21(* ------------------------------------------------------------------------- *) 22 23val module = "mlibModel"; 24val () = add_trace {module = module, alignment = I} 25fun chatting l = tracing {module = module, level = l}; 26fun chat s = (trace s; true) 27 28(* ------------------------------------------------------------------------- *) 29(* Helper functions. *) 30(* ------------------------------------------------------------------------- *) 31 32val gen = Random.newgenseed 1.0; 33 34type fp = string * int list; 35 36val fp_compare = lex_order String.compare (lex_list_order Int.compare); 37 38val pp_fp = pp_map 39 (fn (f,a) => Fn (f, map (fn n => Fn (int_to_string n, [])) a)) pp_term; 40 41fun cached c f k = 42 case Binarymap.peek (!c,k) of 43 SOME v => v 44 | NONE => 45 let 46 val v = f k 47 val () = c := Binarymap.insert (!c,k,v) (* OK *) 48 (* - caches are private per model *) 49 in 50 v 51 end; 52 53fun log2_int 1 = 0 | log2_int n = 1 + log2_int (n div 2); 54 55(* ------------------------------------------------------------------------- *) 56(* The parts of the model that are fixed and cannot be perturbed *) 57(* Note: a model of size N has integer elements 0...N-1 *) 58(* ------------------------------------------------------------------------- *) 59 60type fix = int -> {func : (string * int list) -> int option, 61 pred : (string * int list) -> bool option}; 62 63fun fix_merge fix1 fix2 N = 64 let 65 val {func = func1, pred = pred1} = fix1 N 66 val {func = func2, pred = pred2} = fix2 N 67 fun func x = case func1 x of NONE => func2 x | sn => sn 68 fun pred x = case pred1 x of NONE => pred2 x | sb => sb 69 in 70 {func = func, pred = pred} 71 end; 72 73fun fix_mergel fixl = foldl (fn (h,t) => fix_merge h t) (hd fixl) (tl fixl); 74 75fun map_fix map_fn fix N = 76 let 77 val {func,pred} = fix N 78 fun func' (f,a) = case map_fn f of NONE => NONE | SOME f' => func (f',a) 79 fun pred' (p,a) = case map_fn p of NONE => NONE | SOME p' => pred (p',a) 80 in 81 {func = func', pred = pred'} 82 end; 83 84val pure_fix : fix = 85 fn _ => {func = K NONE, pred = fn ("=",[m,n]) => SOME (m = n) | _ => NONE}; 86 87val basic_fix : fix = 88 let 89 fun func ("id",[n]) = SOME n 90 | func ("fst",[n,_]) = SOME n 91 | func ("snd",[_,n]) = SOME n 92 | func ("#1",n::_) = SOME n 93 | func ("#2",_::n::_) = SOME n 94 | func ("#3",_::_::n::_) = SOME n 95 | func _ = NONE 96 fun pred ("<>",[m,n]) = SOME (m = n) 97 | pred _ = NONE 98 in 99 K {func = func, pred = pred} 100 end; 101 102local 103 type div_set = (int * int) Binaryset.set 104 val empty : div_set = Binaryset.empty (lex_order Int.compare Int.compare); 105 fun member i (s : div_set) = Binaryset.member (s,i); 106 fun add i (s : div_set) = Binaryset.add (s,i); 107 108 fun mk_div _ i 0 s = add (i,0) s 109 | mk_div N i j s = mk_div N i ((j + i) mod N) (add (i,j) s); 110in 111 fun modulo_fix N = 112 let 113 fun f x = x mod N 114 val divides = foldl (fn (i,s) => mk_div N i i s) empty (interval 0 N) 115 val zero = f 0 and one = f 1 and two = f 2 116 fun func ("0",[]) = SOME zero 117 | func ("1",[]) = SOME one 118 | func ("2",[]) = SOME two 119 | func ("suc",[n]) = SOME (f (n + one)) 120 | func ("pre",[n]) = SOME (f (n - one)) 121 | func ("~",[n]) = SOME (f (~n)) 122 | func ("+",[m,n]) = SOME (f (m + n)) 123 | func ("-",[m,n]) = SOME (f (m - n)) 124 | func ("*",[m,n]) = SOME (f (m * n)) 125 | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one) 126 | func ("mod",[m,n]) = SOME (if n = zero then m else m mod n) 127 | func _ = NONE 128 fun pred ("<=",[m,n]) = SOME (m <= n) 129 | pred ("<",[m,n]) = SOME (m < n) 130 | pred (">",[m,n]) = SOME (m > n) 131 | pred (">=",[m,n]) = SOME (m >= n) 132 | pred ("is_0",[n]) = SOME (n = zero) 133 | pred ("divides",[m,n]) = SOME (member (m,n) divides) 134 | pred ("odd",[n]) = Option.map not (pred ("even",[n])) 135 | pred ("even",[n]) = pred ("divides",[two,n]) 136 | pred _ = NONE 137 in 138 {func = func, pred = pred} 139 end; 140end; 141 142fun heap_fix N = 143 let 144 val M = N - 1 145 fun f x = if x <= 0 then 0 else if M <= x then M else x 146 val zero = f 0 and one = f 1 and two = f 2 147 fun func ("0",[]) = SOME zero 148 | func ("1",[]) = SOME one 149 | func ("2",[]) = SOME two 150 | func ("suc",[m]) = SOME (f (m + one)) 151 | func ("pre",[m]) = SOME (f (m - one)) 152 | func ("+",[m,n]) = SOME (f (m + n)) 153 | func ("-",[m,n]) = SOME (f (m - n)) 154 | func ("*",[m,n]) = SOME (f (m * n)) 155 | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one) 156 | func _ = NONE 157 fun pred ("<=",[m,n]) = SOME (m <= n) 158 | pred ("<",[m,n]) = SOME (m < n) 159 | pred (">",[m,n]) = SOME (m > n) 160 | pred (">=",[m,n]) = SOME (m >= n) 161 | pred ("is_0",[m]) = SOME (m = zero) 162 | pred _ = NONE 163 in 164 {func = func, pred = pred} 165 end; 166 167fun set_fix N = 168 let 169 val empty = 0w0 170 and univ = W.- (W.<< (0w1, W.fromInt (log2_int N)), 0w1) 171 fun to_set n = W.max (W.fromInt n, univ) 172 val from_set = W.toInt 173 fun union s t = W.orb (s,t) 174 fun inter s t = W.andb (s,t) 175 fun compl s = W.andb (W.notb s, univ) 176 fun subset s t = inter s (compl t) = empty 177 fun count_bits w = 178 if w = 0w0 then 0 else 179 (if W.andb (w,0w1) = 0w1 then 1 else 0) + count_bits (W.>> (w,0w1)) 180 fun func ("empty",[]) = SOME (from_set empty) 181 | func ("univ",[]) = SOME (from_set univ) 182 | func ("union",[m,n]) = SOME (from_set (union (to_set m) (to_set n))) 183 | func ("inter",[m,n]) = SOME (from_set (inter (to_set m) (to_set n))) 184 | func ("compl",[n]) = SOME (from_set (compl (to_set n))) 185 | func ("card",[n]) = SOME (count_bits (to_set n)) 186 | func _ = NONE 187 fun pred ("in",[_,n]) = 188 let 189 val s = to_set n 190 in 191 if s = empty then SOME false 192 else if s = univ then SOME true else NONE 193 end 194 | pred ("subset",[m,n]) = SOME (subset (to_set m) (to_set n)) 195 | pred _ = NONE 196 in 197 {func = func, pred = pred} 198 end; 199 200(* ------------------------------------------------------------------------- *) 201(* Parameters *) 202(* ------------------------------------------------------------------------- *) 203 204type parameters = {size : int, fix : fix}; 205 206val defaults = {size = 5, fix = pure_fix}; 207 208fun update_size f (parm : parameters) : parameters = 209 let val {size = n, fix = r} = parm in {size = f n, fix = r} end; 210 211fun update_fix f (parm : parameters) : parameters = 212 let val {size = n, fix = r} = parm in {size = n, fix = f r} end; 213 214(* ------------------------------------------------------------------------- *) 215(* Valuations. *) 216(* ------------------------------------------------------------------------- *) 217 218type valuation = (string,int) Binarymap.dict; 219 220val emptyv : valuation = Binarymap.mkDict String.compare; 221 222fun insertv (v |-> n) s : valuation = Binarymap.insert (s,v,n); 223 224fun lookupv (s : valuation) v = 225 case Binarymap.peek (s,v) of SOME n => n 226 | NONE => raise Bug "mlibModel.lookupv"; 227 228fun randomv n = 229 let fun f (v,s) = insertv (v |-> Random.range (0,n) gen) s 230 in foldl f emptyv 231 end; 232 233val pp_valuation = 234 pp_map (map op|-> o Binarymap.listItems) 235 (pp_list (pp_maplet pp_string pp_int)); 236 237fun valuation_to_string v = PP.pp_to_string (!LINE_LENGTH) pp_valuation v; 238 239(* ------------------------------------------------------------------------- *) 240(* Random models are based on cryptographic hashing *) 241(* ------------------------------------------------------------------------- *) 242 243local 244 fun randomize id p pred args = 245 let 246 val mesg = 247 int_to_string id ^ " " ^ p ^ " " ^ (if pred then "p" else "f") ^ 248 foldl (fn (a,s) => s ^ " " ^ int_to_string a) "" args 249 val hash = mlibPortable.md5 mesg 250 val _ = chatting 4 andalso 251 chat ("randomize: mesg=" ^ mesg ^ ", hash=" ^ hash ^ ".\n") 252 in 253 hash 254 end; 255 256 (* Extraction is supposed to follow a uniform distribution. *) 257 (* Unless we are lucky enough to get BASE mod N = 0, to keep the bias *) 258 (* beneath MAX_BIAS we must ensure the number of iterations n satisfies *) 259 (* BASE^n / N >= 1 / MAX_BIAS. *) 260 val BASE = 64; 261 val MAX_BIAS = 0.01; 262 263 val bias = Real.ceil (1.0 / MAX_BIAS); 264 fun extract N = 265 let 266 val base_mod_N = BASE mod N 267 fun ext _ _ [] = raise Bug "mlibModel.extract: ran out of data" 268 | ext t i (c :: cs) = 269 let 270 val i = (base_mod_N * i + base64_to_int c) mod N 271 val t = t div BASE 272 in 273 if t = 0 orelse base_mod_N = 0 then i else ext t i cs 274 end 275 in 276 ext (N * bias - 1) 0 277 end; 278in 279 fun random_fn N id (f,args) = 280 extract N (String.explode (randomize id f false args)); 281 282 fun random_pred id (p,args) = 283 base64_to_int (String.sub (randomize id p true args, 0)) mod 2 = 0; 284end; 285 286fun cached_random_fn cache N id f_args = cached cache (random_fn N id) f_args; 287fun cached_random_pred cache id p_args = cached cache (random_pred id) p_args; 288 289(* ------------------------------------------------------------------------- *) 290(* Representing finite models. *) 291(* ------------------------------------------------------------------------- *) 292 293datatype model = MODEL of 294 {parm : parameters, 295 id : int, 296 cachef : (fp,int) Binarymap.dict ref, 297 cachep : (fp,bool) Binarymap.dict ref, 298 overf : (fp,int) Binarymap.dict, 299 overp : (fp,bool) Binarymap.dict, 300 fixf : (string * int list) -> int option, 301 fixp : (string * int list) -> bool option}; 302 303local 304 val new_id = Portable.make_counter{inc=1,init=0} 305in 306 fun new (parm : parameters) = 307 let 308 val {size = n, fix = r} = parm 309 val {func = fixf, pred = fixp} = r n 310 val () = assert (1 <= n) (Bug "mlibModel.new: nonpositive size") 311 val id = new_id () 312 val cachef = ref (Binarymap.mkDict fp_compare) 313 val cachep = ref (Binarymap.mkDict fp_compare) 314 val overf = Binarymap.mkDict fp_compare 315 val overp = Binarymap.mkDict fp_compare 316 in 317 MODEL 318 {parm = parm, id = id, cachef = cachef, cachep = cachep, 319 overf = overf, overp = overp, fixf = fixf, fixp = fixp} 320 end; 321end; 322 323fun msize (MODEL {parm = {size = N, ...}, ...}) = N; 324 325fun update_overf overf m = 326 let val MODEL {parm, id, cachef, cachep, overp, fixf, fixp, ...} = m 327 in MODEL {parm = parm, id = id, cachef = cachef, cachep = cachep, 328 overf = overf, overp = overp, fixf = fixf, fixp = fixp} 329 end; 330 331fun update_overp overp m = 332 let val MODEL {parm, id, cachef, cachep, overf, fixf, fixp, ...} = m 333 in MODEL {parm = parm, id = id, cachef = cachef, cachep = cachep, 334 overf = overf, overp = overp, fixf = fixf, fixp = fixp} 335 end; 336 337fun pp_model (MODEL {parm = {size = N, ...}, id, ...}) = 338 pp_string (int_to_string id ^ ":" ^ int_to_string N); 339 340(* ------------------------------------------------------------------------- *) 341(* Evaluating ground formulas on models *) 342(* ------------------------------------------------------------------------- *) 343 344fun eval_fn m f_args = 345 let 346 val MODEL {parm = {size = N, ...}, id, cachef, overf, fixf, ...} = m 347 in 348 case fixf f_args of SOME b => b 349 | NONE => 350 (case Binarymap.peek (overf,f_args) of SOME n => n 351 | NONE => cached_random_fn cachef N id f_args) 352 end; 353 354fun eval_pred m p_args = 355 let 356 val MODEL {id,cachep,overp,fixp,...} = m 357 in 358 case fixp p_args of SOME b => b 359 | NONE => 360 (case Binarymap.peek (overp,p_args) of SOME b => b 361 | NONE => cached_random_pred cachep id p_args) 362 end; 363 364fun eval_term m v = 365 let 366 fun e (Var x) = lookupv v x 367 | e (Fn (f,a)) = eval_fn m (f, map (eval_term m v) a) 368 in 369 e 370 end; 371 372fun evaluate_term m tm = eval_term m emptyv tm; 373 374fun eval_formula m = 375 let 376 fun e True _ = true 377 | e False _ = false 378 | e (Atom (Var _)) _ = raise Bug "eval_formula: boolean var" 379 | e (Atom (Fn (p,a))) v = eval_pred m (p, map (eval_term m v) a) 380 | e (Not p) v = not (e p v) 381 | e (Or (p,q)) v = e p v orelse e q v 382 | e (And (p,q)) v = e p v andalso e q v 383 | e (Imp (p,q)) v = e (Or (Not p, q)) v 384 | e (Iff (p,q)) v = e p v = e q v 385 | e (Forall (x,p)) v = List.all (e' p v x) (interval 0 (msize m)) 386 | e (Exists (x,p)) v = e (Not (Forall (x, Not p))) v 387 and e' fm v x n = e fm (insertv (x |-> n) v) 388 in 389 fn v => fn fm => e fm v 390 end; 391 392fun evaluate_formula m fm = eval_formula m emptyv fm; 393 394(* ------------------------------------------------------------------------- *) 395(* Check whether a random grounding of a formula is satisfied by the model *) 396(* ------------------------------------------------------------------------- *) 397 398fun check1 fvs m fm = 399 let 400 val v = randomv (msize m) fvs 401 val _ = chatting 3 andalso 402 chat ("check: valuation=" ^ valuation_to_string v ^ ".\n") 403 in 404 eval_formula m v fm 405 end; 406 407fun check m fm = check1 (FV fm) m fm; 408 409fun checkn m fm n = 410 let 411 val fvs = FV fm 412 val r = 413 if null fvs then if check1 [] m fm then n else 0 414 else funpow n (fn i => if check1 fvs m fm then i + 1 else i) 0 415 val _ = chatting 1 andalso 416 chat ("checkn: " ^ formula_to_string fm ^ ": " ^ 417 int_to_string r ^ "/" ^ int_to_string n ^ "\n") 418 in 419 r 420 end; 421 422fun count m fm = 423 let 424 val n = rev (interval 0 (msize m)) 425 fun f x [] = x 426 | f (i,j) ((v,[]) :: l) = 427 f ((if eval_formula m v fm then i + 1 else i), j + 1) l 428 | f x ((v, w :: ws) :: l) = 429 f x (foldl (fn (i,z) => (insertv (w |-> i) v, ws) :: z) l n) 430 val r = f (0,0) [(emptyv, FV fm)] 431 val _ = chatting 1 andalso 432 chat ("count: " ^ formula_to_string fm ^ ": " ^ 433 int_to_string (fst r) ^ "/" ^ int_to_string (snd r) ^ "\n") 434 in 435 r 436 end; 437 438(* ------------------------------------------------------------------------- *) 439(* Sets of model perturbations *) 440(* ------------------------------------------------------------------------- *) 441 442datatype perturbation = PredP of (fp,bool) maplet | FnP of (fp,int) maplet; 443 444val pp_perturbation = 445 pp_map (fn PredP (p |-> s) => p |-> bool_to_string s 446 | FnP (p |-> n) => p |-> int_to_string n) 447 (pp_maplet pp_fp pp_string); 448 449fun perturbation_to_string p = PP.pp_to_string (!LINE_LENGTH) pp_perturbation p; 450 451fun comparep (PredP _, FnP _) = LESS 452 | comparep (PredP (p1 |-> b1), PredP (p2 |-> b2)) = 453 lex_order fp_compare bool_compare ((p1,b1),(p2,b2)) 454 | comparep (FnP (f1 |-> n1), FnP (f2 |-> n2)) = 455 lex_order fp_compare Int.compare ((f1,n1),(f2,n2)) 456 | comparep (FnP _, PredP _) = GREATER; 457 458val emptyp : perturbation Binaryset.set = Binaryset.empty comparep; 459 460val sizep = Binaryset.numItems; 461 462fun randomp s = List.nth (Binaryset.listItems s, Random.range (0, sizep s) gen); 463 464fun addp x s = Binaryset.add (s,x); 465 466fun deletep x s = Binaryset.delete (s,x); 467 468fun unionp s t = Binaryset.union (s,t); 469 470fun interp s t = Binaryset.intersection (s,t); 471 472(* ------------------------------------------------------------------------- *) 473(* Perturbing a model to make a ground formula true *) 474(* ------------------------------------------------------------------------- *) 475 476fun perturb_targets N p = 477 let 478 val dom = interval 0 N 479 fun g l t x = p (List.revAppend (l, x :: t)) 480 fun f acc _ [] = rev acc 481 | f acc l (h :: t) = f (List.filter (g l t) dom :: acc) (h :: l) t 482 in 483 f [] [] 484 end; 485 486fun perturb_fnl m v = 487 let 488 val MODEL {fixf,...} = m 489 fun pert_fnl tms targs set = foldl pert_fn set (zip tms targs) 490 and pert_fn ((_,[]),set) = set 491 | pert_fn ((Var _,_),set) = set 492 | pert_fn ((Fn (f,tms), targ), set) = 493 let 494 val targset = Intset.addList (Intset.empty,targ) 495 fun testf args = Intset.member (targset, eval_fn m (f,args)) 496 val args = map (eval_term m v) tms 497 val targs = perturb_targets (msize m) testf args 498 val set = 499 case fixf (f,args) of (SOME _) => set 500 | NONE => foldl (fn (x,s) => addp (FnP ((f,args) |-> x)) s) set targ 501 in 502 pert_fnl tms targs set 503 end 504 in 505 pert_fnl 506 end; 507 508fun perturb_atom m v s (p,tms) = 509 let 510 val MODEL {fixp,...} = m 511 fun testp args = eval_pred m (p,args) = s 512 val args = map (eval_term m v) tms 513 val targs = perturb_targets (msize m) testp args 514 val set = 515 case fixp (p,args) of (SOME _) => emptyp 516 | NONE => addp (PredP ((p,args) |-> s)) emptyp 517 in 518 perturb_fnl m v tms targs set 519 end; 520 521fun perturb_formula m = 522 let 523 fun ex v x = map (fn n => insertv (x |-> n) v) (interval 0 (msize m)) 524 fun f _ _ True = emptyp 525 | f _ _ False = emptyp 526 | f s v (Not p) = f (not s) v p 527 | f _ _ (Atom (Var _)) = raise Bug "perturb_formula: boolean var" 528 | f s v (Atom (Fn p)) = perturb_atom m v s p 529 | f true v (Or (p,q)) = fl unionp [(v,p),(v,q)] 530 | f false v (Or (p,q)) = f true v (And (Not p, Not q)) 531 | f true v (And (p,q)) = flc interp [(v,p),(v,q)] 532 | f false v (And (p,q)) = f true v (Or (Not p, Not q)) 533 | f s v (Imp (p,q)) = f s v (Or (Not p, q)) 534 | f s v (Iff (p,q)) = f s v (And (Imp (p,q), Imp (q,p))) 535 | f true v (Exists (x,p)) = fl unionp (map (fn w => (w,p)) (ex v x)) 536 | f false v (Exists (x,p)) = f true v (Forall (x, Not p)) 537 | f true v (Forall (x,p)) = flc interp (map (fn w => (w,p)) (ex v x)) 538 | f false v (Forall (x,p)) = f true v (Exists (x, Not p)) 539 and flc c l = fl c (List.filter (fn (v,p) => not (eval_formula m v p)) l) 540 and fl c l = 541 case map (fn (v,p) => f true v p) l of 542 [] => raise Bug "perturb_formula: no identity" 543 | h :: t => foldl (fn (s,x) => c s x) h t 544 in 545 f true 546 end; 547 548fun override m = 549 let 550 val MODEL {overf,overp,fixf,fixp,...} = m 551 in 552 fn PredP (p |-> b) => 553 (if chatting 2 andalso chat "checking pred override\n" andalso 554 Option.isSome (fixp p) then raise Bug "override: fixp" else (); 555 update_overp (Binarymap.insert (overp,p,b)) m) 556 | FnP (f |-> n) => 557 (if chatting 2 andalso chat "checking fn override\n" andalso 558 Option.isSome (fixf f) then raise Bug "override: fixf" else (); 559 update_overf (Binarymap.insert (overf,f,n)) m) 560 end; 561 562fun perturb m v fm = 563 let 564 fun f perts = 565 if sizep perts = 0 then NONE else 566 let 567 val pert = randomp perts 568 val m' = override m pert 569 val good = eval_formula m' v fm 570 val _ = chatting 2 andalso 571 chat ("perturb: " ^ (if good then "good" else "bad") ^ 572 " pert: " ^ perturbation_to_string pert ^ ".\n") 573 in 574 if good then SOME m' else f (deletep pert perts) 575 end 576 in 577 f (perturb_formula m v fm) 578 end; 579 580local 581 fun integrate (vs,fm,n,i,p) m = 582 let 583 val v = randomv (msize m) vs 584 val _ = chatting 3 andalso 585 chat ("integrate: valuation=" ^ valuation_to_string v ^ ".\n") 586 in 587 if eval_formula m v fm then ((vs, fm, n + 1, i, p), m) else 588 case perturb m v fm of NONE => ((vs, fm, n, i + 1, p), m) 589 | SOME m => ((vs, fm, n, i, p + 1), m) 590 end; 591 592 fun chatperturb (_,fm,n,i,p) = 593 (chat ("perturb: " ^ formula_to_string fm ^ "\n" ^ 594 " tests=" ^ int_to_string (n + i + p) ^ 595 ": natural=" ^ int_to_string n ^ 596 ", impossible=" ^ int_to_string i ^ 597 ", perturbed=" ^ int_to_string p ^ ".\n"); true); 598in 599 fun perturb fms perts m = 600 let 601 val fmi = map (fn p => (FV p, p, 0, 0, 0)) fms 602 val (fmi,m) = funpow perts (uncurry (maps integrate)) (fmi,m) 603 val _ = chatting 1 andalso List.all chatperturb fmi 604 in 605 m 606 end; 607end; 608 609(* ------------------------------------------------------------------------- *) 610(* Pretty-printing terms with free vars *) 611(* ------------------------------------------------------------------------- *) 612 613local 614 exception Toomany; 615 616 val i2s = int_to_string; 617 618 fun b2s true = "T" | b2s false = "F"; 619 620 val mkv = foldl (fn (x,v) => insertv x v) emptyv; 621 622 fun tablify tab = 623 join "\n" 624 (align_table {pad = #" ", left = false} 625 (map (fn l => (" " ^ hd l) :: map (fn x => " " ^ x) (tl l)) tab)) ^ "\n"; 626 627 fun to_string eval x2s m tm [] = x2s (eval m (mkv []) tm) 628 | to_string eval x2s m tm [v] = 629 let 630 val l = interval 0 (msize m) 631 val head = v :: map i2s l 632 val line = "" :: map (fn x => x2s (eval m (mkv [v |-> x]) tm)) l 633 in 634 tablify [head,line] 635 end 636 | to_string eval x2s m tm [v,w] = 637 let 638 val l = interval 0 (msize m) 639 val head = ["" :: v :: map i2s l, w :: "" :: map (K "") l] 640 fun f y x = x2s (eval m (mkv [v |-> x, w |-> y]) tm) 641 val tab = head @ map (fn y => i2s y :: "" :: map (f y) l) l 642 in 643 tablify tab 644 end 645 | to_string _ _ _ _ _ = raise Toomany; 646in 647 fun term_to_string m tm = 648 to_string eval_term i2s m tm (FVT tm) 649 handle Toomany => raise Error "mlibModel.term_to_string: too many free vars"; 650 651 fun formula_to_string m fm = 652 to_string eval_formula b2s m fm (FV fm) 653 handle Toomany => raise Error "mlibModel.formula_to_string: too many free vars"; 654end; 655 656(* ------------------------------------------------------------------------- *) 657(* Rebinding for signature *) 658(* ------------------------------------------------------------------------- *) 659 660val size = msize; 661 662end 663