(* This file was generated by the "make_metis" script. The BSD License is used with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010 email written by him:
I hereby give permission to the Isabelle team to release Metis as part of Isabelle, with the Metis code covered under the Isabelle BSD license.
*)
(******************************************************************) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) (******************************************************************)
(**** Original file: src/Random.sig ****)
(* Title: Tools/random_word.ML Author: Makarius
Simple generator for pseudo-random numbers, using unboxed word arithmetic only. Unprotected concurrency introduces some true randomness.
*)
signature Metis_Random = sig
val nextWord : unit -> word
val nextBool : unit -> bool
val nextInt : int -> int (* k -> [0,k) *)
val nextReal : unit -> real (* () -> [0,1) *)
end;
(**** Original file: src/Random.sml ****)
(* Title: Tools/random_word.ML Author: Makarius
Simple generator for pseudo-random numbers, using unboxed word arithmetic only. Unprotected concurrency introduces some true randomness.
*)
structure Metis_Random :> Metis_Random = struct
(* random words: 0w0 <= result <= max_word *)
(*minimum length of unboxed words on all supported ML platforms*) val _ = Word.wordSize >= 30
orelse raise Fail ("Bad platform word size");
val max_word = 0wx3FFFFFFF; val top_bit = 0wx20000000;
fun change r f = r := f (!r);
local val rand = (*Unsynchronized.*)Unsynchronized.ref 0w1 infun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
(*NB: higher bits are more random than lower ones*) fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;
(* random integers: 0 <= result < k *)
val max_int = Word.toInt max_word;
fun nextInt k = if k <= 0 orelse k > max_int thenraise Fail ("next_int: out of range") elseif k = max_int then Word.toInt (nextWord ()) else Word.toInt (Word.mod (nextWord (), Word.fromInt k));
(* random reals: 0.0 <= result < 1.0 *)
val scaling = real max_int + 1.0; fun nextReal () = real (Word.toInt (nextWord ())) / scaling;
end;
(**** Original file: src/Portable.sig ****)
(* ========================================================================= *) (* ML COMPILER SPECIFIC FUNCTIONS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Portable = sig
(* ------------------------------------------------------------------------- *) (* The ML implementation. *) (* ------------------------------------------------------------------------- *)
val ml : string
(* ------------------------------------------------------------------------- *) (* Pointer equality using the run-time system. *) (* ------------------------------------------------------------------------- *)
fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
local val lock = Thread.Mutex.mutex (); in fun critical e () = Multithreading.synchronized "metis" lock e end;
val randomWord = Metis_Random.nextWord val randomBool = Metis_Random.nextBool val randomInt = Metis_Random.nextInt val randomReal = Metis_Random.nextReal
fun time f x = f x (* dummy *)
end
datatype'a frag = QUOTE of string | ANTIQUOTE of 'a
(**** Original file: src/Useful.sig ****)
(* ========================================================================= *) (* ML UTILITY FUNCTIONS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
val mapCompare : ('a -> 'b) -> ('b * 'b -> order) -> 'a * 'a -> order
val revCompare : ('a * 'a -> order) -> 'a * 'a -> order
val prodCompare :
('a * 'a -> order) -> ('b * 'b -> order) -> ('a * 'b) * ('a * 'b) -> order
val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order
val optionCompare : ('a * 'a -> order) -> 'a option * 'a option -> order
val boolCompare : bool * bool -> order (* false < true *)
(* ------------------------------------------------------------------------- *) (* Lists: note we count elements from 0. *) (* ------------------------------------------------------------------------- *)
val cons : 'a -> 'a list -> 'a list
val hdTl : 'a list -> 'a * 'a list
val append : 'a list -> 'a list -> 'a list
val singleton : 'a -> 'a list
val first : ('a -> 'b option) -> 'a list -> 'b option
val maps : ('a -> 's -> 'b * 's) -> 'a list -> 's -> 'b list * 's
val mapsPartial : ('a -> 's -> 'b option * 's) -> 'a list -> 's -> 'b list * 's
val zipWith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val zip : 'a list -> 'b list -> ('a * 'b) list
val unzip : ('a * 'b) list -> 'a list * 'b list
val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val cart : 'a list -> 'b list -> ('a * 'b) list
val takeWhile : ('a -> bool) -> 'a list -> 'a list
val dropWhile : ('a -> bool) -> 'a list -> 'a list
val divideWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
val groups : ('a * 's -> bool * 's) -> 's -> 'a list -> 'a listlist
val groupsBy : ('a * 'a -> bool) -> 'a list -> 'a listlist
val groupsByFst : (''a * 'b) list -> (''a * 'b list) list
val groupsOf : int -> 'a list -> 'a listlist
val index : ('a -> bool) -> 'a list -> int option
val enumerate : 'a list -> (int * 'a) list
val divide : 'a list -> int -> 'a list * 'a list (* Subscript *)
val revDivide : 'a list -> int -> 'a list * 'a list (* Subscript *)
val updateNth : int * 'a -> 'a list -> 'a list (* Subscript *)
val deleteNth : int -> 'a list -> 'a list(* Subscript *)
fun first f [] = NONE
| first f (x :: xs) = (case f x of NONE => first f xs | s => s);
fun maps (_ : 'a -> 's -> 'b * 's) [] = unit []
| maps f (x :: xs) =
bind (f x) (fn y => bind (maps f xs) (fn ys => unit (y :: ys)));
fun mapsPartial (_ : 'a -> 's -> 'b option * 's) [] = unit []
| mapsPartial f (x :: xs) =
bind
(f x)
(fn yo =>
bind
(mapsPartial f xs)
(fn ys => unit (case yo of NONE => ys | SOME y => y :: ys)));
fun zipWith f = let fun z l [] [] = l
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
| z _ _ _ = raise Error "zipWith: lists different lengths"; in
fn xs => fn ys => List.rev (z [] xs ys) end;
fun zip xs ys = zipWith pair xs ys;
local fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys); in fun unzip ab = List.foldl inc ([],[]) (List.rev ab); end;
fun cartwith f = let fun aux _ res _ [] = res
| aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
| aux xsCopy res (x :: xt) (ys as y :: _) =
aux xsCopy (f x y :: res) xt ys in
fn xs => fn ys => letval xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end end;
fun cart xs ys = cartwith pair xs ys;
fun takeWhile p = let fun f acc [] = List.rev acc
| f acc (x :: xs) = if p x then f (x :: acc) xs elseList.rev acc in
f [] end;
fun dropWhile p = let fun f [] = []
| f (l as x :: xs) = if p x then f xs else l in
f end;
fun divideWhile p = let fun f acc [] = (List.rev acc, [])
| f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l) in
f [] end;
fun groups f = let fun group acc row x l = case l of
[] => let val acc = ifList.null row then acc elseList.rev row :: acc in List.rev acc end
| h :: t => let val (eor,x) = f (h,x) in if eor then group (List.rev row :: acc) [h] x t else group acc (h :: row) x t end in
group [] [] end;
fun groupsBy eq = let fun f (x_y as (x,_)) = (not (eq x_y), x) in
fn [] => []
| h :: t => case groups f h t of
[] => [[h]]
| hs :: ts => (h :: hs) :: ts end;
local fun fstEq ((x,_),(y,_)) = x = y;
fun collapse l = (fst (hd l), List.map snd l); in fun groupsByFst l = List.map collapse (groupsBy fstEq l); end;
fun groupsOf n = let fun f (_,i) = if i = 1 then (true,n) else (false, i - 1) in
groups f (n + 1) end;
fun index p = let fun idx _ [] = NONE
| idx n (x :: xs) = if p x then SOME n else idx (n + 1) xs in
idx 0 end;
fun enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0);
local fun revDiv acc l 0 = (acc,l)
| revDiv _ [] _ = raise Subscript
| revDiv acc (h :: t) n = revDiv (h :: acc) t (n - 1); in fun revDivide l = revDiv [] l; end;
fun divide l n = letval (a,b) = revDivide l n in (List.rev a, b) end;
fun updateNth (n,x) l = let val (a,b) = revDivide l n in case b of [] => raise Subscript | _ :: t => List.revAppend (a, x :: t) end;
fun deleteNth n l = let val (a,b) = revDivide l n in case b of [] => raise Subscript | _ :: t => List.revAppend (a,t) end;
(* Finding the minimum and maximum element of a list, wrt some order. *)
fun minimum cmp = let fun min (l,m,r) _ [] = (m, List.revAppend (l,r))
| min (best as (_,m,_)) l (x :: r) =
min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r in
fn [] => raise Empty
| h :: t => min ([],h,t) [h] t end;
fun maximum cmp = minimum (revCompare cmp);
(* Merge (for the following merge-sort, but generally useful too). *)
fun merge cmp = let fun mrg acc [] ys = List.revAppend (acc,ys)
| mrg acc xs [] = List.revAppend (acc,xs)
| mrg acc (xs as x :: xt) (ys as y :: yt) =
(case cmp (x,y) of
GREATER => mrg (y :: acc) xs yt
| _ => mrg (x :: acc) xt ys) in
mrg [] end;
(* Merge sort (stable). *)
fun sort cmp = let fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
| findRuns acc r rs (x :: xs) = case cmp (r,x) of
GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
| _ => findRuns acc x (r :: rs) xs
fun mergeAdj acc [] = List.rev acc
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
fun mergePairs [xs] = xs
| mergePairs l = mergePairs (mergeAdj [] l) in
fn [] => []
| l as [_] => l
| h :: t => mergePairs (findRuns [] h [] t) end;
fun sortMap _ _ [] = []
| sortMap _ _ (l as [_]) = l
| sortMap f cmp xs = let fun ncmp ((m,_),(n,_)) = cmp (m,n) val nxs = List.map (fn x => (f x, x)) xs val nys = sort ncmp nxs in List.map snd nys end;
fun interval m 0 = []
| interval m len = m :: interval (m + 1) (len - 1);
fun divides _ 0 = true
| divides 0 _ = false
| divides a b = b mod (Int.abs a) = 0;
local fun hcf 0 n = n
| hcf 1 _ = 1
| hcf m n = hcf (n mod m) m; in fun gcd m n = let val m = Int.abs m and n = Int.abs n in if m < n then hcf m n else hcf n m end; end;
val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz");
fun rotate (n,l) c k = List.nth (l, (k + Option.valOf (index (equal c) l)) mod n); in fun rot k c = if Char.isLower c then rotate lower c k elseif Char.isUpper c then rotate upper c k else c; end;
fun charToInt #"0" = SOME 0
| charToInt #"1" = SOME 1
| charToInt #"2" = SOME 2
| charToInt #"3" = SOME 3
| charToInt #"4" = SOME 4
| charToInt #"5" = SOME 5
| charToInt #"6" = SOME 6
| charToInt #"7" = SOME 7
| charToInt #"8" = SOME 8
| charToInt #"9" = SOME 9
| charToInt _ = NONE;
fun charFromInt 0 = SOME #"0"
| charFromInt 1 = SOME #"1"
| charFromInt 2 = SOME #"2"
| charFromInt 3 = SOME #"3"
| charFromInt 4 = SOME #"4"
| charFromInt 5 = SOME #"5"
| charFromInt 6 = SOME #"6"
| charFromInt 7 = SOME #"7"
| charFromInt 8 = SOME #"8"
| charFromInt 9 = SOME #"9"
| charFromInt _ = NONE;
fun nChars x = let fun dup 0 l = l | dup n l = dup (n - 1) (x :: l) in
fn n => String.implode (dup n []) end;
fun chomp s = let val n = size s in if n = 0 orelse String.sub (s, n - 1) <> #"\n"then s elseString.substring (s, 0, n - 1) end;
local fun chop l = case l of
[] => []
| h :: t => if Char.isSpace h then chop t else l; in val trim = String.implode o chop o List.rev o chop o List.rev o String.explode; end;
val join = String.concatWith;
local funmatch [] l = SOME l
| match _ [] = NONE
| match (x :: xs) (y :: ys) = if x = y thenmatch xs ys else NONE;
fun stringify acc [] = acc
| stringify acc (h :: t) = stringify (String.implode h :: acc) t; in fun split sep = let val pat = String.explode sep
fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
| div1 prev recent (l as h :: t) = casematch pat l of
NONE => div1 prev (h :: recent) t
| SOME rest => div1 (List.rev recent :: prev) [] rest in
fn s => div1 [] [] (String.explode s) end; end;
fun capitalize s = if s = ""then s else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
fun mkPrefix p s = p ^ s;
fun destPrefix p = let fun check s = ifString.isPrefix p s then () elseraise Error "destPrefix"
val sizeP = size p in
fn s => let val () = check s in String.extract (s,sizeP,NONE) end end;
fun isPrefix p = can (destPrefix p);
fun stripPrefix pred s = Substring.string (Substring.dropl pred (Substring.full s));
fun mkSuffix p s = s ^ p;
fun destSuffix p = let fun check s = ifString.isSuffix p s then () elseraise Error "destSuffix"
val sizeP = size p in
fn s => let val () = check s
val sizeS = size s in String.substring (s, 0, sizeS - sizeP) end end;
fun isSuffix p = can (destSuffix p);
fun stripSuffix pred s = Substring.string (Substring.dropr pred (Substring.full s));
type columnAlignment = {leftAlign : bool, padChar : char}
fun alignColumn {leftAlign,padChar} column = let val (n,_) = maximum Int.compare (List.mapsize column)
fun pad entry row = let val padding = nChars padChar (n - size entry) in if leftAlign then entry ^ padding ^ row else padding ^ entry ^ row end in
zipWith pad column end;
local fun alignTab aligns rows = case aligns of
[] => List.map (K "") rows
| [{leftAlign = true, padChar = #" "}] => List.map hd rows
| align :: aligns => let val col = List.map hd rows and cols = alignTab aligns (List.map tl rows) in
alignColumn align col cols end; in fun alignTable aligns rows = ifList.null rows then [] else alignTab aligns rows; end;
fun chat s = TextIO.output (TextIO.stdOut, s ^ "\n");
fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n");
local fun err x s = chide (x ^ ": " ^ s); in funtry f x = f x handle e as Error _ => (err "try" (errorToString e); raise e)
| e as Bug _ => (err "try" (bugToString e); raise e)
| e => (err "try""strange exception raised"; raise e);
val warn = err "WARNING";
fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure); end;
fun timed f a = let val tmr = Timer.startCPUTimer ()
val res = f a
val {usr,sys,...} = Timer.checkCPUTimer tmr in
(Time.toReal usr + Time.toReal sys, res) end;
local val MIN = 1.0;
fun several n t f a = let val (t',res) = timed f a val t = t + t' val n = n + 1 in if t > MIN then (t / Real.fromInt n, res) else several n t f a end; in fun timedMany f a = several 0 0.0 f a end;
val executionTime = let val startTime = Time.toReal (Time.now ()) in
fn () => Time.toReal (Time.now ()) - startTime end;
end
(**** Original file: src/Lazy.sig ****)
(* ========================================================================= *) (* SUPPORT FOR LAZY EVALUATION *) (* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Lazy = sig
type'a lazy
val quickly : 'a -> 'a lazy
val delay : (unit -> 'a) -> 'a lazy
val force : 'a lazy -> 'a
val memoize : (unit -> 'a) -> unit -> 'a
end
(**** Original file: src/Lazy.sml ****)
(* ========================================================================= *) (* SUPPORT FOR LAZY EVALUATION *) (* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Lazy :> Metis_Lazy = struct
datatype'a thunk =
Value of'a
| Thunk of unit -> 'a;
datatype'a lazy = Metis_Lazy of 'a thunk Unsynchronized.ref;
fun quickly v = Metis_Lazy (Unsynchronized.ref (Value v));
fun delay f = Metis_Lazy (Unsynchronized.ref (Thunk f));
fun force (Metis_Lazy s) = case !s of
Value v => v
| Thunk f => let val v = f ()
val () = s := Value v in
v end;
fun memoize f = let val t = delay f in
fn () => force t end;
end
(**** Original file: src/Ordered.sig ****)
(* ========================================================================= *) (* ORDERED TYPES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Ordered = sig
type t
val compare : t * t -> order
(* PROVIDES
!x : t. compare (x,x) = EQUAL
!x y : t. compare (x,y) = LESS <=> compare (y,x) = GREATER
!x y : t. compare (x,y) = EQUAL ==> compare (y,x) = EQUAL
!x y z : t. compare (x,y) = EQUAL ==> compare (x,z) = compare (y,z)
!x y z : t. compare (x,y) = LESS andalso compare (y,z) = LESS ==> compare (x,z) = LESS
!x y z : t. compare (x,y) = GREATER andalso compare (y,z) = GREATER ==> compare (x,z) = GREATER
*)
end
(**** Original file: src/Ordered.sml ****)
(* ========================================================================= *) (* ORDERED TYPES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_IntOrdered = structtype t = int val compare = Int.compare end;
structure Metis_IntPairOrdered = struct
type t = int * int;
fun compare ((i1,j1),(i2,j2)) = case Int.compare (i1,i2) of
LESS => LESS
| EQUAL => Int.compare (j1,j2)
| GREATER => GREATER;
(* ========================================================================= *) (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Map = sig
(* ------------------------------------------------------------------------- *) (* A type of finite maps. *) (* ------------------------------------------------------------------------- *)
val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
val keys : ('key,'a) map -> 'key list
val values : ('key,'a) map -> 'a list
val toList : ('key,'a) map -> ('key * 'a) list
val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
(* ------------------------------------------------------------------------- *) (* Converting a comparison function to an equality function. *) (* ------------------------------------------------------------------------- *)
fun equalKey compareKey key1 key2 = compareKey (key1,key2) = EQUAL;
datatype ('key,'value) tree =
E
| T of ('key,'value) node
and ('key,'value) node =
Node of
{size : int,
priority : priority,
left : ('key,'value) tree,
key : 'key,
value : 'value,
right : ('key,'value) tree};
fun lowerPriorityNode node1 node2 = let val Node {priority = p1, ...} = node1 and Node {priority = p2, ...} = node2 in
comparePriority (p1,p2) = LESS end;
(*BasicDebug local fun checkSizes tree = case tree of E => 0 | T (Node {size,left,right,...}) => let val l = checkSizes left and r = checkSizes right
val () = if l + 1 + r = size then () else raise Bug "wrong size" in size end;
fun checkSorted compareKey x tree = case tree of E => x | T (Node {left,key,right,...}) => let val x = checkSorted compareKey x left
val () = case x of NONE => () | SOME k => case compareKey (k,key) of LESS => () | EQUAL => raise Bug "duplicate keys" | GREATER => raise Bug "unsorted"
val x = SOME key in checkSorted compareKey x right end;
fun checkPriorities compareKey tree = case tree of E => NONE | T node => let val Node {left,right,...} = node
val () = case checkPriorities compareKey left of NONE => () | SOME lnode => if not (lowerPriorityNode node lnode) then () else raise Bug "left child has greater priority"
val () = case checkPriorities compareKey right of NONE => () | SOME rnode => if not (lowerPriorityNode node rnode) then () else raise Bug "right child has greater priority" in SOME node end; in fun treeCheckInvariants compareKey tree = let val _ = checkSizes tree
val _ = checkSorted compareKey NONE tree
val _ = checkPriorities compareKey tree in tree end handle Error err => raise Bug err; end;
*)
(* ------------------------------------------------------------------------- *) (* Tree operations. *) (* ------------------------------------------------------------------------- *)
fun treeNew () = E;
fun nodeSize (Node {size = x, ...}) = x;
fun treeSize tree = case tree of
E => 0
| T x => nodeSize x;
fun mkNode priority left key value right = let valsize = treeSize left + 1 + treeSize right in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} end;
fun mkTree priority left key value right = let val node = mkNode priority left key value right in
T node end;
(* ------------------------------------------------------------------------- *) (* Extracting the left and right spines of a tree. *) (* ------------------------------------------------------------------------- *)
fun treeLeftSpine acc tree = case tree of
E => acc
| T node => nodeLeftSpine acc node
and nodeLeftSpine acc node = let val Node {left,...} = node in
treeLeftSpine (node :: acc) left end;
fun treeRightSpine acc tree = case tree of
E => acc
| T node => nodeRightSpine acc node
and nodeRightSpine acc node = let val Node {right,...} = node in
treeRightSpine (node :: acc) right end;
fun mkNodeSingleton priority key value = let valsize = 1 and left = E and right = E in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} end;
fun nodeSingleton (key,value) = let val priority = randomPriority () in
mkNodeSingleton priority key value end;
fun treeSingleton key_value = let val node = nodeSingleton key_value in
T node end;
(* ------------------------------------------------------------------------- *) (* Appending two trees, where every element of the first tree is less than *) (* every element of the second tree. *) (* ------------------------------------------------------------------------- *)
fun treeAppend tree1 tree2 = case tree1 of
E => tree2
| T node1 => case tree2 of
E => tree1
| T node2 => if lowerPriorityNode node1 node2 then let val Node {priority,left,key,value,right,...} = node2
val left = treeAppend tree1 left in
mkTree priority left key value right end else let val Node {priority,left,key,value,right,...} = node1
val right = treeAppend right tree2 in
mkTree priority left key value right end;
(* ------------------------------------------------------------------------- *) (* Appending two trees and a node, where every element of the first tree is *) (* less than the node, which in turn is less than every element of the *) (* second tree. *) (* ------------------------------------------------------------------------- *)
fun treeCombine left node right = let val left_node = treeAppend left (T node) in
treeAppend left_node right end;
(* ------------------------------------------------------------------------- *) (* Searching a tree for a value. *) (* ------------------------------------------------------------------------- *)
fun treePeek compareKey pkey tree = case tree of
E => NONE
| T node => nodePeek compareKey pkey node
and nodePeek compareKey pkey node = let val Node {left,key,value,right,...} = node in case compareKey (pkey,key) of
LESS => treePeek compareKey pkey left
| EQUAL => SOME value
| GREATER => treePeek compareKey pkey right end;
(* ------------------------------------------------------------------------- *) (* Tree paths. *) (* ------------------------------------------------------------------------- *)
(* Generating a path by searching a tree for a key/value pair *)
fun treePeekPath compareKey pkey path tree = case tree of
E => (path,NONE)
| T node => nodePeekPath compareKey pkey path node
and nodePeekPath compareKey pkey path node = let val Node {left,key,right,...} = node in case compareKey (pkey,key) of
LESS => treePeekPath compareKey pkey ((true,node) :: path) left
| EQUAL => (path, SOME node)
| GREATER => treePeekPath compareKey pkey ((false,node) :: path) right end;
(* A path splits a tree into left/right components *)
fun addSidePath ((wentLeft,node),(leftTree,rightTree)) = let val Node {priority,left,key,value,right,...} = node in if wentLeft then (leftTree, mkTree priority rightTree key value right) else (mkTree priority left key value leftTree, rightTree) end;
fun addSidesPath left_right = List.foldl addSidePath left_right;
fun mkSidesPath path = addSidesPath (E,E) path;
(* Updating the subtree at a path *)
local fun updateTree ((wentLeft,node),tree) = let val Node {priority,left,key,value,right,...} = node in if wentLeft then mkTree priority tree key value right else mkTree priority left key value tree end; in fun updateTreePath tree = List.foldl updateTree tree; end;
(* Inserting a new node at a path position *)
fun insertNodePath node = let fun insert left_right path = case path of
[] => let val (left,right) = left_right in
treeCombine left node right end
| (step as (_,snode)) :: rest => if lowerPriorityNode snode node then let val left_right = addSidePath (step,left_right) in
insert left_right rest end else let val (left,right) = left_right
val tree = treeCombine left node right in
updateTreePath tree path end in
insert (E,E) end;
(* ------------------------------------------------------------------------- *) (* Using a key to split a node into three components: the keys comparing *) (* less than the supplied key, an optional equal key, and the keys comparing *) (* greater. *) (* ------------------------------------------------------------------------- *)
fun nodePartition compareKey pkey node = let val (path,pnode) = nodePeekPath compareKey pkey [] node in case pnode of
NONE => let val (left,right) = mkSidesPath path in
(left,NONE,right) end
| SOME node => let val Node {left,key,value,right,...} = node
val (left,right) = addSidesPath (left,right) path in
(left, SOME (key,value), right) end end;
(* ------------------------------------------------------------------------- *) (* Searching a tree for a key/value pair. *) (* ------------------------------------------------------------------------- *)
fun treePeekKey compareKey pkey tree = case tree of
E => NONE
| T node => nodePeekKey compareKey pkey node
and nodePeekKey compareKey pkey node = let val Node {left,key,value,right,...} = node in case compareKey (pkey,key) of
LESS => treePeekKey compareKey pkey left
| EQUAL => SOME (key,value)
| GREATER => treePeekKey compareKey pkey right end;
(* ------------------------------------------------------------------------- *) (* Inserting new key/values into the tree. *) (* ------------------------------------------------------------------------- *)
fun treeInsert compareKey key_value tree = let val (key,value) = key_value
val (path,inode) = treePeekPath compareKey key [] tree in case inode of
NONE => let val node = nodeSingleton (key,value) in
insertNodePath node path end
| SOME node => let val Node {size,priority,left,right,...} = node
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
updateTreePath (T node) path end end;
(* ------------------------------------------------------------------------- *) (* Deleting key/value pairs: it raises an exception if the supplied key is *) (* not present. *) (* ------------------------------------------------------------------------- *)
fun treeDelete compareKey dkey tree = case tree of
E => raise Bug "Metis_Map.delete: element not found"
| T node => nodeDelete compareKey dkey node
and nodeDelete compareKey dkey node = let val Node {size,priority,left,key,value,right} = node in case compareKey (dkey,key) of
LESS => let valsize = size - 1 and left = treeDelete compareKey dkey left
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
T node end
| EQUAL => treeAppend left right
| GREATER => let valsize = size - 1 and right = treeDelete compareKey dkey right
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
T node end end;
(* ------------------------------------------------------------------------- *) (* Partial map is the basic operation for preserving tree structure. *) (* It applies its argument function to the elements *in order*. *) (* ------------------------------------------------------------------------- *)
fun treeMapPartial f tree = case tree of
E => E
| T node => nodeMapPartial f node
and nodeMapPartial f (Node {priority,left,key,value,right,...}) = let val left = treeMapPartial f left and vo = f (key,value) and right = treeMapPartial f right in case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right end;
fun treeMap f tree = case tree of
E => E
| T node => T (nodeMap f node)
and nodeMap f node = let val Node {size,priority,left,key,value,right} = node
val left = treeMap f left and value = f (key,value) and right = treeMap f right in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} end;
(* ------------------------------------------------------------------------- *) (* Merge is the basic operation for joining two trees. Note that the merged *) (* key is always the one from the second map. *) (* ------------------------------------------------------------------------- *)
fun treeMerge compareKey f1 f2 fb tree1 tree2 = case tree1 of
E => treeMapPartial f2 tree2
| T node1 => case tree2 of
E => treeMapPartial f1 tree1
| T node2 => nodeMerge compareKey f1 f2 fb node1 node2
and nodeMerge compareKey f1 f2 fb node1 node2 = let val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition compareKey key node1
val left = treeMerge compareKey f1 f2 fb l left and right = treeMerge compareKey f1 f2 fb r right
val vo = case kvo of
NONE => f2 (key,value)
| SOME kv => fb (kv,(key,value)) in case vo of
NONE => treeAppend left right
| SOME value => let val node = mkNodeSingleton priority key value in
treeCombine left node right end end;
(* ------------------------------------------------------------------------- *) (* A union operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeUnion compareKey f f2 tree1 tree2 = case tree1 of
E => tree2
| T node1 => case tree2 of
E => tree1
| T node2 => nodeUnion compareKey f f2 node1 node2
and nodeUnion compareKey f f2 node1 node2 = if pointerEqual (node1,node2) then nodeMapPartial f2 node1 else let val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition compareKey key node1
val left = treeUnion compareKey f f2 l left and right = treeUnion compareKey f f2 r right
val vo = case kvo of
NONE => SOME value
| SOME kv => f (kv,(key,value)) in case vo of
NONE => treeAppend left right
| SOME value => let val node = mkNodeSingleton priority key value in
treeCombine left node right end end;
(* ------------------------------------------------------------------------- *) (* An intersect operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeIntersect compareKey f t1 t2 = case t1 of
E => E
| T n1 => case t2 of
E => E
| T n2 => nodeIntersect compareKey f n1 n2
and nodeIntersect compareKey f n1 n2 = let val Node {priority,left,key,value,right,...} = n2
val (l,kvo,r) = nodePartition compareKey key n1
val left = treeIntersect compareKey f l left and right = treeIntersect compareKey f r right
val vo = case kvo of
NONE => NONE
| SOME kv => f (kv,(key,value)) in case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right end;
(* ------------------------------------------------------------------------- *) (* A union operation on trees which simply chooses the second value. *) (* ------------------------------------------------------------------------- *)
fun treeUnionDomain compareKey tree1 tree2 = case tree1 of
E => tree2
| T node1 => case tree2 of
E => tree1
| T node2 => if pointerEqual (node1,node2) then tree2 else nodeUnionDomain compareKey node1 node2
and nodeUnionDomain compareKey node1 node2 = let val Node {priority,left,key,value,right,...} = node2
val (l,_,r) = nodePartition compareKey key node1
val left = treeUnionDomain compareKey l left and right = treeUnionDomain compareKey r right
val node = mkNodeSingleton priority key value in
treeCombine left node right end;
(* ------------------------------------------------------------------------- *) (* An intersect operation on trees which simply chooses the second value. *) (* ------------------------------------------------------------------------- *)
fun treeIntersectDomain compareKey tree1 tree2 = case tree1 of
E => E
| T node1 => case tree2 of
E => E
| T node2 => if pointerEqual (node1,node2) then tree2 else nodeIntersectDomain compareKey node1 node2
and nodeIntersectDomain compareKey node1 node2 = let val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition compareKey key node1
val left = treeIntersectDomain compareKey l left and right = treeIntersectDomain compareKey r right in ifOption.isSome kvo then mkTree priority left key value right else treeAppend left right end;
(* ------------------------------------------------------------------------- *) (* A difference operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeDifferenceDomain compareKey t1 t2 = case t1 of
E => E
| T n1 => case t2 of
E => t1
| T n2 => nodeDifferenceDomain compareKey n1 n2
and nodeDifferenceDomain compareKey n1 n2 = if pointerEqual (n1,n2) then E else let val Node {priority,left,key,value,right,...} = n1
val (l,kvo,r) = nodePartition compareKey key n2
val left = treeDifferenceDomain compareKey left l and right = treeDifferenceDomain compareKey right r in ifOption.isSome kvo then treeAppend left right else mkTree priority left key value right end;
(* ------------------------------------------------------------------------- *) (* A subset operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeSubsetDomain compareKey tree1 tree2 = case tree1 of
E => true
| T node1 => case tree2 of
E => false
| T node2 => nodeSubsetDomain compareKey node1 node2
and nodeSubsetDomain compareKey node1 node2 =
pointerEqual (node1,node2) orelse let val Node {size,left,key,right,...} = node1 in size <= nodeSize node2 andalso let val (l,kvo,r) = nodePartition compareKey key node2 in Option.isSome kvo andalso
treeSubsetDomain compareKey left l andalso
treeSubsetDomain compareKey right r end end;
(* ------------------------------------------------------------------------- *) (* Picking an arbitrary key/value pair from a tree. *) (* ------------------------------------------------------------------------- *)
fun nodePick node = let val Node {key,value,...} = node in
(key,value) end;
fun treePick tree = case tree of
E => raise Bug "Metis_Map.treePick"
| T node => nodePick node;
(* ------------------------------------------------------------------------- *) (* Removing an arbitrary key/value pair from a tree. *) (* ------------------------------------------------------------------------- *)
fun nodeDeletePick node = let val Node {left,key,value,right,...} = node in
((key,value), treeAppend left right) end;
fun treeDeletePick tree = case tree of
E => raise Bug "Metis_Map.treeDeletePick"
| T node => nodeDeletePick node;
(* ------------------------------------------------------------------------- *) (* Finding the nth smallest key/value (counting from 0). *) (* ------------------------------------------------------------------------- *)
fun treeNth n tree = case tree of
E => raise Bug "Metis_Map.treeNth"
| T node => nodeNth n node
and nodeNth n node = let val Node {left,key,value,right,...} = node
val k = treeSize left in if n = k then (key,value) elseif n < k then treeNth n left else treeNth (n - (k + 1)) right end;
(* ------------------------------------------------------------------------- *) (* Removing the nth smallest key/value (counting from 0). *) (* ------------------------------------------------------------------------- *)
fun treeDeleteNth n tree = case tree of
E => raise Bug "Metis_Map.treeDeleteNth"
| T node => nodeDeleteNth n node
and nodeDeleteNth n node = let val Node {size,priority,left,key,value,right} = node
val k = treeSize left in if n = k then ((key,value), treeAppend left right) elseif n < k then let val (key_value,left) = treeDeleteNth n left
valsize = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
(key_value, T node) end else let val n = n - (k + 1)
val (key_value,right) = treeDeleteNth n right
valsize = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
(key_value, T node) end end;
datatype ('key,'value) iterator =
LeftToRightIterator of
('key * 'value) * ('key,'value) tree * ('key,'value) node list
| RightToLeftIterator of
('key * 'value) * ('key,'value) tree * ('key,'value) node list;
fun fromSpineLeftToRightIterator nodes = case nodes of
[] => NONE
| Node {key,value,right,...} :: nodes =>
SOME (LeftToRightIterator ((key,value),right,nodes));
fun fromSpineRightToLeftIterator nodes = case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
SOME (RightToLeftIterator ((key,value),left,nodes));
fun addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);
fun addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);
fun treeMkIterator tree = addLeftToRightIterator [] tree;
fun treeMkRevIterator tree = addRightToLeftIterator [] tree;
fun readIterator iter = case iter of
LeftToRightIterator (key_value,_,_) => key_value
| RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter = case iter of
LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
| RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io = case io of
NONE => acc
| SOME iter => let val (key,value) = readIterator iter in
foldIterator f (f (key,value,acc)) (advanceIterator iter) end;
fun findIterator pred io = case io of
NONE => NONE
| SOME iter => let val key_value = readIterator iter in if pred key_value then SOME key_value else findIterator pred (advanceIterator iter) end;
fun firstIterator f io = case io of
NONE => NONE
| SOME iter => let val key_value = readIterator iter in case f key_value of
NONE => firstIterator f (advanceIterator iter)
| s => s end;
fun compareIterator compareKey compareValue io1 io2 = case (io1,io2) of
(NONE,NONE) => EQUAL
| (NONE, SOME _) => LESS
| (SOME _, NONE) => GREATER
| (SOME i1, SOME i2) => let val (k1,v1) = readIterator i1 and (k2,v2) = readIterator i2 in case compareKey (k1,k2) of
LESS => LESS
| EQUAL =>
(case compareValue (v1,v2) of
LESS => LESS
| EQUAL => let val io1 = advanceIterator i1 and io2 = advanceIterator i2 in
compareIterator compareKey compareValue io1 io2 end
| GREATER => GREATER)
| GREATER => GREATER end;
fun equalIterator equalKey equalValue io1 io2 = case (io1,io2) of
(NONE,NONE) => true
| (NONE, SOME _) => false
| (SOME _, NONE) => false
| (SOME i1, SOME i2) => let val (k1,v1) = readIterator i1 and (k2,v2) = readIterator i2 in
equalKey k1 k2 andalso
equalValue v1 v2 andalso let val io1 = advanceIterator i1 and io2 = advanceIterator i2 in
equalIterator equalKey equalValue io1 io2 end end;
(* ------------------------------------------------------------------------- *) (* A type of finite maps. *) (* ------------------------------------------------------------------------- *)
fun delete (Metis_Map (compareKey,tree)) dkey = let val tree = treeDelete compareKey dkey tree in
Metis_Map (compareKey,tree) end;
(*BasicDebug val delete = fn m => fn k => checkInvariants "Metis_Map.delete: result" (delete (checkInvariants "Metis_Map.delete: input" m) k);
*)
fun remove m key = if inDomain key m then delete m key else m;
fun deletePick (Metis_Map (compareKey,tree)) = let val (key_value,tree) = treeDeletePick tree in
(key_value, Metis_Map (compareKey,tree)) end;
(*BasicDebug val deletePick = fn m => let val (kv,m) = deletePick (checkInvariants "Metis_Map.deletePick: input" m) in (kv, checkInvariants "Metis_Map.deletePick: result" m) end;
*)
fun deleteNth (Metis_Map (compareKey,tree)) n = let val (key_value,tree) = treeDeleteNth n tree in
(key_value, Metis_Map (compareKey,tree)) end;
(*BasicDebug val deleteNth = fn m => fn n => let val (kv,m) = deleteNth (checkInvariants "Metis_Map.deleteNth: input" m) n in (kv, checkInvariants "Metis_Map.deleteNth: result" m) end;
*)
fun deleteRandom m = let val n = size m in if n = 0 thenraise Bug "Metis_Map.deleteRandom: empty" else deleteNth m (randomInt n) end;
(* ------------------------------------------------------------------------- *) (* Joining (all join operations prefer keys in the second map). *) (* ------------------------------------------------------------------------- *)
fun merge {first,second,both} (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) = let val tree = treeMerge compareKey first second both tree1 tree2 in
Metis_Map (compareKey,tree) end;
(*BasicDebug val merge = fn f => fn m1 => fn m2 => checkInvariants "Metis_Map.merge: result" (merge f (checkInvariants "Metis_Map.merge: input 1" m1) (checkInvariants "Metis_Map.merge: input 2" m2));
*)
fun union f (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) = let fun f2 kv = f (kv,kv)
val tree = treeUnion compareKey f f2 tree1 tree2 in
Metis_Map (compareKey,tree) end;
(*BasicDebug val union = fn f => fn m1 => fn m2 => checkInvariants "Metis_Map.union: result" (union f (checkInvariants "Metis_Map.union: input 1" m1) (checkInvariants "Metis_Map.union: input 2" m2));
*)
fun intersect f (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) = let val tree = treeIntersect compareKey f tree1 tree2 in
Metis_Map (compareKey,tree) end;
(*BasicDebug val intersect = fn f => fn m1 => fn m2 => checkInvariants "Metis_Map.intersect: result" (intersect f (checkInvariants "Metis_Map.intersect: input 1" m1) (checkInvariants "Metis_Map.intersect: input 2" m2));
*)
fun mapPartial f (Metis_Map (compareKey,tree)) = let val tree = treeMapPartial f tree in
Metis_Map (compareKey,tree) end;
(*BasicDebug val mapPartial = fn f => fn m => checkInvariants "Metis_Map.mapPartial: result" (mapPartial f (checkInvariants "Metis_Map.mapPartial: input" m));
*)
funmap f (Metis_Map (compareKey,tree)) = let val tree = treeMap f tree in
Metis_Map (compareKey,tree) end;
(*BasicDebug val map = fn f => fn m => checkInvariants "Metis_Map.map: result" (map f (checkInvariants "Metis_Map.map: input" m));
*)
fun transform f = map (fn (_,value) => f value);
funfilter pred = let fun f (key_value as (_,value)) = if pred key_value then SOME value else NONE in
mapPartial f end;
fun partition p = let fun np x = not (p x) in
fn m => (filter p m, filter np m) end;
fun foldl f b m = foldIterator f b (mkIterator m);
fun foldr f b m = foldIterator f b (mkRevIterator m);
funapp f m = foldl (fn (key,value,()) => f (key,value)) () m;
fun compare compareValue (m1,m2) = if pointerEqual (m1,m2) then EQUAL else case Int.compare (size m1, size m2) of
LESS => LESS
| EQUAL => let val Metis_Map (compareKey,_) = m1
val io1 = mkIterator m1 and io2 = mkIterator m2 in
compareIterator compareKey compareValue io1 io2 end
| GREATER => GREATER;
fun equal equalValue m1 m2 =
pointerEqual (m1,m2) orelse
(size m1 = size m2 andalso let val Metis_Map (compareKey,_) = m1
val io1 = mkIterator m1 and io2 = mkIterator m2 in
equalIterator (equalKey compareKey) equalValue io1 io2 end);
(* ------------------------------------------------------------------------- *) (* Metis_Set operations on the domain. *) (* ------------------------------------------------------------------------- *)
fun unionDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) = let val tree = treeUnionDomain compareKey tree1 tree2 in
Metis_Map (compareKey,tree) end;
local fun uncurriedUnionDomain (m,acc) = unionDomain acc m; in fun unionListDomain ms = case ms of
[] => raise Bug "Metis_Map.unionListDomain: no sets"
| m :: ms => List.foldl uncurriedUnionDomain m ms; end;
fun intersectDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) = let val tree = treeIntersectDomain compareKey tree1 tree2 in
Metis_Map (compareKey,tree) end;
local fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m; in fun intersectListDomain ms = case ms of
[] => raise Bug "Metis_Map.intersectListDomain: no sets"
| m :: ms => List.foldl uncurriedIntersectDomain m ms; end;
fun differenceDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) = let val tree = treeDifferenceDomain compareKey tree1 tree2 in
Metis_Map (compareKey,tree) end;
fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
fun values m = foldr (fn (_,value,l) => value :: l) [] m;
fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
fun fromList compareKey l = let val m = new compareKey in
insertList m l end;
fun toString m = "<" ^ (if null m then""else Int.toString (size m)) ^ ">";
end
(**** Original file: src/KeyMap.sig ****)
(* ========================================================================= *) (* FINITE MAPS WITH A FIXED KEY TYPE *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_KeyMap = sig
(* ------------------------------------------------------------------------- *) (* A type of map keys. *) (* ------------------------------------------------------------------------- *)
type key
val compareKey : key * key -> order
val equalKey : key -> key -> bool
(* ------------------------------------------------------------------------- *) (* A type of finite maps. *) (* ------------------------------------------------------------------------- *)
val compare : ('a * 'a -> order) -> 'a map * 'a map -> order
val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
val advanceIterator : 'a iterator -> 'a iterator option
end
(**** Original file: src/KeyMap.sml ****)
(* ========================================================================= *) (* FINITE MAPS WITH A FIXED KEY TYPE *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
functor Metis_KeyMap (Key : Metis_Ordered) :> Metis_KeyMap where type key = Key.t = struct
(* ------------------------------------------------------------------------- *) (* Importing from the input signature. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* Converting a comparison function to an equality function. *) (* ------------------------------------------------------------------------- *)
fun equalKey key1 key2 = compareKey (key1,key2) = EQUAL;
and'value node =
Node of
{size : int,
priority : priority,
left : 'value tree,
key : key,
value : 'value,
right : 'value tree};
fun lowerPriorityNode node1 node2 = let val Node {priority = p1, ...} = node1 and Node {priority = p2, ...} = node2 in
comparePriority (p1,p2) = LESS end;
(*BasicDebug local fun checkSizes tree = case tree of E => 0 | T (Node {size,left,right,...}) => let val l = checkSizes left and r = checkSizes right
val () = if l + 1 + r = size then () else raise Bug "wrong size" in size end;
fun checkSorted x tree = case tree of E => x | T (Node {left,key,right,...}) => let val x = checkSorted x left
val () = case x of NONE => () | SOME k => case compareKey (k,key) of LESS => () | EQUAL => raise Bug "duplicate keys" | GREATER => raise Bug "unsorted"
val x = SOME key in checkSorted x right end;
fun checkPriorities tree = case tree of E => NONE | T node => let val Node {left,right,...} = node
val () = case checkPriorities left of NONE => () | SOME lnode => if not (lowerPriorityNode node lnode) then () else raise Bug "left child has greater priority"
val () = case checkPriorities right of NONE => () | SOME rnode => if not (lowerPriorityNode node rnode) then () else raise Bug "right child has greater priority" in SOME node end; in fun treeCheckInvariants tree = let val _ = checkSizes tree
val _ = checkSorted NONE tree
val _ = checkPriorities tree in tree end handle Error err => raise Bug err; end;
*)
(* ------------------------------------------------------------------------- *) (* Tree operations. *) (* ------------------------------------------------------------------------- *)
fun treeNew () = E;
fun nodeSize (Node {size = x, ...}) = x;
fun treeSize tree = case tree of
E => 0
| T x => nodeSize x;
fun mkNode priority left key value right = let valsize = treeSize left + 1 + treeSize right in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} end;
fun mkTree priority left key value right = let val node = mkNode priority left key value right in
T node end;
(* ------------------------------------------------------------------------- *) (* Extracting the left and right spines of a tree. *) (* ------------------------------------------------------------------------- *)
fun treeLeftSpine acc tree = case tree of
E => acc
| T node => nodeLeftSpine acc node
and nodeLeftSpine acc node = let val Node {left,...} = node in
treeLeftSpine (node :: acc) left end;
fun treeRightSpine acc tree = case tree of
E => acc
| T node => nodeRightSpine acc node
and nodeRightSpine acc node = let val Node {right,...} = node in
treeRightSpine (node :: acc) right end;
fun mkNodeSingleton priority key value = let valsize = 1 and left = E and right = E in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} end;
fun nodeSingleton (key,value) = let val priority = randomPriority () in
mkNodeSingleton priority key value end;
fun treeSingleton key_value = let val node = nodeSingleton key_value in
T node end;
(* ------------------------------------------------------------------------- *) (* Appending two trees, where every element of the first tree is less than *) (* every element of the second tree. *) (* ------------------------------------------------------------------------- *)
fun treeAppend tree1 tree2 = case tree1 of
E => tree2
| T node1 => case tree2 of
E => tree1
| T node2 => if lowerPriorityNode node1 node2 then let val Node {priority,left,key,value,right,...} = node2
val left = treeAppend tree1 left in
mkTree priority left key value right end else let val Node {priority,left,key,value,right,...} = node1
val right = treeAppend right tree2 in
mkTree priority left key value right end;
(* ------------------------------------------------------------------------- *) (* Appending two trees and a node, where every element of the first tree is *) (* less than the node, which in turn is less than every element of the *) (* second tree. *) (* ------------------------------------------------------------------------- *)
fun treeCombine left node right = let val left_node = treeAppend left (T node) in
treeAppend left_node right end;
(* ------------------------------------------------------------------------- *) (* Searching a tree for a value. *) (* ------------------------------------------------------------------------- *)
fun treePeek pkey tree = case tree of
E => NONE
| T node => nodePeek pkey node
and nodePeek pkey node = let val Node {left,key,value,right,...} = node in case compareKey (pkey,key) of
LESS => treePeek pkey left
| EQUAL => SOME value
| GREATER => treePeek pkey right end;
(* ------------------------------------------------------------------------- *) (* Tree paths. *) (* ------------------------------------------------------------------------- *)
(* Generating a path by searching a tree for a key/value pair *)
fun treePeekPath pkey path tree = case tree of
E => (path,NONE)
| T node => nodePeekPath pkey path node
and nodePeekPath pkey path node = let val Node {left,key,right,...} = node in case compareKey (pkey,key) of
LESS => treePeekPath pkey ((true,node) :: path) left
| EQUAL => (path, SOME node)
| GREATER => treePeekPath pkey ((false,node) :: path) right end;
(* A path splits a tree into left/right components *)
fun addSidePath ((wentLeft,node),(leftTree,rightTree)) = let val Node {priority,left,key,value,right,...} = node in if wentLeft then (leftTree, mkTree priority rightTree key value right) else (mkTree priority left key value leftTree, rightTree) end;
fun addSidesPath left_right = List.foldl addSidePath left_right;
fun mkSidesPath path = addSidesPath (E,E) path;
(* Updating the subtree at a path *)
local fun updateTree ((wentLeft,node),tree) = let val Node {priority,left,key,value,right,...} = node in if wentLeft then mkTree priority tree key value right else mkTree priority left key value tree end; in fun updateTreePath tree = List.foldl updateTree tree; end;
(* Inserting a new node at a path position *)
fun insertNodePath node = let fun insert left_right path = case path of
[] => let val (left,right) = left_right in
treeCombine left node right end
| (step as (_,snode)) :: rest => if lowerPriorityNode snode node then let val left_right = addSidePath (step,left_right) in
insert left_right rest end else let val (left,right) = left_right
val tree = treeCombine left node right in
updateTreePath tree path end in
insert (E,E) end;
(* ------------------------------------------------------------------------- *) (* Using a key to split a node into three components: the keys comparing *) (* less than the supplied key, an optional equal key, and the keys comparing *) (* greater. *) (* ------------------------------------------------------------------------- *)
fun nodePartition pkey node = let val (path,pnode) = nodePeekPath pkey [] node in case pnode of
NONE => let val (left,right) = mkSidesPath path in
(left,NONE,right) end
| SOME node => let val Node {left,key,value,right,...} = node
val (left,right) = addSidesPath (left,right) path in
(left, SOME (key,value), right) end end;
(* ------------------------------------------------------------------------- *) (* Searching a tree for a key/value pair. *) (* ------------------------------------------------------------------------- *)
fun treePeekKey pkey tree = case tree of
E => NONE
| T node => nodePeekKey pkey node
and nodePeekKey pkey node = let val Node {left,key,value,right,...} = node in case compareKey (pkey,key) of
LESS => treePeekKey pkey left
| EQUAL => SOME (key,value)
| GREATER => treePeekKey pkey right end;
(* ------------------------------------------------------------------------- *) (* Inserting new key/values into the tree. *) (* ------------------------------------------------------------------------- *)
fun treeInsert key_value tree = let val (key,value) = key_value
val (path,inode) = treePeekPath key [] tree in case inode of
NONE => let val node = nodeSingleton (key,value) in
insertNodePath node path end
| SOME node => let val Node {size,priority,left,right,...} = node
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
updateTreePath (T node) path end end;
(* ------------------------------------------------------------------------- *) (* Deleting key/value pairs: it raises an exception if the supplied key is *) (* not present. *) (* ------------------------------------------------------------------------- *)
fun treeDelete dkey tree = case tree of
E => raise Bug "Metis_KeyMap.delete: element not found"
| T node => nodeDelete dkey node
and nodeDelete dkey node = let val Node {size,priority,left,key,value,right} = node in case compareKey (dkey,key) of
LESS => let valsize = size - 1 and left = treeDelete dkey left
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
T node end
| EQUAL => treeAppend left right
| GREATER => let valsize = size - 1 and right = treeDelete dkey right
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
T node end end;
(* ------------------------------------------------------------------------- *) (* Partial map is the basic operation for preserving tree structure. *) (* It applies its argument function to the elements *in order*. *) (* ------------------------------------------------------------------------- *)
fun treeMapPartial f tree = case tree of
E => E
| T node => nodeMapPartial f node
and nodeMapPartial f (Node {priority,left,key,value,right,...}) = let val left = treeMapPartial f left and vo = f (key,value) and right = treeMapPartial f right in case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right end;
fun treeMap f tree = case tree of
E => E
| T node => T (nodeMap f node)
and nodeMap f node = let val Node {size,priority,left,key,value,right} = node
val left = treeMap f left and value = f (key,value) and right = treeMap f right in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} end;
(* ------------------------------------------------------------------------- *) (* Merge is the basic operation for joining two trees. Note that the merged *) (* key is always the one from the second map. *) (* ------------------------------------------------------------------------- *)
fun treeMerge f1 f2 fb tree1 tree2 = case tree1 of
E => treeMapPartial f2 tree2
| T node1 => case tree2 of
E => treeMapPartial f1 tree1
| T node2 => nodeMerge f1 f2 fb node1 node2
and nodeMerge f1 f2 fb node1 node2 = let val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition key node1
val left = treeMerge f1 f2 fb l left and right = treeMerge f1 f2 fb r right
val vo = case kvo of
NONE => f2 (key,value)
| SOME kv => fb (kv,(key,value)) in case vo of
NONE => treeAppend left right
| SOME value => let val node = mkNodeSingleton priority key value in
treeCombine left node right end end;
(* ------------------------------------------------------------------------- *) (* A union operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeUnion f f2 tree1 tree2 = case tree1 of
E => tree2
| T node1 => case tree2 of
E => tree1
| T node2 => nodeUnion f f2 node1 node2
and nodeUnion f f2 node1 node2 = if pointerEqual (node1,node2) then nodeMapPartial f2 node1 else let val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition key node1
val left = treeUnion f f2 l left and right = treeUnion f f2 r right
val vo = case kvo of
NONE => SOME value
| SOME kv => f (kv,(key,value)) in case vo of
NONE => treeAppend left right
| SOME value => let val node = mkNodeSingleton priority key value in
treeCombine left node right end end;
(* ------------------------------------------------------------------------- *) (* An intersect operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeIntersect f t1 t2 = case t1 of
E => E
| T n1 => case t2 of
E => E
| T n2 => nodeIntersect f n1 n2
and nodeIntersect f n1 n2 = let val Node {priority,left,key,value,right,...} = n2
val (l,kvo,r) = nodePartition key n1
val left = treeIntersect f l left and right = treeIntersect f r right
val vo = case kvo of
NONE => NONE
| SOME kv => f (kv,(key,value)) in case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right end;
(* ------------------------------------------------------------------------- *) (* A union operation on trees which simply chooses the second value. *) (* ------------------------------------------------------------------------- *)
fun treeUnionDomain tree1 tree2 = case tree1 of
E => tree2
| T node1 => case tree2 of
E => tree1
| T node2 => if pointerEqual (node1,node2) then tree2 else nodeUnionDomain node1 node2
and nodeUnionDomain node1 node2 = let val Node {priority,left,key,value,right,...} = node2
val (l,_,r) = nodePartition key node1
val left = treeUnionDomain l left and right = treeUnionDomain r right
val node = mkNodeSingleton priority key value in
treeCombine left node right end;
(* ------------------------------------------------------------------------- *) (* An intersect operation on trees which simply chooses the second value. *) (* ------------------------------------------------------------------------- *)
fun treeIntersectDomain tree1 tree2 = case tree1 of
E => E
| T node1 => case tree2 of
E => E
| T node2 => if pointerEqual (node1,node2) then tree2 else nodeIntersectDomain node1 node2
and nodeIntersectDomain node1 node2 = let val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition key node1
val left = treeIntersectDomain l left and right = treeIntersectDomain r right in ifOption.isSome kvo then mkTree priority left key value right else treeAppend left right end;
(* ------------------------------------------------------------------------- *) (* A difference operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeDifferenceDomain t1 t2 = case t1 of
E => E
| T n1 => case t2 of
E => t1
| T n2 => nodeDifferenceDomain n1 n2
and nodeDifferenceDomain n1 n2 = if pointerEqual (n1,n2) then E else let val Node {priority,left,key,value,right,...} = n1
val (l,kvo,r) = nodePartition key n2
val left = treeDifferenceDomain left l and right = treeDifferenceDomain right r in ifOption.isSome kvo then treeAppend left right else mkTree priority left key value right end;
(* ------------------------------------------------------------------------- *) (* A subset operation on trees. *) (* ------------------------------------------------------------------------- *)
fun treeSubsetDomain tree1 tree2 = case tree1 of
E => true
| T node1 => case tree2 of
E => false
| T node2 => nodeSubsetDomain node1 node2
and nodeSubsetDomain node1 node2 =
pointerEqual (node1,node2) orelse let val Node {size,left,key,right,...} = node1 in size <= nodeSize node2 andalso let val (l,kvo,r) = nodePartition key node2 in Option.isSome kvo andalso
treeSubsetDomain left l andalso
treeSubsetDomain right r end end;
(* ------------------------------------------------------------------------- *) (* Picking an arbitrary key/value pair from a tree. *) (* ------------------------------------------------------------------------- *)
fun nodePick node = let val Node {key,value,...} = node in
(key,value) end;
fun treePick tree = case tree of
E => raise Bug "Metis_KeyMap.treePick"
| T node => nodePick node;
(* ------------------------------------------------------------------------- *) (* Removing an arbitrary key/value pair from a tree. *) (* ------------------------------------------------------------------------- *)
fun nodeDeletePick node = let val Node {left,key,value,right,...} = node in
((key,value), treeAppend left right) end;
fun treeDeletePick tree = case tree of
E => raise Bug "Metis_KeyMap.treeDeletePick"
| T node => nodeDeletePick node;
(* ------------------------------------------------------------------------- *) (* Finding the nth smallest key/value (counting from 0). *) (* ------------------------------------------------------------------------- *)
fun treeNth n tree = case tree of
E => raise Bug "Metis_KeyMap.treeNth"
| T node => nodeNth n node
and nodeNth n node = let val Node {left,key,value,right,...} = node
val k = treeSize left in if n = k then (key,value) elseif n < k then treeNth n left else treeNth (n - (k + 1)) right end;
(* ------------------------------------------------------------------------- *) (* Removing the nth smallest key/value (counting from 0). *) (* ------------------------------------------------------------------------- *)
fun treeDeleteNth n tree = case tree of
E => raise Bug "Metis_KeyMap.treeDeleteNth"
| T node => nodeDeleteNth n node
and nodeDeleteNth n node = let val Node {size,priority,left,key,value,right} = node
val k = treeSize left in if n = k then ((key,value), treeAppend left right) elseif n < k then let val (key_value,left) = treeDeleteNth n left
valsize = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
(key_value, T node) end else let val n = n - (k + 1)
val (key_value,right) = treeDeleteNth n right
valsize = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right} in
(key_value, T node) end end;
datatype'value iterator =
LeftToRightIterator of
(key * 'value) * 'value tree * 'value node list
| RightToLeftIterator of
(key * 'value) * 'value tree * 'value node list;
fun fromSpineLeftToRightIterator nodes = case nodes of
[] => NONE
| Node {key,value,right,...} :: nodes =>
SOME (LeftToRightIterator ((key,value),right,nodes));
fun fromSpineRightToLeftIterator nodes = case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
SOME (RightToLeftIterator ((key,value),left,nodes));
fun addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);
fun addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);
fun treeMkIterator tree = addLeftToRightIterator [] tree;
fun treeMkRevIterator tree = addRightToLeftIterator [] tree;
fun readIterator iter = case iter of
LeftToRightIterator (key_value,_,_) => key_value
| RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter = case iter of
LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
| RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io = case io of
NONE => acc
| SOME iter => let val (key,value) = readIterator iter in
foldIterator f (f (key,value,acc)) (advanceIterator iter) end;
fun findIterator pred io = case io of
NONE => NONE
| SOME iter => let val key_value = readIterator iter in if pred key_value then SOME key_value else findIterator pred (advanceIterator iter) end;
fun firstIterator f io = case io of
NONE => NONE
| SOME iter => let val key_value = readIterator iter in case f key_value of
NONE => firstIterator f (advanceIterator iter)
| s => s end;
fun compareIterator compareValue io1 io2 = case (io1,io2) of
(NONE,NONE) => EQUAL
| (NONE, SOME _) => LESS
| (SOME _, NONE) => GREATER
| (SOME i1, SOME i2) => let val (k1,v1) = readIterator i1 and (k2,v2) = readIterator i2 in case compareKey (k1,k2) of
LESS => LESS
| EQUAL =>
(case compareValue (v1,v2) of
LESS => LESS
| EQUAL => let val io1 = advanceIterator i1 and io2 = advanceIterator i2 in
compareIterator compareValue io1 io2 end
| GREATER => GREATER)
| GREATER => GREATER end;
fun equalIterator equalValue io1 io2 = case (io1,io2) of
(NONE,NONE) => true
| (NONE, SOME _) => false
| (SOME _, NONE) => false
| (SOME i1, SOME i2) => let val (k1,v1) = readIterator i1 and (k2,v2) = readIterator i2 in
equalKey k1 k2 andalso
equalValue v1 v2 andalso let val io1 = advanceIterator i1 and io2 = advanceIterator i2 in
equalIterator equalValue io1 io2 end end;
(* ------------------------------------------------------------------------- *) (* A type of finite maps. *) (* ------------------------------------------------------------------------- *)
fun delete (Metis_Map tree) dkey = let val tree = treeDelete dkey tree in
Metis_Map tree end;
(*BasicDebug val delete = fn m => fn k => checkInvariants "Metis_KeyMap.delete: result" (delete (checkInvariants "Metis_KeyMap.delete: input" m) k);
*)
fun remove m key = if inDomain key m then delete m key else m;
fun deletePick (Metis_Map tree) = let val (key_value,tree) = treeDeletePick tree in
(key_value, Metis_Map tree) end;
(*BasicDebug val deletePick = fn m => let val (kv,m) = deletePick (checkInvariants "Metis_KeyMap.deletePick: input" m) in (kv, checkInvariants "Metis_KeyMap.deletePick: result" m) end;
*)
fun deleteNth (Metis_Map tree) n = let val (key_value,tree) = treeDeleteNth n tree in
(key_value, Metis_Map tree) end;
(*BasicDebug val deleteNth = fn m => fn n => let val (kv,m) = deleteNth (checkInvariants "Metis_KeyMap.deleteNth: input" m) n in (kv, checkInvariants "Metis_KeyMap.deleteNth: result" m) end;
*)
fun deleteRandom m = let val n = size m in if n = 0 thenraise Bug "Metis_KeyMap.deleteRandom: empty" else deleteNth m (randomInt n) end;
(* ------------------------------------------------------------------------- *) (* Joining (all join operations prefer keys in the second map). *) (* ------------------------------------------------------------------------- *)
fun merge {first,second,both} (Metis_Map tree1) (Metis_Map tree2) = let val tree = treeMerge first second both tree1 tree2 in
Metis_Map tree end;
(*BasicDebug val merge = fn f => fn m1 => fn m2 => checkInvariants "Metis_KeyMap.merge: result" (merge f (checkInvariants "Metis_KeyMap.merge: input 1" m1) (checkInvariants "Metis_KeyMap.merge: input 2" m2));
*)
fun union f (Metis_Map tree1) (Metis_Map tree2) = let fun f2 kv = f (kv,kv)
val tree = treeUnion f f2 tree1 tree2 in
Metis_Map tree end;
(*BasicDebug val union = fn f => fn m1 => fn m2 => checkInvariants "Metis_KeyMap.union: result" (union f (checkInvariants "Metis_KeyMap.union: input 1" m1) (checkInvariants "Metis_KeyMap.union: input 2" m2));
*)
fun intersect f (Metis_Map tree1) (Metis_Map tree2) = let val tree = treeIntersect f tree1 tree2 in
Metis_Map tree end;
(*BasicDebug val intersect = fn f => fn m1 => fn m2 => checkInvariants "Metis_KeyMap.intersect: result" (intersect f (checkInvariants "Metis_KeyMap.intersect: input 1" m1) (checkInvariants "Metis_KeyMap.intersect: input 2" m2));
*)
fun mapPartial f (Metis_Map tree) = let val tree = treeMapPartial f tree in
Metis_Map tree end;
(*BasicDebug val mapPartial = fn f => fn m => checkInvariants "Metis_KeyMap.mapPartial: result" (mapPartial f (checkInvariants "Metis_KeyMap.mapPartial: input" m));
*)
funmap f (Metis_Map tree) = let val tree = treeMap f tree in
Metis_Map tree end;
(*BasicDebug val map = fn f => fn m => checkInvariants "Metis_KeyMap.map: result" (map f (checkInvariants "Metis_KeyMap.map: input" m));
*)
fun transform f = map (fn (_,value) => f value);
funfilter pred = let fun f (key_value as (_,value)) = if pred key_value then SOME value else NONE in
mapPartial f end;
fun partition p = let fun np x = not (p x) in
fn m => (filter p m, filter np m) end;
fun foldl f b m = foldIterator f b (mkIterator m);
fun foldr f b m = foldIterator f b (mkRevIterator m);
funapp f m = foldl (fn (key,value,()) => f (key,value)) () m;
fun compare compareValue (m1,m2) = if pointerEqual (m1,m2) then EQUAL else case Int.compare (size m1, size m2) of
LESS => LESS
| EQUAL => let val Metis_Map _ = m1
val io1 = mkIterator m1 and io2 = mkIterator m2 in
compareIterator compareValue io1 io2 end
| GREATER => GREATER;
fun equal equalValue m1 m2 =
pointerEqual (m1,m2) orelse
(size m1 = size m2 andalso let val Metis_Map _ = m1
val io1 = mkIterator m1 and io2 = mkIterator m2 in
equalIterator equalValue io1 io2 end);
(* ------------------------------------------------------------------------- *) (* Metis_Set operations on the domain. *) (* ------------------------------------------------------------------------- *)
fun unionDomain (Metis_Map tree1) (Metis_Map tree2) = let val tree = treeUnionDomain tree1 tree2 in
Metis_Map tree end;
local fun uncurriedUnionDomain (m,acc) = unionDomain acc m; in fun unionListDomain ms = case ms of
[] => raise Bug "Metis_KeyMap.unionListDomain: no sets"
| m :: ms => List.foldl uncurriedUnionDomain m ms; end;
fun intersectDomain (Metis_Map tree1) (Metis_Map tree2) = let val tree = treeIntersectDomain tree1 tree2 in
Metis_Map tree end;
local fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m; in fun intersectListDomain ms = case ms of
[] => raise Bug "Metis_KeyMap.intersectListDomain: no sets"
| m :: ms => List.foldl uncurriedIntersectDomain m ms; end;
fun differenceDomain (Metis_Map tree1) (Metis_Map tree2) = let val tree = treeDifferenceDomain tree1 tree2 in
Metis_Map tree end;
fun subsetDomain (Metis_Map tree1) (Metis_Map tree2) =
treeSubsetDomain tree1 tree2;
fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
fun values m = foldr (fn (_,value,l) => value :: l) [] m;
fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
fun fromList l = let val m = new () in
insertList m l end;
(* ========================================================================= *) (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Set = sig
(* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
val transform : ('elt -> 'a) -> 'elt set -> 'a list
val toList : 'elt set -> 'elt list
val fromList : ('elt * 'elt -> order) -> 'elt list -> 'elt set
(* ------------------------------------------------------------------------- *) (* Converting to and from maps. *) (* ------------------------------------------------------------------------- *)
type ('elt,'a) map = ('elt,'a) Metis_Map.map
val mapPartial : ('elt -> 'a option) -> 'elt set -> ('elt,'a) map
val mkRevIterator : 'elt set -> 'elt iterator option
val readIterator : 'elt iterator -> 'elt
val advanceIterator : 'elt iterator -> 'elt iterator option
end
(**** Original file: src/Set.sml ****)
(* ========================================================================= *) (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Set :> Metis_Set = struct
(* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *)
type ('elt,'a) map = ('elt,'a) Metis_Map.map;
datatype'elt set = Metis_Set of ('elt,unit) map;
(* ------------------------------------------------------------------------- *) (* Converting to and from maps. *) (* ------------------------------------------------------------------------- *)
fun dest (Metis_Set m) = m;
fun mapPartial f = let fun mf (elt,()) = f elt in
fn Metis_Set m => Metis_Map.mapPartial mf m end;
funmap f = let fun mf (elt,()) = f elt in
fn Metis_Set m => Metis_Map.map mf m end;
fun domain m = Metis_Set (Metis_Map.transform (fn _ => ()) m);
funfilter pred = let fun mpred (elt,()) = pred elt in
fn Metis_Set m => Metis_Set (Metis_Map.filter mpred m) end;
fun partition pred = let fun mpred (elt,()) = pred elt in
fn Metis_Set m => let val (m1,m2) = Metis_Map.partition mpred m in
(Metis_Set m1, Metis_Set m2) end end;
funapp f = let fun mf (elt,()) = f elt in
fn Metis_Set m => Metis_Map.app mf m end;
fun foldl f = let fun mf (elt,(),acc) = f (elt,acc) in
fn acc => fn Metis_Set m => Metis_Map.foldl mf acc m end;
fun foldr f = let fun mf (elt,(),acc) = f (elt,acc) in
fn acc => fn Metis_Set m => Metis_Map.foldr mf acc m end;
fun subset (Metis_Set m1) (Metis_Set m2) = Metis_Map.subsetDomain m1 m2;
fun disjoint (Metis_Set m1) (Metis_Set m2) = Metis_Map.disjointDomain m1 m2;
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
fun transform f = let fun inc (x,l) = f x :: l in
foldr inc [] end;
fun mkIterator (Metis_Set m) = Metis_Map.mkIterator m;
fun mkRevIterator (Metis_Set m) = Metis_Map.mkRevIterator m;
fun readIterator iter = let val (elt,()) = Metis_Map.readIterator iter in
elt end;
fun advanceIterator iter = Metis_Map.advanceIterator iter;
end
(**** Original file: src/ElementSet.sig ****)
(* ========================================================================= *) (* FINITE SETS WITH A FIXED ELEMENT TYPE *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_ElementSet = sig
(* ------------------------------------------------------------------------- *) (* A type of set elements. *) (* ------------------------------------------------------------------------- *)
type element
val compareElement : element * element -> order
val equalElement : element -> element -> bool
(* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *)
val closedAdd : (element -> set) -> set -> set -> set
val close : (element -> set) -> set -> set
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
val transform : (element -> 'a) -> set -> 'a list
val toList : set -> element list
val fromList : element list -> set
(* ------------------------------------------------------------------------- *) (* Converting to and from maps. *) (* ------------------------------------------------------------------------- *)
type'a map
val mapPartial : (element -> 'a option) -> set -> 'a map
(* ========================================================================= *) (* FINITE SETS WITH A FIXED ELEMENT TYPE *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
functor Metis_ElementSet (
KM : Metis_KeyMap
) :> Metis_ElementSet
where type element = KM.key andtype'a map = 'a KM.map = struct
(* ------------------------------------------------------------------------- *) (* A type of set elements. *) (* ------------------------------------------------------------------------- *)
type element = KM.key;
val compareElement = KM.compareKey;
val equalElement = KM.equalKey;
(* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *)
type'a map = 'a KM.map;
datatypeset = Metis_Set of unit map;
(* ------------------------------------------------------------------------- *) (* Converting to and from maps. *) (* ------------------------------------------------------------------------- *)
fun dest (Metis_Set m) = m;
fun mapPartial f = let fun mf (elt,()) = f elt in
fn Metis_Set m => KM.mapPartial mf m end;
funmap f = let fun mf (elt,()) = f elt in
fn Metis_Set m => KM.map mf m end;
fun domain m = Metis_Set (KM.transform (fn _ => ()) m);
funfilter pred = let fun mpred (elt,()) = pred elt in
fn Metis_Set m => Metis_Set (KM.filter mpred m) end;
fun partition pred = let fun mpred (elt,()) = pred elt in
fn Metis_Set m => let val (m1,m2) = KM.partition mpred m in
(Metis_Set m1, Metis_Set m2) end end;
funapp f = let fun mf (elt,()) = f elt in
fn Metis_Set m => KM.app mf m end;
fun foldl f = let fun mf (elt,(),acc) = f (elt,acc) in
fn acc => fn Metis_Set m => KM.foldl mf acc m end;
fun foldr f = let fun mf (elt,(),acc) = f (elt,acc) in
fn acc => fn Metis_Set m => KM.foldr mf acc m end;
fun lift f = let fun inc (elt,set) = union set (f elt) in
foldl inc empty end;
fun closedAdd f = let fun adds acc set = foldl check acc set
and check (elt,acc) = if member elt acc then acc else expand (add acc elt) elt
and expand acc elt = adds acc (f elt) in
adds end;
fun close f = closedAdd f empty;
(* ------------------------------------------------------------------------- *) (* Converting to and from lists. *) (* ------------------------------------------------------------------------- *)
fun transform f = let fun inc (x,l) = f x :: l in
foldr inc [] end;
datatype ordering =
Linear of element list
| Cycle of element list;
fun postOrdered children = let fun check acc elts = case elts of
[] => true
| elt :: elts => not (member elt acc) andalso let val acc = closedAdd children acc (singleton elt) in
check acc elts end in
check empty end;
fun preOrdered children elts = postOrdered children (List.rev elts);
local fun takeStackset elt = let fun notElement (e,_,_) = not (equalElement e elt) in
Metis_Useful.takeWhile notElement end;
fun consElement ((e,_,_),el) = e :: el;
fun depthFirstSearch children = let fun traverse (dealt,dealtset) (stack,stackset) work = case work of
[] =>
(case stack of
[] => Linear dealt
| (elt,work,stackset) :: stack => let val dealt = elt :: dealt
val dealtset = add dealtset elt in
traverse (dealt,dealtset) (stack,stackset) work end)
| elt :: work => if member elt dealtset then
traverse (dealt,dealtset) (stack,stackset) work elseif member elt stackset then let val cycle = takeStackset elt stack
val cycle = elt :: List.foldl consElement [elt] cycle in
Cycle cycle end else let val stack = (elt,work,stackset) :: stack
val stackset = add stackset elt
val work = toList (children elt) in
traverse (dealt,dealtset) (stack,stackset) work end
val dealt = [] and dealtset = empty and stack = [] and stackset = empty in
traverse (dealt,dealtset) (stack,stackset) end; in fun preOrder children roots = let val result = depthFirstSearch children (toList roots)
(*BasicDebug val () = case result of Cycle _ => () | Linear l => let val () = if subset roots (fromList l) then () else raise Metis_Useful.Bug "Metis_ElementSet.preOrder: missing roots"
val () = if preOrdered children l then () else raise Metis_Useful.Bug "Metis_ElementSet.preOrder: bad ordering" in () end
*) in
result end;
fun postOrder children roots = case depthFirstSearch children (toList roots) of
Linear l => let val l = List.rev l
(*BasicDebug val () = if subset roots (fromList l) then () else raise Metis_Useful.Bug "Metis_ElementSet.postOrder: missing roots"
val () = if postOrdered children l then () else raise Metis_Useful.Bug "Metis_ElementSet.postOrder: bad ordering"
*) in
Linear l end
| cycle => cycle; end;
fun postOrderedSCC children = let fun check acc eltsl = case eltsl of
[] => true
| elts :: eltsl => not (null elts) andalso
disjoint elts acc andalso let fun addElt elt = closedAdd children acc (singleton elt)
val (root,elts) = deletePick elts
fun checkElt elt = member root (addElt elt) in all checkElt elts andalso let val acc = addElt root in
subset elts acc andalso
check acc eltsl end end in
check empty end;
fun preOrderedSCC children eltsl = postOrderedSCC children (List.rev eltsl);
fun inStack elt (StackSCC (elts,_)) = member elt elts;
fun popStack root = let fun pop scc eltl = case eltl of
[] => raise Metis_Useful.Bug "Metis_ElementSet.popStack"
| (elt,elts) :: eltl => let val scc = add scc elt in if equalElement elt root then (scc, StackSCC (elts,eltl)) else pop scc eltl end in
fn sccs => fn StackSCC (_,eltl) => let val (scc,stack) = pop empty eltl in
(scc :: sccs, stack) end end;
fun getIndex indices e : int = case KM.peek indices e of
SOME i => i
| NONE => raise Metis_Useful.Bug "Metis_ElementSet.getIndex";
fun isRoot indices lows e = getIndex indices e = getIndex lows e;
fun reduceIndex indices (e,i) = let val j = getIndex indices e in if j <= i then indices else KM.insert indices (e,i) end;
fun tarjan children = let fun dfsVertex sccs callstack index indices lows stack elt = let val indices = KM.insert indices (elt,index) and lows = KM.insert lows (elt,index)
val index = index + 1
val stack = pushStack stack elt
val chil = toList (children elt) in
dfsSuccessors sccs callstack index indices lows stack elt chil end
and dfsSuccessors sccs callstack index indices lows stack elt chil = case chil of
[] => let val (sccs,stack) = if isRoot indices lows elt then popStack elt sccs stack else (sccs,stack) in case callstack of
[] => (sccs,index,indices,lows)
| (p,elts) :: callstack => let val lows = reduceIndex lows (p, getIndex lows elt) in
dfsSuccessors sccs callstack index indices lows stack p elts end end
| c :: chil => case KM.peek indices c of
NONE => let val callstack = (elt,chil) :: callstack in
dfsVertex sccs callstack index indices lows stack c end
| SOME cind => let val lows = if inStack c stack then reduceIndex lows (elt,cind) else lows in
dfsSuccessors sccs callstack index indices lows stack elt chil end
fun dfsRoots sccs index indices lows elts = case elts of
[] => sccs
| elt :: elts => if KM.inDomain elt indices then
dfsRoots sccs index indices lows elts else let val callstack = []
val (sccs,index,indices,lows) =
dfsVertex sccs callstack index indices lows emptyStack elt in
dfsRoots sccs index indices lows elts end
val sccs = [] and index = 0 and indices = KM.new () and lows = KM.new () in
dfsRoots sccs index indices lows end; in fun preOrderSCC children roots = let val result = tarjan children (toList roots)
(*BasicDebug val () = if subset roots (unionList result) then () else raise Metis_Useful.Bug "Metis_ElementSet.preOrderSCC: missing roots"
val () = if preOrderedSCC children result then () else raise Metis_Useful.Bug "Metis_ElementSet.preOrderSCC: bad ordering"
*) in
result end;
fun postOrderSCC children roots = let val result = List.rev (tarjan children (toList roots))
(*BasicDebug val () = if subset roots (unionList result) then () else raise Metis_Useful.Bug "Metis_ElementSet.postOrderSCC: missing roots"
val () = if postOrderedSCC children result then () else raise Metis_Useful.Bug "Metis_ElementSet.postOrderSCC: bad ordering"
*) in
result end; end;
(* ========================================================================= *) (* PRESERVING SHARING OF ML VALUES *) (* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
(* ========================================================================= *) (* PRESERVING SHARING OF ML VALUES *) (* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
fun mapOption f xo = case xo of
SOME x => let val y = f x in if x == y then xo else SOME y end
| NONE => xo;
fun mapsOption f xo acc = case xo of
SOME x => let val (y,acc) = f x acc in if x == y then (xo,acc) else (SOME y, acc) end
| NONE => (xo,acc);
(* ------------------------------------------------------------------------- *) (* List operations. *) (* ------------------------------------------------------------------------- *)
funmap f = let fun m ys ys_xs xs = case xs of
[] => List.revAppend ys_xs
| x :: xs => let val y = f x val ys = y :: ys val ys_xs = if x == y then ys_xs else (ys,xs) in
m ys ys_xs xs end in
fn xs => m [] ([],xs) xs end;
fun maps f = let fun m acc ys ys_xs xs = case xs of
[] => (List.revAppend ys_xs, acc)
| x :: xs => let val (y,acc) = f x acc val ys = y :: ys val ys_xs = if x == y then ys_xs else (ys,xs) in
m acc ys ys_xs xs end in
fn xs => fn acc => m acc [] ([],xs) xs end;
local fun revTails acc xs = case xs of
[] => acc
| x :: xs' => revTails ((x,xs) :: acc) xs'; in fun revMap f = let fun m ys same xxss = case xxss of
[] => ys
| (x,xs) :: xxss => let val y = f x val same = same andalso x == y val ys = if same then xs else y :: ys in
m ys same xxss end in
fn xs => m [] true (revTails [] xs) end;
fun revMaps f = let fun m acc ys same xxss = case xxss of
[] => (ys,acc)
| (x,xs) :: xxss => let val (y,acc) = f x acc val same = same andalso x == y val ys = if same then xs else y :: ys in
m acc ys same xxss end in
fn xs => fn acc => m acc [] true (revTails [] xs) end; end;
fun updateNth (n,x) l = let val (a,b) = Metis_Useful.revDivide l n in case b of
[] => raise Subscript
| h :: t => if x == h then l elseList.revAppend (a, x :: t) end;
fun setify l = let val l' = Metis_Useful.setify l in if length l' = length l then l else l' end;
(* ------------------------------------------------------------------------- *) (* Function caching. *) (* ------------------------------------------------------------------------- *)
fun cache cmp f = let val cache = Unsynchronized.ref (Metis_Map.new cmp) in
fn a => case Metis_Map.peek (!cache) a of
SOME b => b
| NONE => let val b = f a val () = cache := Metis_Map.insert (!cache) (a,b) in
b end end;
(* ========================================================================= *) (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
(* ------------------------------------------------------------------------- *) (* Metis_Stream versions of standard list operations: these should all terminate. *) (* ------------------------------------------------------------------------- *)
val cons : 'a -> (unit -> 'a stream) -> 'a stream
val null : 'a stream -> bool
val hd : 'a stream -> 'a (* raises Empty *)
val tl : 'a stream -> 'a stream (* raises Empty *)
val hdTl : 'a stream -> 'a * 'a stream (* raises Empty *)
val singleton : 'a -> 'a stream
val append : 'a stream -> (unit -> 'a stream) -> 'a stream
val zipwith : ('a -> 'b -> 'c) -> 'a stream -> 'b stream -> 'c stream
val zip : 'a stream -> 'b stream -> ('a * 'b) stream
val take : int -> 'a stream -> 'a stream (* raises Subscript *)
val drop : int -> 'a stream -> 'a stream (* raises Subscript *)
val unfold : ('b -> ('a * 'b) option) -> 'b -> 'a stream
(* ------------------------------------------------------------------------- *) (* Metis_Stream versions of standard list operations: these might not terminate. *) (* ------------------------------------------------------------------------- *)
val length : 'a stream -> int
valexists : ('a -> bool) -> 'a stream -> bool
valall : ('a -> bool) -> 'a stream -> bool
valfilter : ('a -> bool) -> 'a stream -> 'a stream
val foldl : ('a * 's -> 's) -> 's -> 'a stream -> 's
val concat : 'a stream stream -> 'a stream
val mapPartial : ('a -> 'b option) -> 'a stream -> 'b stream
val toTextFile : {filename : string} -> string stream -> unit
val fromTextFile : {filename : string} -> string stream (* line by line *)
end
(**** Original file: src/Stream.sml ****)
(* ========================================================================= *) (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
fun repeat x = letfun rep () = Cons (x,rep) in rep () end;
fun count n = Cons (n, fn () => count (n + 1));
fun funpows f x = Cons (x, fn () => funpows f (f x));
(* ------------------------------------------------------------------------- *) (* Metis_Stream versions of standard list operations: these should all terminate. *) (* ------------------------------------------------------------------------- *)
fun cons h t = Cons (h,t);
fun null Nil = true
| null (Cons _) = false;
fun hd Nil = raise Empty
| hd (Cons (h,_)) = h;
fun tl Nil = raise Empty
| tl (Cons (_,t)) = t ();
fun hdTl s = (hd s, tl s);
fun singleton s = Cons (s, K Nil);
fun append Nil s = s ()
| append (Cons (h,t)) s = Cons (h, fn () => append (t ()) s);
funmap f = let fun m Nil = Nil
| m (Cons (h,t)) = Cons (f h, m o t) in
m end;
fun maps f g = let fun mm s Nil = g s
| mm s (Cons (x,xs)) = let val (y,s') = f x s in
Cons (y, mm s' o xs) end in
mm end;
fun zipwith f = let fun z Nil _ = Nil
| z _ Nil = Nil
| z (Cons (x,xs)) (Cons (y,ys)) =
Cons (f x y, fn () => z (xs ()) (ys ())) in
z end;
fun zip s t = zipwith pair s t;
fun take 0 _ = Nil
| take n Nil = raise Subscript
| take 1 (Cons (x,_)) = Cons (x, K Nil)
| take n (Cons (x,xs)) = Cons (x, fn () => take (n - 1) (xs ()));
fun drop n s = funpow n tl s handle Empty => raise Subscript;
fun unfold f = let fun next b () = case f b of
NONE => Nil
| SOME (a,b) => Cons (a, next b) in
fn b => next b () end;
(* ------------------------------------------------------------------------- *) (* Metis_Stream versions of standard list operations: these might not terminate. *) (* ------------------------------------------------------------------------- *)
local fun len n Nil = n
| len n (Cons (_,t)) = len (n + 1) (t ()); in fun length s = len 0 s; end;
funexists pred = let fun f Nil = false
| f (Cons (h,t)) = pred h orelse f (t ()) in
f end;
funall pred = not o exists (not o pred);
funfilter p Nil = Nil
| filter p (Cons (x,xs)) = if p x then Cons (x, fn () => filter p (xs ())) elsefilter p (xs ());
fun foldl f = let fun fold b Nil = b
| fold b (Cons (h,t)) = fold (f (h,b)) (t ()) in
fold end;
fun mapPartial f = let fun mp Nil = Nil
| mp (Cons (h,t)) = case f h of
NONE => mp (t ())
| SOME h' => Cons (h', fn () => mp (t ())) in
mp end;
fun mapsPartial f g = let fun mp s Nil = g s
| mp s (Cons (h,t)) = let val (h,s) = f h s in case h of
NONE => mp s (t ())
| SOME h => Cons (h, fn () => mp s (t ())) end in
mp end;
fun mapConcat f = let fun mc Nil = Nil
| mc (Cons (h,t)) = append (f h) (fn () => mc (t ())) in
mc end;
fun mapsConcat f g = let fun mc s Nil = g s
| mc s (Cons (h,t)) = let val (l,s) = f h s in
append l (fn () => mc s (t ())) end in
mc end;
fun fromTextFile {filename = f} = let val (h,close) = if f = "-"then (TextIO.stdIn, K ()) else (TextIO.openIn f, TextIO.closeIn)
fun strm () = case TextIO.inputLine h of
NONE => (close h; Nil)
| SOME s => Cons (s,strm) in
memoize (strm ()) end;
end
(**** Original file: src/Heap.sig ****)
(* ========================================================================= *) (* A HEAP DATATYPE FOR ML *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Heap = sig
type'a heap
val new : ('a * 'a -> order) -> 'a heap
val add : 'a heap -> 'a -> 'a heap
val null : 'a heap -> bool
val top : 'a heap -> 'a (* raises Empty *)
val remove : 'a heap -> 'a * 'a heap (* raises Empty *)
valsize : 'a heap -> int
valapp : ('a -> unit) -> 'a heap -> unit
val toList : 'a heap -> 'a list
val toStream : 'a heap -> 'a Metis_Stream.stream
val toString : 'a heap -> string
end
(**** Original file: src/Heap.sml ****)
(* ========================================================================= *) (* A HEAP DATATYPE FOR ML *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Heap :> Metis_Heap = struct
(* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)
datatype'a node = E | T of int * 'a * 'a node * 'a node;
datatype'a heap = Metis_Heap of ('a * 'a -> order) * int * 'a node;
fun rank E = 0
| rank (T (r,_,_,_)) = r;
fun makeT (x,a,b) = if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a);
fun merge cmp = let fun mrg (h,E) = h
| mrg (E,h) = h
| mrg (h1 as T (_,x,a1,b1), h2 as T (_,y,a2,b2)) = case cmp (x,y) of
GREATER => makeT (y, a2, mrg (h1,b2))
| _ => makeT (x, a1, mrg (b1,h2)) in
mrg end;
fun new cmp = Metis_Heap (cmp,0,E);
fun add (Metis_Heap (f,n,a)) x = Metis_Heap (f, n + 1, merge f (T (1,x,E,E), a));
funsize (Metis_Heap (_, n, _)) = n;
fun null h = size h = 0;
fun top (Metis_Heap (_,_,E)) = raise Empty
| top (Metis_Heap (_, _, T (_,x,_,_))) = x;
fun remove (Metis_Heap (_,_,E)) = raise Empty
| remove (Metis_Heap (f, n, T (_,x,a,b))) = (x, Metis_Heap (f, n - 1, merge f (a,b)));
funapp f = let fun ap [] = ()
| ap (E :: rest) = ap rest
| ap (T (_,d,a,b) :: rest) = (f d; ap (a :: b :: rest)) in
fn Metis_Heap (_,_,a) => ap [a] end;
fun toList h = if null h then [] else let val (x,h) = remove h in
x :: toList h end;
fun toStream h = if null h then Metis_Stream.Nil else let val (x,h) = remove h in
Metis_Stream.Cons (x, fn () => toStream h) end;
fun toString h = "Metis_Heap[" ^ (if null h then""else Int.toString (size h)) ^ "]";
end
(**** Original file: src/Print.sig ****)
(* ========================================================================= *) (* PRETTY-PRINTING *) (* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
(* ------------------------------------------------------------------------- *) (* A type of pretty-printers. *) (* ------------------------------------------------------------------------- *)
type ppstream
type'a pp = 'a -> ppstream
val skip : ppstream
val sequence : ppstream -> ppstream -> ppstream
val duplicate : int -> ppstream -> ppstream
val program : ppstream list -> ppstream
val stream : ppstream Metis_Stream.stream -> ppstream
val consistentBlock : int -> ppstream list -> ppstream
val inconsistentBlock : int -> ppstream list -> ppstream
(* ------------------------------------------------------------------------- *) (* Words are unbreakable strings annotated with their effective size. *) (* ------------------------------------------------------------------------- *)
datatype word = Word of {word : string, size : int}
val mkWord : string -> word
val emptyWord : word
val charWord : char -> word
val ppWord : word pp
val space : ppstream
val spaces : int -> ppstream
(* ------------------------------------------------------------------------- *) (* Possible line breaks. *) (* ------------------------------------------------------------------------- *)
val render :
{lineLength : int option} -> ppstream ->
{indent : int, line : string} Metis_Stream.stream
val toStringWithLineLength :
{lineLength : int option} -> 'a pp -> 'a -> string
val toStreamWithLineLength :
{lineLength : int option} -> 'a pp -> 'a -> string Metis_Stream.stream
val toLine : 'a pp -> 'a -> string
(* ------------------------------------------------------------------------- *) (* Pretty-printer rendering with a global line length. *) (* ------------------------------------------------------------------------- *)
val lineLength : int Unsynchronized.ref
val toString : 'a pp -> 'a -> string
val toStream : 'a pp -> 'a -> string Metis_Stream.stream
val trace : 'a pp -> string -> 'a -> unit
end
(**** Original file: src/Print.sml ****)
(* ========================================================================= *) (* PRETTY-PRINTING *) (* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
fun revAppend xs s = case xs of
[] => s ()
| x :: xs => revAppend xs (K (Metis_Stream.Cons (x,s)));
fun revConcat strm = case strm of
Metis_Stream.Nil => Metis_Stream.Nil
| Metis_Stream.Cons (h,t) => revAppend h (fn () => revConcat (t ()));
local fun calcSpaces n = nChars #" " n;
val cacheSize = 2 * initialLineLength;
val cachedSpaces = Vector.tabulate (cacheSize,calcSpaces); in fun nSpaces n = if n < cacheSize then Vector.sub (cachedSpaces,n) else calcSpaces n; end;
fun escapeString {escape} = let val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
fun escapeChar c = case c of
#"\\" => "\\\\"
| #"\n" => "\\n"
| #"\t" => "\\t"
| _ => caseList.find (equal c o fst) escapeMap of
SOME (_,s) => s
| NONE => str c in String.translate escapeChar end;
fun isConsistentBlock block = isConsistentStyle (styleBlock block);
fun isInconsistentBlock block = isInconsistentStyle (styleBlock block);
(* ------------------------------------------------------------------------- *) (* Words are unbreakable strings annotated with their effective size. *) (* ------------------------------------------------------------------------- *)
datatype word = Word of {word : string, size : int};
fun mkWord s = Word {word = s, size = String.size s};
val emptyWord = mkWord "";
fun charWord c = mkWord (str c);
fun spacesWord i = Word {word = nSpaces i, size = i};
fun sizeWord (Word {size = x, ...}) = x;
fun renderWord (Word {word = x, ...}) = x;
(* ------------------------------------------------------------------------- *) (* Possible line breaks. *) (* ------------------------------------------------------------------------- *)
fun mkBreak n = Break {size = n, extraIndent = 0};
fun sizeBreak (Break {size = x, ...}) = x;
fun extraIndentBreak (Break {extraIndent = x, ...}) = x;
fun renderBreak b = nSpaces (sizeBreak b);
fun updateSizeBreak size break = let val Break {size = _, extraIndent} = break in
Break
{size = size,
extraIndent = extraIndent} end;
fun appendBreak break1 break2 = let (*BasicDebug val () = warn "merging consecutive pretty-printing breaks"
*) val Break {size = size1, extraIndent = extraIndent1} = break1 and Break {size = size2, extraIndent = extraIndent2} = break2
valsize = size1 + size2 and extraIndent = Int.max (extraIndent1,extraIndent2) in
Break
{size = size,
extraIndent = extraIndent} end;
(* ------------------------------------------------------------------------- *) (* A type of pretty-printers. *) (* ------------------------------------------------------------------------- *)
datatype step =
BeginBlock of block
| EndBlock
| AddWord of word
| AddBreak of break
| AddNewline;
type ppstream = step Metis_Stream.stream;
type'a pp = 'a -> ppstream;
fun toStringStep step = case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
| AddWord _ => "Word"
| AddBreak _ => "Break"
| AddNewline => "Newline";
local fun dup pp n () = if n = 1 then pp else Metis_Stream.append pp (dup pp (n - 1)); in fun duplicate n pp : ppstream = let (*BasicDebug val () = if 0 <= n then () else raise Bug "Metis_Print.duplicate"
*) in if n = 0 then skip else dup pp n () end; end;
val program : ppstream list -> ppstream = Metis_Stream.concatList;
val stream : ppstream Metis_Stream.stream -> ppstream = Metis_Stream.concat;
local fun beginBlock b = Metis_Stream.singleton (BeginBlock b);
val endBlock = Metis_Stream.singleton EndBlock; in fun block b pp = program [beginBlock b, pp, endBlock]; end;
fun consistentBlock i pps = block (mkConsistentBlock i) (program pps);
fun inconsistentBlock i pps = block (mkInconsistentBlock i) (program pps);
(* ------------------------------------------------------------------------- *) (* Words are unbreakable strings annotated with their effective size. *) (* ------------------------------------------------------------------------- *)
fun ppWord w = Metis_Stream.singleton (AddWord w);
val space = ppWord (mkWord " ");
fun spaces i = ppWord (spacesWord i);
(* ------------------------------------------------------------------------- *) (* Possible line breaks. *) (* ------------------------------------------------------------------------- *)
fun ppBreak b = Metis_Stream.singleton (AddBreak b);
fun ppBracket' l r ppA a = let val n = sizeWord l in
inconsistentBlock n
[ppWord l,
ppA a,
ppWord r] end;
fun ppOp' w = sequence (ppWord w) break;
fun ppOp2' ab ppA ppB (a,b) =
inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b];
fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b,
ppOp' bc,
ppC c];
fun ppOpList' s ppA = let fun ppOpA a = sequence (ppOp' s) (ppA a) in
fn [] => skip
| h :: t => inconsistentBlock 0 (ppA h :: List.map ppOpA t) end;
fun ppOpStream' s ppA = let fun ppOpA a = sequence (ppOp' s) (ppA a) in
fn Metis_Stream.Nil => skip
| Metis_Stream.Cons (h,t) =>
inconsistentBlock 0
[ppA h,
Metis_Stream.concat (Metis_Stream.map ppOpA (t ()))] end;
fun ppBracket l r = ppBracket' (mkWord l) (mkWord r);
fun ppOp s = ppOp' (mkWord s);
fun ppOp2 ab = ppOp2' (mkWord ab);
fun ppOp3 ab bc = ppOp3' (mkWord ab) (mkWord bc);
fun ppOpList s = ppOpList' (mkWord s);
fun ppOpStream s = ppOpStream' (mkWord s);
(* ------------------------------------------------------------------------- *) (* Pretty-printers for common types. *) (* ------------------------------------------------------------------------- *)
fun ppChar c = ppWord (charWord c);
fun ppString s = ppWord (mkWord s);
fun ppEscapeString escape = ppMap (escapeString escape) ppString;
local val pp = ppString "()"; in fun ppUnit () = pp; end;
local val ppTrue = ppString "true" and ppFalse = ppString "false"; in fun ppBool b = if b then ppTrue else ppFalse; end;
val ppInt = ppMap Int.toString ppString;
local val ppNeg = ppString "~" and ppSep = ppString "," and ppZero = ppString "0" and ppZeroZero = ppString "00";
fun ppIntBlock i = if i < 10 then sequence ppZeroZero (ppInt i) elseif i < 100 then sequence ppZero (ppInt i) else ppInt i;
fun ppIntBlocks i = if i < 1000 then ppInt i else sequence (ppIntBlocks (i div 1000))
(sequence ppSep (ppIntBlock (i mod 1000))); in fun ppPrettyInt i = if i < 0 then sequence ppNeg (ppIntBlocks (~i)) else ppIntBlocks i; end;
val ppReal = ppMap Real.toString ppString;
val ppPercent = ppMap percentToString ppString;
local val ppLess = ppString "Less" and ppEqual = ppString "Equal" and ppGreater = ppString "Greater"; in fun ppOrder ord = caseordof
LESS => ppLess
| EQUAL => ppEqual
| GREATER => ppGreater; end;
local val left = mkWord "[" and right = mkWord "]" and sep = mkWord ","; in fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;
fun ppStream ppX xs = ppBracket' left right (ppOpStream' sep ppX) xs; end;
local val ppNone = ppString "-"; in fun ppOption ppX xo = case xo of
SOME x => ppX x
| NONE => ppNone; end;
local val left = mkWord "(" and right = mkWord ")" and sep = mkWord ","; in fun ppPair ppA ppB =
ppBracket' left right (ppOp2' sep ppA ppB);
fun ppTriple ppA ppB ppC =
ppBracket' left right (ppOp3' sep sep ppA ppB ppC); end;
fun ppException e = ppString (exnMessage e);
(* ------------------------------------------------------------------------- *) (* A type of pretty-printers. *) (* ------------------------------------------------------------------------- *)
local val ppStepType = ppMap toStringStep ppString;
val ppStyle = ppMap toStringStyle ppString;
val ppBlockInfo = let val sep = mkWord " " in
fn Block {style = s, indent = i} =>
program [ppStyle s, ppWord sep, ppInt i] end;
val ppWordInfo = let val left = mkWord "\"" and right = mkWord "\"" and escape = {escape = [#"\""]}
val pp = ppBracket' left right (ppEscapeString escape) in
fn Word {word = s, size = n} => ifsize s = n then pp s else ppPair pp ppInt (s,n) end;
val ppBreakInfo = let val sep = mkWord "+" in
fn Break {size = n, extraIndent = k} => if k = 0 then ppInt n else program [ppInt n, ppWord sep, ppInt k] end;
fun ppStep step =
inconsistentBlock 2
(ppStepType step ::
(case step of
BeginBlock b =>
[break,
ppBlockInfo b]
| EndBlock => []
| AddWord w =>
[break,
ppWordInfo w]
| AddBreak b =>
[break,
ppBreakInfo b]
| AddNewline => [])); in val ppPpstream = ppStream ppStep; end;
local fun comparePrecedence (io1,io2) = let val {token = _, precedence = p1, assoc = _} = io1 and {token = _, precedence = p2, assoc = _} = io2 in
Int.compare (p2,p1) end;
fun equalAssoc a a' = case a of
LeftAssoc => (case a' of LeftAssoc => true | _ => false)
| NonAssoc => (case a' of NonAssoc => true | _ => false)
| RightAssoc => (case a' of RightAssoc => true | _ => false);
fun new t a acc = {tokens = Metis_StringSet.singleton t, assoc = a} :: acc;
fun add t a' acc = case acc of
[] => raise Bug "Metis_Print.layerInfixes: null"
| {tokens = ts, assoc = a} :: acc => if equalAssoc a a' then {tokens = Metis_StringSet.add ts t, assoc = a} :: acc elseraise Bug "Metis_Print.layerInfixes: mixed assocs";
fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) = let val acc = if p = p' then add t a acc else new t a acc in
(acc,p) end; in fun layerInfixes (Infixes ios) = case sort comparePrecedence ios of
[] => []
| {token = t, precedence = p, assoc = a} :: ios => let val acc = new t a []
val (acc,_) = List.foldl layer (acc,p) ios in
acc end; end;
local fun add ({tokens = ts, assoc = _}, tokens) = Metis_StringSet.union ts tokens; in fun tokensLayeredInfixes l = List.foldl add Metis_StringSet.empty l; end;
fun tokensInfixes ios = tokensLayeredInfixes (layerInfixes ios);
fun destInfixOp dest tokens tm = case dest tm of
NONE => NONE
| s as SOME (t,a,b) => if Metis_StringSet.member t tokens then s else NONE;
fun ppLayeredInfixes dest ppTok {tokens,assoc} ppLower ppSub = let fun isLayer t = Metis_StringSet.member t tokens
fun ppTerm aligned (tm,r) = case dest tm of
NONE => ppSub (tm,r)
| SOME (t,a,b) => if aligned andalso isLayer t then ppLayer (tm,t,a,b,r) else ppLower (tm,t,a,b,r)
and ppLeft tm_r = let val aligned = case assoc of LeftAssoc => true | _ => false in
ppTerm aligned tm_r end
and ppLayer (tm,t,a,b,r) =
program
[ppLeft (a,true),
ppTok (tm,t),
ppRight (b,r)]
and ppRight tm_r = let val aligned = case assoc of RightAssoc => true | _ => false in
ppTerm aligned tm_r end in
fn tm_t_a_b_r as (_,t,_,_,_) => if isLayer t then inconsistentBlock 0 [ppLayer tm_t_a_b_r] else ppLower tm_t_a_b_r end;
local val leftBrack = mkWord "(" and rightBrack = mkWord ")"; in fun ppInfixes ops = let val layers = layerInfixes ops
val toks = tokensLayeredInfixes layers in
fn dest => fn ppTok => fn ppSub => let fun destOp tm = destInfixOp dest toks tm
fun ppInfix tm_t_a_b_r = ppLayers layers tm_t_a_b_r
and ppLayers ls (tm,t,a,b,r) = case ls of
[] =>
ppBracket' leftBrack rightBrack ppInfix (tm,t,a,b,false)
| l :: ls => let val ppLower = ppLayers ls in
ppLayeredInfixes destOp ppTok l ppLower ppSub (tm,t,a,b,r) end in
fn (tm,r) => case destOp tm of
SOME (t,a,b) => ppInfix (tm,t,a,b,r)
| NONE => ppSub (tm,r) end end; end;
(* ------------------------------------------------------------------------- *) (* A type of output lines. *) (* ------------------------------------------------------------------------- *)
type line = {indent : int, line : string};
val emptyLine = let val indent = 0 and line = "" in
{indent = indent,
line = line} end;
fun addEmptyLine lines = emptyLine :: lines;
fun addLine lines indent line = {indent = indent, line = line} :: lines;
datatype state =
State of
{lineIndent : int,
lineSize : int,
stack : frame list};
fun blockFrame (Frame {block = x, ...}) = x;
fun brokenFrame (Frame {broken = x, ...}) = x;
fun indentFrame (Frame {indent = x, ...}) = x;
fun sizeFrame (Frame {size = x, ...}) = x;
fun chunksFrame (Frame {chunks = x, ...}) = x;
fun styleFrame frame = styleBlock (blockFrame frame);
fun isConsistentFrame frame = isConsistentBlock (blockFrame frame);
fun breakingFrame frame = isConsistentFrame frame andalso brokenFrame frame;
fun sizeChunk chunk = case chunk of
WordChunk w => sizeWord w
| BreakChunk b => sizeBreak b
| FrameChunk f => sizeFrame f;
local fun add (c,acc) = sizeChunk c + acc; in fun sizeChunks cs = List.foldl add 0 cs; end;
local fun flattenChunks acc chunks = case chunks of
[] => acc
| chunk :: chunks => flattenChunk acc chunk chunks
and flattenChunk acc chunk chunks = case chunk of
WordChunk w => flattenChunks (renderWord w :: acc) chunks
| BreakChunk b => flattenChunks (renderBreak b :: acc) chunks
| FrameChunk f => flattenFrame acc f chunks
and flattenFrame acc frame chunks =
flattenChunks acc (chunksFrame frame @ chunks); in fun renderChunks chunks = String.concat (flattenChunks [] chunks); end;
local fun add baseIndent ((extraIndent,chunks),lines) =
addChunksLine lines (baseIndent + extraIndent) chunks; in fun addIndentChunksLines lines baseIndent indent_chunks = List.foldl (add baseIndent) lines indent_chunks; end;
fun isEmptyFrame frame = let val chunks = chunksFrame frame
val empty = List.null chunks
(*BasicDebug val () = if not empty orelse sizeFrame frame = 0 then () else raise Bug "Metis_Print.isEmptyFrame: bad size"
*) in
empty end;
local fun breakInconsistent blockIndent = let fun break chunks = case chunks of
[] => NONE
| chunk :: chunks => case chunk of
BreakChunk b => let val pre = chunks and indent = blockIndent + extraIndentBreak b and post = [] in
SOME (pre,indent,post) end
| _ => case break chunks of
SOME (pre,indent,post) => let val post = chunk :: post in
SOME (pre,indent,post) end
| NONE => NONE in
break end;
fun breakConsistent blockIndent = let fun break indent_chunks chunks = case breakInconsistent blockIndent chunks of
NONE => (chunks,indent_chunks)
| SOME (pre,indent,post) =>
break ((indent,post) :: indent_chunks) pre in
break [] end; in fun breakFrame frame = let val Frame
{block,
broken = _,
indent = _, size = _,
chunks} = frame
val blockIndent = indentBlock block in case breakInconsistent blockIndent chunks of
NONE => NONE
| SOME (pre,indent,post) => let val broken = true andsize = sizeChunks post
val frame =
Frame
{block = block,
broken = broken,
indent = indent, size = size,
chunks = post} in case styleBlock block of
Inconsistent => let val indent_chunks = [] in
SOME (pre,indent_chunks,frame) end
| Consistent => let val (pre,indent_chunks) = breakConsistent blockIndent pre in
SOME (pre,indent_chunks,frame) end end end; end;
fun removeChunksFrame frame = let val Frame
{block,
broken,
indent, size = _,
chunks} = frame in if broken andalso List.null chunks then NONE else let val frame =
Frame
{block = block,
broken = true,
indent = indent, size = 0,
chunks = []} in
SOME (chunks,frame) end end;
val removeChunksFrames = let fun remove frames = case frames of
[] => let val chunks = [] and frames = NONE and indent = 0 in
(chunks,frames,indent) end
| top :: rest => let val (chunks,rest',indent) = remove rest
val indent = indent + indentFrame top
val (chunks,top') = case removeChunksFrame top of
NONE => (chunks,NONE)
| SOME (topChunks,top) => (topChunks @ chunks, SOME top)
val frames' = case (top',rest') of
(NONE,NONE) => NONE
| (SOME top, NONE) => SOME (top :: rest)
| (NONE, SOME rest) => SOME (top :: rest)
| (SOME top, SOME rest) => SOME (top :: rest) in
(chunks,frames',indent) end in
fn frames => let val (chunks,frames',indent) = remove frames
val frames = Option.getOpt (frames',frames) in
(chunks,frames,indent) end end;
local fun breakUp lines lineIndent frames = case frames of
[] => NONE
| frame :: frames => case breakUp lines lineIndent frames of
SOME (lines_indent,lineSize,frames) => let val lineSize = lineSize + sizeFrame frame and frames = frame :: frames in
SOME (lines_indent,lineSize,frames) end
| NONE => case breakFrame frame of
NONE => NONE
| SOME (frameChunks,indent_chunks,frame) => let val (chunks,frames,indent) = removeChunksFrames frames
val chunks = frameChunks @ chunks
val lines = addChunksLine lines lineIndent chunks
val lines = addIndentChunksLines lines indent indent_chunks
val lineIndent = indent + indentFrame frame
val lineSize = sizeFrame frame
val frames = frame :: frames in
SOME ((lines,lineIndent),lineSize,frames) end;
fun breakInsideChunk chunk = case chunk of
WordChunk _ => NONE
| BreakChunk _ => raise Bug "Metis_Print.breakInsideChunk"
| FrameChunk frame => case breakFrame frame of
SOME (pathChunks,indent_chunks,frame) => let val pathIndent = 0 and breakIndent = indentFrame frame in
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) end
| NONE => breakInsideFrame frame
and breakInsideChunks chunks = case chunks of
[] => NONE
| chunk :: chunks => case breakInsideChunk chunk of
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) => let val pathChunks = pathChunks @ chunks and chunks = [FrameChunk frame] in
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) end
| NONE => case breakInsideChunks chunks of
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) => let val chunks = chunk :: chunks in
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) end
| NONE => NONE
and breakInsideFrame frame = let val Frame
{block,
broken = _,
indent, size = _,
chunks} = frame in case breakInsideChunks chunks of
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) => let val pathIndent = pathIndent + indent and broken = true andsize = sizeChunks chunks
val frame =
Frame
{block = block,
broken = broken,
indent = indent, size = size,
chunks = chunks} in
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) end
| NONE => NONE end;
fun breakInside lines lineIndent frames = case frames of
[] => NONE
| frame :: frames => case breakInsideFrame frame of
SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) => let val (chunks,frames,indent) = removeChunksFrames frames
val chunks = pathChunks @ chunks and indent = indent + pathIndent
val lines = addChunksLine lines lineIndent chunks
val lines = addIndentChunksLines lines indent indent_chunks
val lineIndent = indent + breakIndent
val lineSize = sizeFrame frame
val frames = frame :: frames in
SOME ((lines,lineIndent),lineSize,frames) end
| NONE => case breakInside lines lineIndent frames of
SOME (lines_indent,lineSize,frames) => let val lineSize = lineSize + sizeFrame frame and frames = frame :: frames in
SOME (lines_indent,lineSize,frames) end
| NONE => NONE; in fun breakFrames lines lineIndent frames = case breakUp lines lineIndent frames of
SOME ((lines,lineIndent),lineSize,frames) =>
SOME (lines,lineIndent,lineSize,frames)
| NONE => case breakInside lines lineIndent frames of
SOME ((lines,lineIndent),lineSize,frames) =>
SOME (lines,lineIndent,lineSize,frames)
| NONE => NONE; end;
(*BasicDebug fun checkChunk chunk = case chunk of WordChunk t => (false, sizeWord t) | BreakChunk b => (false, sizeBreak b) | FrameChunk b => checkFrame b
and checkChunks chunks = case chunks of [] => (false,0) | chunk :: chunks => let val (bk,sz) = checkChunk chunk
val (bk',sz') = checkChunks chunks in (bk orelse bk', sz + sz') end
and checkFrame frame = let val Frame {block = _, broken, indent = _, size, chunks} = frame
val (bk,sz) = checkChunks chunks
val () = if size = sz then () else raise Bug "Metis_Print.checkFrame: wrong size"
val () = if broken orelse not bk then () else raise Bug "Metis_Print.checkFrame: deep broken frame" in (broken,size) end;
fun checkFrames frames = case frames of [] => (true,0) | frame :: frames => let val (bk,sz) = checkFrame frame
val (bk',sz') = checkFrames frames
val () = if bk' orelse not bk then () else raise Bug "Metis_Print.checkFrame: broken stack frame" in (bk, sz + sz') end;
*)
(*BasicDebug fun checkState state = (let val State {lineIndent,lineSize,stack} = state
val () = if not (List.null stack) then () else raise Error "no stack"
val (_,sz) = checkFrames stack
val () = if lineSize = sz then () else raise Error "wrong lineSize" in () end handle Error err => raise Bug err) handle Bug bug => raise Bug ("Metis_Print.checkState: " ^ bug);
*)
fun isEmptyState state = let val State {lineSize,stack,...} = state in
lineSize = 0 andalso List.all isEmptyFrame stack end;
fun isFinalState state = let val State {stack,...} = state in case stack of
[] => raise Bug "Metis_Print.isFinalState: empty stack"
| [frame] => isEmptyFrame frame
| _ :: _ :: _ => false end;
local val initialBlock = let val indent = 0 and style = Inconsistent in
Block
{indent = indent,
style = style} end;
val initialFrame = let val block = initialBlock and broken = false and indent = 0 andsize = 0 and chunks = [] in
Frame
{block = block,
broken = broken,
indent = indent, size = size,
chunks = chunks} end; in val initialState = let val lineIndent = 0 and lineSize = 0 and stack = [initialFrame] in
State
{lineIndent = lineIndent,
lineSize = lineSize,
stack = stack} end; end;
fun normalizeState lineLength lines state = let val State {lineIndent,lineSize,stack} = state
val within = case lineLength of
NONE => true
| SOME len => lineIndent + lineSize <= len in if within then (lines,state) else case breakFrames lines lineIndent stack of
NONE => (lines,state)
| SOME (lines,lineIndent,lineSize,stack) => let (*BasicDebug val () = checkState state
*) val state =
State
{lineIndent = lineIndent,
lineSize = lineSize,
stack = stack} in
normalizeState lineLength lines state end end (*BasicDebug handle Bug bug => raise Bug ("Metis_Print.normalizeState:\n" ^ bug)
*)
local fun executeBeginBlock block lines state = let val State {lineIndent,lineSize,stack} = state
val broken = false and indent = indentBlock block andsize = 0 and chunks = []
val state =
State
{lineIndent = lineIndent,
lineSize = lineSize,
stack = stack} in
(lines,state) end;
fun executeEndBlock lines state = let val State {lineIndent,lineSize,stack} = state
val (lineSize,stack) = case stack of
[] => raise Bug "Metis_Print.executeEndBlock: empty stack"
| topFrame :: stack => let val Frame
{block = topBlock,
broken = topBroken,
indent = topIndent, size = topSize,
chunks = topChunks} = topFrame
val (lineSize,topSize,topChunks,topFrame) = case topChunks of
BreakChunk break :: chunks => let (*BasicDebug val () = let val mesg = "ignoring a break at the end of a " ^ "pretty-printing block" in warn mesg end
*) val n = sizeBreak break
val lineSize = lineSize - n and topSize = topSize - n and topChunks = chunks
val topFrame =
Frame
{block = topBlock,
broken = topBroken,
indent = topIndent, size = topSize,
chunks = topChunks} in
(lineSize,topSize,topChunks,topFrame) end
| _ => (lineSize,topSize,topChunks,topFrame) in ifList.null topChunks then (lineSize,stack) else case stack of
[] => raise Error "Metis_Print.execute: too many end blocks"
| frame :: stack => let val Frame
{block,
broken,
indent, size,
chunks} = frame
val state =
State
{lineIndent = lineIndent,
lineSize = lineSize,
stack = stack} in
normalizeState lineLength lines state end;
fun executeAddBreak lineLength break lines state = let val State {lineIndent,lineSize,stack} = state
val (topFrame,restFrames) = case stack of
[] => raise Bug "Metis_Print.executeAddBreak: empty stack"
| topFrame :: restFrames => (topFrame,restFrames)
val Frame
{block = topBlock,
broken = topBroken,
indent = topIndent, size = topSize,
chunks = topChunks} = topFrame in case topChunks of
[] => (lines,state)
| topChunk :: restTopChunks => let val (topChunks,n) = case topChunk of
BreakChunk break' => let val break = appendBreak break' break
val chunk = BreakChunk break
val topChunks = chunk :: restTopChunks and n = sizeBreak break - sizeBreak break' in
(topChunks,n) end
| _ => let val chunk = BreakChunk break
val topChunks = chunk :: topChunks and n = sizeBreak break in
(topChunks,n) end
val state =
State
{lineIndent = lineIndent,
lineSize = lineSize,
stack = stack}
val lineLength = if breakingFrame topFrame then SOME ~1 else lineLength in
normalizeState lineLength lines state end end;
fun executeBigBreak lines state = let val lineLength = SOME ~1 and break = mkBreak 0 in
executeAddBreak lineLength break lines state end;
fun executeAddNewline lineLength lines state = if isEmptyState state then (addEmptyLine lines, state) else executeBigBreak lines state;
fun executeEof lineLength lines state = if isFinalState state then (lines,state) else let val (lines,state) = executeBigBreak lines state
(*BasicDebug val () = if isFinalState state then () else raise Bug "Metis_Print.executeEof: not a final state"
*) in
(lines,state) end; in fun render {lineLength} = let fun execute step state = let val lines = [] in case step of
BeginBlock block => executeBeginBlock block lines state
| EndBlock => executeEndBlock lines state
| AddWord word => executeAddWord lineLength word lines state
| AddBreak break => executeAddBreak lineLength break lines state
| AddNewline => executeAddNewline lineLength lines state end
(*BasicDebug val execute = fn step => fn state => let val (lines,state) = execute step state
val () = checkState state in (lines,state) end handle Bug bug => raise Bug ("Metis_Print.execute: after " ^ toStringStep step ^ " command:\n" ^ bug)
*)
fun final state = let val lines = []
val (lines,state) = executeEof lineLength lines state
(*BasicDebug val () = checkState state
*) in ifList.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines end (*BasicDebug handle Bug bug => raise Bug ("Metis_Print.final: " ^ bug)
*) in
fn pps => let val lines = Metis_Stream.maps execute final initialState pps in
revConcat lines end end; end;
local fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc); in fun toStringWithLineLength len ppA a = case render len (ppA a) of
Metis_Stream.Nil => ""
| Metis_Stream.Cons (h,t) => let val lines = Metis_Stream.foldl incn (inc h []) (t ()) in String.concat (List.rev lines) end; end;
local fun renderLine {indent,line} = nSpaces indent ^ line ^ "\n"; in fun toStreamWithLineLength len ppA a =
Metis_Stream.map renderLine (render len (ppA a)); end;
fun toLine ppA a = toStringWithLineLength {lineLength = NONE} ppA a;
(* ------------------------------------------------------------------------- *) (* Pretty-printer rendering with a global line length. *) (* ------------------------------------------------------------------------- *)
val lineLength = Unsynchronized.ref initialLineLength;
fun toString ppA a = let val len = {lineLength = SOME (!lineLength)} in
toStringWithLineLength len ppA a end;
fun toStream ppA a = let val len = {lineLength = SOME (!lineLength)} in
toStreamWithLineLength len ppA a end;
fun trace ppX nameX = let fun ppNameX x =
consistentBlock 2
[ppString nameX,
ppString " =",
break,
ppX x] in
fn x => Metis_Useful.trace (toString ppNameX x ^ "\n") end;
end
(**** Original file: src/Parse.sig ****)
(* ========================================================================= *) (* PARSING *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
fun initialize {lines} = let val lastLine = Unsynchronized.ref (~1,"","","")
val chars = let fun saveLast line = let val Unsynchronized.ref (n,_,l2,l3) = lastLine val () = lastLine := (n + 1, l2, l3, line) in String.explode line end in
Metis_Stream.memoize (Metis_Stream.map saveLast lines) end
fun parseErrorLocation () = let val Unsynchronized.ref (n,l1,l2,l3) = lastLine in
(if n <= 0 then"at start" else"around line " ^ Int.toString n) ^
chomp (":\n" ^ l1 ^ l2 ^ l3) end in
{chars = chars,
parseErrorLocation = parseErrorLocation} end;
fun exactChar (c : char) = some (equal c) >> K ();
fun exactCharList cs = case cs of
[] => nothing
| c :: cs => (exactChar c ++ exactCharList cs) >> snd;
fun exactString s = exactCharList (String.explode s);
fun escapeString {escape} = let fun isEscape c = mem c escape
fun isNormal c = case c of
#"\\" => false
| #"\n" => false
| #"\t" => false
| _ => not (isEscape c)
val escapeParser =
(exactChar #"\\" >> K #"\\") ||
(exactChar #"n" >> K #"\n") ||
(exactChar #"t" >> K #"\t") ||
some isEscape
val charParser =
((exactChar #"\\" ++ escapeParser) >> snd) ||
some isNormal in
many charParser >> String.implode end;
local val isSpace = Char.isSpace;
val space = some isSpace; in val manySpace = many space >> K ();
val atLeastOneSpace = atLeastOne space >> K (); end;
fun fromString parser s = fromList parser (String.explode s);
fun parseLayeredInfixes {tokens,assoc} mk tokParser subParser = let fun layerTokParser inp = let val tok_rest as (tok,_) = tokParser inp in if Metis_StringSet.member tok tokens then tok_rest elseraise NoParse end
fun layerMk (x,txs) = case assoc of
Metis_Print.LeftAssoc => let fun inc ((t,y),z) = mk (t,z,y) in List.foldl inc x txs end
| Metis_Print.NonAssoc =>
(case txs of
[] => x
| [(t,y)] => mk (t,x,y)
| _ => raise NoParse)
| Metis_Print.RightAssoc =>
(caseList.rev txs of
[] => x
| tx :: txs => let fun inc ((t,y),(u,z)) = (t, mk (u,y,z))
val (t,y) = List.foldl inc tx txs in
mk (t,x,y) end)
val layerParser = subParser ++ many (layerTokParser ++ subParser) in
layerParser >> layerMk end;
fun parseInfixes ops = let val layeredOps = Metis_Print.layerInfixes ops
val iparsers = List.map parseLayeredInfixes layeredOps in
fn mk => fn tokParser => fn subParser => List.foldr (fn (p,sp) => p mk tokParser sp) subParser iparsers end;
fun parseQuotation printer parser quote = let fun expand (QUOTE q, s) = s ^ q
| expand (ANTIQUOTE a, s) = s ^ printer a
valstring = List.foldl expand "" quote in
parser string end;
end
(**** Original file: src/Name.sig ****)
(* ========================================================================= *) (* NAMES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Name = sig
(* ------------------------------------------------------------------------- *) (* A type of names. *) (* ------------------------------------------------------------------------- *)
type name
(* ------------------------------------------------------------------------- *) (* A total ordering. *) (* ------------------------------------------------------------------------- *)
(* ========================================================================= *) (* NAMES *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Name :> Metis_Name = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type of names. *) (* ------------------------------------------------------------------------- *)
type name = string;
(* ------------------------------------------------------------------------- *) (* A total ordering. *) (* ------------------------------------------------------------------------- *)
fun numName i = mkPrefix prefix (Int.toString i); in fun newName () = numName (newInt ());
fun newNames n = List.map numName (newInts n); end;
fun variantPrime {avoid} = let fun variant n = if avoid n then variant (n ^ "'") else n in
variant end;
local fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c; in fun variantNum {avoid} n = ifnot (avoid n) then n else let val n = stripSuffix isDigitOrPrime n
fun variant i = let val n_i = n ^ Int.toString i in if avoid n_i then variant (i + 1) else n_i end in
variant 0 end; end;
local structure S = Metis_ElementSet (Metis_NameMap); in open S; end;
val pp =
Metis_Print.ppMap
toList
(Metis_Print.ppBracket "{""}" (Metis_Print.ppOpList "," Metis_Name.pp));
end
(**** Original file: src/NameArity.sig ****)
(* ========================================================================= *) (* NAME/ARITY PAIRS *) (* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_NameArity = sig
(* ------------------------------------------------------------------------- *) (* A type of name/arity pairs. *) (* ------------------------------------------------------------------------- *)
type nameArity = Metis_Name.name * int
val name : nameArity -> Metis_Name.name
val arity : nameArity -> int
(* ------------------------------------------------------------------------- *) (* Testing for different arities. *) (* ------------------------------------------------------------------------- *)
val nary : int -> nameArity -> bool
val nullary : nameArity -> bool
val unary : nameArity -> bool
val binary : nameArity -> bool
val ternary : nameArity -> bool
(* ------------------------------------------------------------------------- *) (* A total ordering. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* A type of name/arity pairs. *) (* ------------------------------------------------------------------------- *)
type nameArity = Metis_Name.name * int;
fun name ((n,_) : nameArity) = n;
fun arity ((_,i) : nameArity) = i;
(* ------------------------------------------------------------------------- *) (* Testing for different arities. *) (* ------------------------------------------------------------------------- *)
fun nary i n_i = arity n_i = i;
val nullary = nary 0 and unary = nary 1 and binary = nary 2 and ternary = nary 3;
(* ------------------------------------------------------------------------- *) (* A total ordering. *) (* ------------------------------------------------------------------------- *)
fun compare ((n1,i1),(n2,i2)) = case Metis_Name.compare (n1,n2) of
LESS => LESS
| EQUAL => Int.compare (i1,i2)
| GREATER => GREATER;
fun pp (n,i) =
Metis_Print.inconsistentBlock 0
[Metis_Name.pp n,
Metis_Print.ppString "/",
Metis_Print.ppInt i];
end
structure Metis_NameArityOrdered = structtype t = Metis_NameArity.nameArity val compare = Metis_NameArity.compare end
structure Metis_NameArityMap = struct
local structure S = Metis_KeyMap (Metis_NameArityOrdered); in open S; end;
fun compose m1 m2 = let fun pk ((_,a),n) = peek m2 (n,a) in
mapPartial pk m1 end;
end
structure Metis_NameAritySet = struct
local structure S = Metis_ElementSet (Metis_NameArityMap); in open S; end;
val allNullary = all Metis_NameArity.nullary;
val pp =
Metis_Print.ppMap
toList
(Metis_Print.ppBracket "{""}" (Metis_Print.ppOpList "," Metis_NameArity.pp));
end
(**** Original file: src/Term.sig ****)
(* ========================================================================= *) (* FIRST ORDER LOGIC TERMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Term = sig
(* ------------------------------------------------------------------------- *) (* A type of first order logic terms. *) (* ------------------------------------------------------------------------- *)
type var = Metis_Name.name
type functionName = Metis_Name.name
type function = functionName * int
typeconst = functionName
datatype term =
Var of var
| Fn of functionName * term list
val destBinop : functionName -> term -> term * term
val isBinop : functionName -> term -> bool
(* ------------------------------------------------------------------------- *) (* The size of a term in symbols. *) (* ------------------------------------------------------------------------- *)
val symbols : term -> int
(* ------------------------------------------------------------------------- *) (* A total comparison function for terms. *) (* ------------------------------------------------------------------------- *)
val variantPrime : Metis_NameSet.set -> var -> var
val variantNum : Metis_NameSet.set -> var -> var
(* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *)
val hasTypeFunctionName : functionName
val hasTypeFunction : function
val isTypedVar : term -> bool
val typedSymbols : term -> int
val nonVarTypedSubterms : term -> (path * term) list
(* ------------------------------------------------------------------------- *) (* Special support for terms with an explicit function application operator. *) (* ------------------------------------------------------------------------- *)
val infixes : Metis_Print.infixes Unsynchronized.ref
(* The negation symbol *)
val negation : string Unsynchronized.ref
(* Binder symbols *)
val binders : stringlist Unsynchronized.ref
(* Bracket symbols *)
val brackets : (string * string) list Unsynchronized.ref
(* Pretty printing *)
val pp : term Metis_Print.pp
val toString : term -> string
(* Parsing *)
val fromString : string -> term
val parse : term Metis_Parse.quotation -> term
end
(**** Original file: src/Term.sml ****)
(* ========================================================================= *) (* FIRST ORDER LOGIC TERMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Term :> Metis_Term = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type of first order logic terms. *) (* ------------------------------------------------------------------------- *)
type var = Metis_Name.name;
type functionName = Metis_Name.name;
type function = functionName * int;
typeconst = functionName;
datatype term =
Var of Metis_Name.name
| Fn of Metis_Name.name * term list;
fun destConst (Fn (c, [])) = c
| destConst _ = raise Error "destConst";
val isConst = can destConst;
(* Binary functions *)
fun mkBinop f (a,b) = Fn (f,[a,b]);
fun destBinop f (Fn (x,[a,b])) = if Metis_Name.equal x f then (a,b) elseraise Error "Metis_Term.destBinop: wrong binop"
| destBinop _ _ = raise Error "Metis_Term.destBinop: not a binop";
fun isBinop f = can (destBinop f);
(* ------------------------------------------------------------------------- *) (* The size of a term in symbols. *) (* ------------------------------------------------------------------------- *)
val VAR_SYMBOLS = 1;
val FN_SYMBOLS = 1;
local fun sz n [] = n
| sz n (Var _ :: tms) = sz (n + VAR_SYMBOLS) tms
| sz n (Fn (func,args) :: tms) = sz (n + FN_SYMBOLS) (args @ tms); in fun symbols tm = sz 0 [tm]; end;
(* ------------------------------------------------------------------------- *) (* A total comparison function for terms. *) (* ------------------------------------------------------------------------- *)
local fun cmp [] [] = EQUAL
| cmp (tm1 :: tms1) (tm2 :: tms2) = let val tm1_tm2 = (tm1,tm2) in if Metis_Portable.pointerEqual tm1_tm2 then cmp tms1 tms2 else case tm1_tm2 of
(Var v1, Var v2) =>
(case Metis_Name.compare (v1,v2) of
LESS => LESS
| EQUAL => cmp tms1 tms2
| GREATER => GREATER)
| (Var _, Fn _) => LESS
| (Fn _, Var _) => GREATER
| (Fn (f1,a1), Fn (f2,a2)) =>
(case Metis_Name.compare (f1,f2) of
LESS => LESS
| EQUAL =>
(case Int.compare (length a1, length a2) of
LESS => LESS
| EQUAL => cmp (a1 @ tms1) (a2 @ tms2)
| GREATER => GREATER)
| GREATER => GREATER) end
| cmp _ _ = raise Bug "Metis_Term.compare"; in fun compare (tm1,tm2) = cmp [tm1] [tm2]; end;
local fun subtms [] acc = acc
| subtms ((path,tm) :: rest) acc = let fun f (n,arg) = (n :: path, arg)
val acc = (List.rev path, tm) :: acc in case tm of
Var _ => subtms rest acc
| Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc end; in fun subterms tm = subtms [([],tm)] []; end;
fun replace tm ([],res) = if equal res tm then tm else res
| replace tm (h :: t, res) = case tm of
Var _ => raise Error "Metis_Term.replace: Var"
| Fn (func,tms) => if h >= length tms thenraise Error "Metis_Term.replace: Fn" else let val arg = List.nth (tms,h) val arg' = replace arg (t,res) in if Metis_Portable.pointerEqual (arg',arg) then tm else Fn (func, updateNth (h,arg') tms) end;
funfind pred = let fun search [] = NONE
| search ((path,tm) :: rest) = if pred tm then SOME (List.rev path) else case tm of
Var _ => search rest
| Fn (_,a) => let val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a) in
search (subtms @ rest) end in
fn tm => search [([],tm)] end;
val ppPath = Metis_Print.ppList Metis_Print.ppInt;
local fun free _ [] = false
| free v (Var w :: tms) = Metis_Name.equal v w orelse free v tms
| free v (Fn (_,args) :: tms) = free v (args @ tms); in fun freeIn v tm = free v [tm]; end;
local fun free vs [] = vs
| free vs (Var v :: tms) = free (Metis_NameSet.add vs v) tms
| free vs (Fn (_,args) :: tms) = free vs (args @ tms); in val freeVarsList = free Metis_NameSet.empty;
fun newVars n = List.map Var (Metis_Name.newNames n);
local fun avoid av n = Metis_NameSet.member n av; in fun variantPrime av = Metis_Name.variantPrime {avoid = avoid av};
fun variantNum av = Metis_Name.variantNum {avoid = avoid av}; end;
(* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *)
val hasTypeFunctionName = Metis_Name.fromString ":";
val hasTypeFunction = (hasTypeFunctionName,2);
fun destFnHasType ((f,a) : functionName * term list) = ifnot (Metis_Name.equal f hasTypeFunctionName) then raise Error "Metis_Term.destFnHasType" else case a of
[tm,ty] => (tm,ty)
| _ => raise Error "Metis_Term.destFnHasType";
val isFnHasType = can destFnHasType;
fun isTypedVar tm = case tm of
Var _ => true
| Fn func => case total destFnHasType func of
SOME (Var _, _) => true
| _ => false;
local fun sz n [] = n
| sz n (tm :: tms) = case tm of
Var _ => sz (n + 1) tms
| Fn func => case total destFnHasType func of
SOME (tm,_) => sz n (tm :: tms)
| NONE => let val (_,a) = func in
sz (n + 1) (a @ tms) end; in fun typedSymbols tm = sz 0 [tm]; end;
local fun subtms [] acc = acc
| subtms ((path,tm) :: rest) acc = case tm of
Var _ => subtms rest acc
| Fn func => case total destFnHasType func of
SOME (t,_) =>
(case t of
Var _ => subtms rest acc
| Fn _ => let val acc = (List.rev path, tm) :: acc val rest = (0 :: path, t) :: rest in
subtms rest acc end)
| NONE => let fun f (n,arg) = (n :: path, arg)
val (_,args) = func
val acc = (List.rev path, tm) :: acc
val rest = List.map f (enumerate args) @ rest in
subtms rest acc end; in fun nonVarTypedSubterms tm = subtms [([],tm)] []; end;
(* ------------------------------------------------------------------------- *) (* Special support for terms with an explicit function application operator. *) (* ------------------------------------------------------------------------- *)
val appName = Metis_Name.fromString ".";
fun mkFnApp (fTm,aTm) = (appName, [fTm,aTm]);
fun mkApp f_a = Fn (mkFnApp f_a);
fun destFnApp ((f,a) : Metis_Name.name * term list) = ifnot (Metis_Name.equal f appName) thenraise Error "Metis_Term.destFnApp" else case a of
[fTm,aTm] => (fTm,aTm)
| _ => raise Error "Metis_Term.destFnApp";
val isFnApp = can destFnApp;
fun destApp tm = case tm of
Var _ => raise Error "Metis_Term.destApp"
| Fn func => destFnApp func;
val isApp = can destApp;
fun listMkApp (f,l) = List.foldl mkApp f l;
local fun strip tms tm = case total destApp tm of
SOME (f,a) => strip (a :: tms) f
| NONE => (tm,tms); in fun stripApp tm = strip [] tm; end;
val negation : string Unsynchronized.ref = Unsynchronized.ref"~";
(* Binder symbols *)
val binders : stringlist Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"];
(* Bracket symbols *)
val brackets : (string * string) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")];
(* Pretty printing *)
fun pp inputTerm = let val quants = !binders and iOps = !infixes and neg = !negation and bracks = !brackets
val bMap = let fun f (b1,b2) = (b1 ^ b2, b1, b2) in List.map f bracks end
val bTokens = op@ (unzip bracks)
val iTokens = Metis_Print.tokensInfixes iOps
fun destI tm = case tm of
Fn (f,[a,b]) => let val f = Metis_Name.toString f in if Metis_StringSet.member f iTokens then SOME (f,a,b) else NONE end
| _ => NONE
fun isI tm = Option.isSome (destI tm)
fun iToken (_,tok) =
Metis_Print.program
[(if tok = ","then Metis_Print.skip else Metis_Print.ppString " "),
Metis_Print.ppString tok,
Metis_Print.break];
val iPrinter = Metis_Print.ppInfixes iOps destI iToken
fun checkVarName bv n = let val s = Metis_Name.toString n in if vName bv s then s else"$" ^ s end
fun varName bv = Metis_Print.ppMap (checkVarName bv) Metis_Print.ppString
fun checkFunctionName bv n = let val s = Metis_Name.toString n in if Metis_StringSet.member s specialTokens orelse vName bv s then "(" ^ s ^ ")" else
s end
fun functionName bv = Metis_Print.ppMap (checkFunctionName bv) Metis_Print.ppString
fun stripNeg tm = case tm of
Fn (f,[a]) => if Metis_Name.toString f <> neg then (0,tm) elseletval (n,tm) = stripNeg a in (n + 1, tm) end
| _ => (0,tm)
val destQuant = let fun dest q (Fn (q', [Var v, body])) = if Metis_Name.toString q' <> q then NONE else
(case dest q body of
NONE => SOME (q,v,[],body)
| SOME (_,v',vs,body) => SOME (q, v, v' :: vs, body))
| dest _ _ = NONE in
fn tm => Metis_Useful.first (fn q => dest q tm) quants end
fun isQuant tm = Option.isSome (destQuant tm)
fun destBrack (Fn (b,[tm])) = let val s = Metis_Name.toString b in caseList.find (fn (n,_,_) => n = s) bMap of
NONE => NONE
| SOME (_,b1,b2) => SOME (b1,tm,b2) end
| destBrack _ = NONE
fun isBrack tm = Option.isSome (destBrack tm)
fun functionArgument bv tm =
Metis_Print.sequence
Metis_Print.break
(if isBrack tm then customBracket bv tm elseif isVar tm orelse isConst tm then basic bv tm else bracket bv tm)
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
Metis_Print.inconsistentBlock 2
(functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm = case destBrack tm of
SOME (b1,tm,b2) => Metis_Print.ppBracket b1 b2 (term bv) tm
| NONE => basic bv tm
and innerQuant bv tm = case destQuant tm of
NONE => term bv tm
| SOME (q,v,vs,tm) => let val bv = Metis_StringSet.addList bv (List.map Metis_Name.toString (v :: vs)) in
Metis_Print.program
[Metis_Print.ppString q,
varName bv v,
Metis_Print.program
(List.map (Metis_Print.sequence Metis_Print.break o varName bv) vs),
Metis_Print.ppString ".",
Metis_Print.break,
innerQuant bv tm] end
and quantifier bv tm = ifnot (isQuant tm) then customBracket bv tm else Metis_Print.inconsistentBlock 2 [innerQuant bv tm]
and molecule bv (tm,r) = let val (n,tm) = stripNeg tm in
Metis_Print.inconsistentBlock n
[Metis_Print.duplicate n (Metis_Print.ppString neg), if isI tm orelse (r andalso isQuant tm) then bracket bv tm else quantifier bv tm] end
and term bv tm = iPrinter (molecule bv) (tm,false)
and bracket bv tm = Metis_Print.ppBracket "("")" (term bv) tm in
term Metis_StringSet.empty end inputTerm;
val toString = Metis_Print.toString pp;
(* Parsing *)
local open Metis_Parse;
infixr 9 >>++
infixr 8 ++
infixr 7 >>
infixr 6 ||
val isAlphaNum = let val alphaNumChars = String.explode "_'" in
fn c => mem c alphaNumChars orelse Char.isAlphaNum c end;
local val alphaNumToken = atLeastOne (some isAlphaNum) >> String.implode;
val symbolToken = let fun isNeg c = str c = !negation
val symbolChars = String.explode "<>=-*+/\\?@|!$%&#^:;~"
fun isSymbol c = mem c symbolChars
fun isNonNegSymbol c = not (isNeg c) andalso isSymbol c in
some isNeg >> str ||
(some isNonNegSymbol ++ many (some isSymbol)) >>
(String.implode o op::) end;
val punctToken = let val punctChars = String.explode "()[]{}.,"
fun isPunct c = mem c punctChars in
some isPunct >> str end;
val lexToken = alphaNumToken || symbolToken || punctToken;
val space = many (some Char.isSpace); in val lexer = (space ++ lexToken ++ space) >> (fn (_,(tok,_)) => tok); end;
fun termParser inputStream = let val quants = !binders and iOps = !infixes and neg = !negation and bracks = ("(",")") :: !brackets
fun bracket (ab,a,b) =
(some (Metis_Useful.equal a) ++ term bv ++ some (Metis_Useful.equal b)) >>
(fn (_,(tm,_)) => if ab = "()"then tm else Fn (Metis_Name.fromString ab, [tm]))
fun quantifier q = let fun bind (v,t) =
Fn (Metis_Name.fromString q, [Var (Metis_Name.fromString v), t]) in
(some (Metis_Useful.equal q) ++
atLeastOne (some possibleVarName) ++
some (Metis_Useful.equal ".")) >>++
(fn (_,(vs,_)) =>
term (Metis_StringSet.addList bv vs) >>
(fn body => List.foldr bind body vs)) end in
var || const ||
first (List.map bracket bracks) ||
first (List.map quantifier quants) end tokens
and molecule bv tokens = let val negations = many (some (Metis_Useful.equal neg)) >> length
val function =
(functionName bv ++ many (basic bv)) >>
(fn (f,args) => Fn (Metis_Name.fromString f, args)) ||
basic bv in
(negations ++ function) >>
(fn (n,tm) => funpow n (fn t => Fn (Metis_Name.fromString neg, [t])) tm) end tokens
and term bv tokens = iParser (molecule bv) tokens in
term Metis_StringSet.empty end inputStream; in fun fromString input = let val chars = Metis_Stream.fromList (String.explode input)
val tokens = everything (lexer >> singleton) chars
val terms = everything (termParser >> singleton) tokens in case Metis_Stream.toList terms of
[tm] => tm
| _ => raise Error "Metis_Term.fromString" end; end;
local val antiquotedTermToString =
Metis_Print.toString (Metis_Print.ppBracket "("")" pp); in val parse = Metis_Parse.parseQuotation antiquotedTermToString fromString; end;
end
structure Metis_TermOrdered = structtype t = Metis_Term.term val compare = Metis_Term.compare end
(* ========================================================================= *) (* FIRST ORDER LOGIC SUBSTITUTIONS *) (* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Subst = sig
(* ------------------------------------------------------------------------- *) (* A type of first order logic substitutions. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* Applying a substitution to a first order logic term. *) (* ------------------------------------------------------------------------- *)
val subst : subst -> Metis_Term.term -> Metis_Term.term
(* ------------------------------------------------------------------------- *) (* Restricting a substitution to a smaller set of variables. *) (* ------------------------------------------------------------------------- *)
val restrict : subst -> Metis_NameSet.set -> subst
val remove : subst -> Metis_NameSet.set -> subst
(* ------------------------------------------------------------------------- *) (* Composing two substitutions so that the following identity holds: *) (* *) (* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *) (* ------------------------------------------------------------------------- *)
val compose : subst -> subst -> subst
(* ------------------------------------------------------------------------- *) (* Creating the union of two compatible substitutions. *) (* ------------------------------------------------------------------------- *)
val union : subst -> subst -> subst (* raises Error *)
(* ------------------------------------------------------------------------- *) (* Substitutions can be inverted iff they are renaming substitutions. *) (* ------------------------------------------------------------------------- *)
val invert : subst -> subst (* raises Error *)
val isRenaming : subst -> bool
(* ------------------------------------------------------------------------- *) (* Creating a substitution to freshen variables. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* Matching for first order logic terms. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* Unification for first order logic terms. *) (* ------------------------------------------------------------------------- *)
(* ========================================================================= *) (* FIRST ORDER LOGIC SUBSTITUTIONS *) (* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Subst :> Metis_Subst = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type of first order logic substitutions. *) (* ------------------------------------------------------------------------- *)
datatype subst = Metis_Subst of Metis_Term.term Metis_NameMap.map;
local fun isNotId (v,tm) = not (Metis_Term.equalVar v tm); in fun normalize (sub as Metis_Subst m) = let val m' = Metis_NameMap.filter isNotId m in if Metis_NameMap.size m = Metis_NameMap.size m' then sub else Metis_Subst m' end; end;
(* ------------------------------------------------------------------------- *) (* Applying a substitution to a first order logic term. *) (* ------------------------------------------------------------------------- *)
fun subst sub = let fun tmSub (tm as Metis_Term.Var v) =
(case peek sub v of
SOME tm' => if Metis_Portable.pointerEqual (tm,tm') then tm else tm'
| NONE => tm)
| tmSub (tm as Metis_Term.Fn (f,args)) = let val args' = Metis_Sharing.map tmSub args in if Metis_Portable.pointerEqual (args,args') then tm else Metis_Term.Fn (f,args') end in
fn tm => if null subthen tm else tmSub tm end;
(* ------------------------------------------------------------------------- *) (* Restricting a substitution to a given set of variables. *) (* ------------------------------------------------------------------------- *)
fun restrict (sub as Metis_Subst m) varSet = let fun isRestrictedVar (v,_) = Metis_NameSet.member v varSet
val m' = Metis_NameMap.filter isRestrictedVar m in if Metis_NameMap.size m = Metis_NameMap.size m' then sub else Metis_Subst m' end;
fun remove (sub as Metis_Subst m) varSet = let fun isRestrictedVar (v,_) = not (Metis_NameSet.member v varSet)
val m' = Metis_NameMap.filter isRestrictedVar m in if Metis_NameMap.size m = Metis_NameMap.size m' then sub else Metis_Subst m' end;
(* ------------------------------------------------------------------------- *) (* Composing two substitutions so that the following identity holds: *) (* *) (* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *) (* ------------------------------------------------------------------------- *)
fun compose (sub1 as Metis_Subst m1) sub2 = let fun f (v,tm,s) = insert s (v, subst sub2 tm) in if null sub2 then sub1 else Metis_NameMap.foldl f sub2 m1 end;
(* ------------------------------------------------------------------------- *) (* Creating the union of two compatible substitutions. *) (* ------------------------------------------------------------------------- *)
local fun compatible ((_,tm1),(_,tm2)) = if Metis_Term.equal tm1 tm2 then SOME tm1 elseraise Error "Metis_Subst.union: incompatible"; in fun union (s1 as Metis_Subst m1) (s2 as Metis_Subst m2) = if Metis_NameMap.null m1 then s2 elseif Metis_NameMap.null m2 then s1 else Metis_Subst (Metis_NameMap.union compatible m1 m2); end;
(* ------------------------------------------------------------------------- *) (* Substitutions can be inverted iff they are renaming substitutions. *) (* ------------------------------------------------------------------------- *)
local fun inv (v, Metis_Term.Var w, s) = if Metis_NameMap.inDomain w s thenraise Error "Metis_Subst.invert: non-injective" else Metis_NameMap.insert s (w, Metis_Term.Var v)
| inv (_, Metis_Term.Fn _, _) = raise Error "Metis_Subst.invert: non-variable"; in fun invert (Metis_Subst m) = Metis_Subst (Metis_NameMap.foldl inv (Metis_NameMap.new ()) m); end;
val isRenaming = can invert;
(* ------------------------------------------------------------------------- *) (* Creating a substitution to freshen variables. *) (* ------------------------------------------------------------------------- *)
val freshVars = let fun add (v,m) = insert m (v, Metis_Term.newVar ()) in
Metis_NameSet.foldl add empty end;
val functions = let fun add (_,t,s) = Metis_NameAritySet.union s (Metis_Term.functions t) in
foldl add Metis_NameAritySet.empty end;
(* ------------------------------------------------------------------------- *) (* Matching for first order logic terms. *) (* ------------------------------------------------------------------------- *)
local fun matchList sub [] = sub
| matchList sub ((Metis_Term.Var v, tm) :: rest) = let valsub = case peek sub v of
NONE => insert sub (v,tm)
| SOME tm' => if Metis_Term.equal tm tm' then sub elseraise Error "Metis_Subst.match: incompatible matches" in
matchList sub rest end
| matchList sub ((Metis_Term.Fn (f1,args1), Metis_Term.Fn (f2,args2)) :: rest) = if Metis_Name.equal f1 f2 andalso length args1 = length args2 then
matchList sub (zip args1 args2 @ rest) elseraise Error "Metis_Subst.match: different structure"
| matchList _ _ = raise Error "Metis_Subst.match: functions can't match vars"; in funmatchsub tm1 tm2 = matchList sub [(tm1,tm2)]; end;
(* ------------------------------------------------------------------------- *) (* Unification for first order logic terms. *) (* ------------------------------------------------------------------------- *)
local fun solve sub [] = sub
| solve sub ((tm1_tm2 as (tm1,tm2)) :: rest) = if Metis_Portable.pointerEqual tm1_tm2 then solve sub rest else solve' sub (subst sub tm1) (subst sub tm2) rest
and solve' sub (Metis_Term.Var v) tm rest = if Metis_Term.equalVar v tm then solve sub rest elseif Metis_Term.freeIn v tm thenraise Error "Metis_Subst.unify: occurs check" else
(case peek sub v of
NONE => solve (compose sub (singleton (v,tm))) rest
| SOME tm' => solve'sub tm' tm rest)
| solve' sub tm1 (tm2 as Metis_Term.Var _) rest = solve'sub tm2 tm1 rest
| solve' sub (Metis_Term.Fn (f1,args1)) (Metis_Term.Fn (f2,args2)) rest = if Metis_Name.equal f1 f2 andalso length args1 = length args2 then
solve sub (zip args1 args2 @ rest) else raise Error "Metis_Subst.unify: different structure"; in fun unify sub tm1 tm2 = solve sub [(tm1,tm2)]; end;
end
(**** Original file: src/Atom.sig ****)
(* ========================================================================= *) (* FIRST ORDER LOGIC ATOMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Atom = sig
(* ------------------------------------------------------------------------- *) (* A type for storing first order logic atoms. *) (* ------------------------------------------------------------------------- *)
val mkBinop : relationName -> Metis_Term.term * Metis_Term.term -> atom
val destBinop : relationName -> atom -> Metis_Term.term * Metis_Term.term
val isBinop : relationName -> atom -> bool
(* ------------------------------------------------------------------------- *) (* The size of an atom in symbols. *) (* ------------------------------------------------------------------------- *)
val symbols : atom -> int
(* ------------------------------------------------------------------------- *) (* A total comparison function for atoms. *) (* ------------------------------------------------------------------------- *)
val mkEq : Metis_Term.term * Metis_Term.term -> atom
val destEq : atom -> Metis_Term.term * Metis_Term.term
val isEq : atom -> bool
val mkRefl : Metis_Term.term -> atom
val destRefl : atom -> Metis_Term.term
val isRefl : atom -> bool
val sym : atom -> atom (* raises Error if given a refl *)
val lhs : atom -> Metis_Term.term
val rhs : atom -> Metis_Term.term
(* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *)
val typedSymbols : atom -> int
val nonVarTypedSubterms : atom -> (Metis_Term.path * Metis_Term.term) list
val parse : Metis_Term.term Metis_Parse.quotation -> atom
end
(**** Original file: src/Atom.sml ****)
(* ========================================================================= *) (* FIRST ORDER LOGIC ATOMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Atom :> Metis_Atom = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type for storing first order logic atoms. *) (* ------------------------------------------------------------------------- *)
val functions = let fun f (tm,acc) = Metis_NameAritySet.union (Metis_Term.functions tm) acc in
fn atm => List.foldl f Metis_NameAritySet.empty (arguments atm) end;
val functionNames = let fun f (tm,acc) = Metis_NameSet.union (Metis_Term.functionNames tm) acc in
fn atm => List.foldl f Metis_NameSet.empty (arguments atm) end;
(* Binary relations *)
fun mkBinop p (a,b) : atom = (p,[a,b]);
fun destBinop p (x,[a,b]) = if Metis_Name.equal x p then (a,b) elseraise Error "Metis_Atom.destBinop: wrong binop"
| destBinop _ _ = raise Error "Metis_Atom.destBinop: not a binop";
fun isBinop p = can (destBinop p);
(* ------------------------------------------------------------------------- *) (* The size of an atom in symbols. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* A total comparison function for atoms. *) (* ------------------------------------------------------------------------- *)
fun compare ((p1,tms1),(p2,tms2)) = case Metis_Name.compare (p1,p2) of
LESS => LESS
| EQUAL => lexCompare Metis_Term.compare (tms1,tms2)
| GREATER => GREATER;
fun equal atm1 atm2 = compare (atm1,atm2) = EQUAL;
fun subterm _ [] = raise Bug "Metis_Atom.subterm: empty path"
| subterm ((_,tms) : atom) (h :: t) = if h >= length tms thenraise Error "Metis_Atom.subterm: bad path" else Metis_Term.subterm (List.nth (tms,h)) t;
fun subterms ((_,tms) : atom) = let fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l in List.foldl f [] (enumerate tms) end;
fun replace _ ([],_) = raise Bug "Metis_Atom.replace: empty path"
| replace (atm as (rel,tms)) (h :: t, res) : atom = if h >= length tms thenraise Error "Metis_Atom.replace: bad path" else let val tm = List.nth (tms,h) val tm' = Metis_Term.replace tm (t,res) in if Metis_Portable.pointerEqual (tm,tm') then atm else (rel, updateNth (h,tm') tms) end;
funfind pred = let fun f (i,tm) = case Metis_Term.find pred tm of
SOME path => SOME (i :: path)
| NONE => NONE in
fn (_,tms) : atom => first f (enumerate tms) end;
fun freeIn v atm = List.exists (Metis_Term.freeIn v) (arguments atm);
val freeVars = let fun f (tm,acc) = Metis_NameSet.union (Metis_Term.freeVars tm) acc in
fn atm => List.foldl f Metis_NameSet.empty (arguments atm) end;
fun subst sub (atm as (p,tms)) : atom = let val tms' = Metis_Sharing.map (Metis_Subst.subst sub) tms in if Metis_Portable.pointerEqual (tms',tms) then atm else (p,tms') end;
local fun unifyArg ((tm1,tm2),sub) = Metis_Subst.unify sub tm1 tm2; in fun unify sub (p1,tms1) (p2,tms2) = let val _ = (Metis_Name.equal p1 p2 andalso length tms1 = length tms2) orelse raise Error "Metis_Atom.unify" in List.foldl unifyArg sub (zip tms1 tms2) end; end;
val eqRelation = (eqRelationName,eqRelationArity);
val mkEq = mkBinop eqRelationName;
fun destEq x = destBinop eqRelationName x;
fun isEq x = isBinop eqRelationName x;
fun mkRefl tm = mkEq (tm,tm);
fun destRefl atm = let val (l,r) = destEq atm val _ = Metis_Term.equal l r orelse raise Error "Metis_Atom.destRefl" in
l end;
fun isRefl x = can destRefl x;
fun sym atm = let val (l,r) = destEq atm val _ = not (Metis_Term.equal l r) orelse raise Error "Metis_Atom.sym: refl" in
mkEq (r,l) end;
fun lhs atm = fst (destEq atm);
fun rhs atm = snd (destEq atm);
(* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *)
fun nonVarTypedSubterms (_,tms) = let fun addArg ((n,arg),acc) = let fun addTm ((path,tm),acc) = (n :: path, tm) :: acc in List.foldl addTm acc (Metis_Term.nonVarTypedSubterms arg) end in List.foldl addArg [] (enumerate tms) end;
(* ========================================================================= *) (* FIRST ORDER LOGIC FORMULAS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Formula = sig
(* ------------------------------------------------------------------------- *) (* A type of first order logic formulas. *) (* ------------------------------------------------------------------------- *)
datatype formula = True
| False
| Metis_Atom of Metis_Atom.atom
| Notof formula
| Andof formula * formula
| Orof formula * formula
| Imp of formula * formula
| Iff of formula * formula
| Forall of Metis_Term.var * formula
| Existsof Metis_Term.var * formula
val destForall : formula -> Metis_Term.var * formula
val isForall : formula -> bool
val listMkForall : Metis_Term.var list * formula -> formula
val setMkForall : Metis_NameSet.set * formula -> formula
val stripForall : formula -> Metis_Term.var list * formula
(* Existential quantification *)
val destExists : formula -> Metis_Term.var * formula
val isExists : formula -> bool
val listMkExists : Metis_Term.var list * formula -> formula
val setMkExists : Metis_NameSet.set * formula -> formula
val stripExists : formula -> Metis_Term.var list * formula
(* ------------------------------------------------------------------------- *) (* The size of a formula in symbols. *) (* ------------------------------------------------------------------------- *)
val symbols : formula -> int
(* ------------------------------------------------------------------------- *) (* A total comparison function for formulas. *) (* ------------------------------------------------------------------------- *)
(* ========================================================================= *) (* FIRST ORDER LOGIC FORMULAS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Formula :> Metis_Formula = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type of first order logic formulas. *) (* ------------------------------------------------------------------------- *)
datatype formula = True
| False
| Metis_Atom of Metis_Atom.atom
| Notof formula
| Andof formula * formula
| Orof formula * formula
| Imp of formula * formula
| Iff of formula * formula
| Forall of Metis_Term.var * formula
| Existsof Metis_Term.var * formula;
fun listMkExists ([],body) = body
| listMkExists (v :: vs, body) = Exists (v, listMkExists (vs,body));
fun setMkExists (vs,body) = Metis_NameSet.foldr Exists body vs;
local fun strip vs (Exists (v,b)) = strip (v :: vs) b
| strip vs tm = (List.rev vs, tm); in val stripExists = strip []; end;
(* ------------------------------------------------------------------------- *) (* The size of a formula in symbols. *) (* ------------------------------------------------------------------------- *)
local fun sz n [] = n
| sz n (True :: fms) = sz (n + 1) fms
| sz n (False :: fms) = sz (n + 1) fms
| sz n (Metis_Atom atm :: fms) = sz (n + Metis_Atom.symbols atm) fms
| sz n (Not p :: fms) = sz (n + 1) (p :: fms)
| sz n (And (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
| sz n (Or (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
| sz n (Imp (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
| sz n (Iff (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
| sz n (Forall (_,p) :: fms) = sz (n + 1) (p :: fms)
| sz n (Exists (_,p) :: fms) = sz (n + 1) (p :: fms); in fun symbols fm = sz 0 [fm]; end;
(* ------------------------------------------------------------------------- *) (* A total comparison function for formulas. *) (* ------------------------------------------------------------------------- *)
local fun cmp [] = EQUAL
| cmp (f1_f2 :: fs) = if Metis_Portable.pointerEqual f1_f2 then cmp fs else case f1_f2 of
(True,True) => cmp fs
| (True,_) => LESS
| (_,True) => GREATER
| (False,False) => cmp fs
| (False,_) => LESS
| (_,False) => GREATER
| (Metis_Atom atm1, Metis_Atom atm2) =>
(case Metis_Atom.compare (atm1,atm2) of
LESS => LESS
| EQUAL => cmp fs
| GREATER => GREATER)
| (Metis_Atom _, _) => LESS
| (_, Metis_Atom _) => GREATER
| (Not p1, Not p2) => cmp ((p1,p2) :: fs)
| (Not _, _) => LESS
| (_, Not _) => GREATER
| (And (p1,q1), And (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
| (And _, _) => LESS
| (_, And _) => GREATER
| (Or (p1,q1), Or (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
| (Or _, _) => LESS
| (_, Or _) => GREATER
| (Imp (p1,q1), Imp (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
| (Imp _, _) => LESS
| (_, Imp _) => GREATER
| (Iff (p1,q1), Iff (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
| (Iff _, _) => LESS
| (_, Iff _) => GREATER
| (Forall (v1,p1), Forall (v2,p2)) =>
(case Metis_Name.compare (v1,v2) of
LESS => LESS
| EQUAL => cmp ((p1,p2) :: fs)
| GREATER => GREATER)
| (Forall _, Exists _) => LESS
| (Exists _, Forall _) => GREATER
| (Exists (v1,p1), Exists (v2,p2)) =>
(case Metis_Name.compare (v1,v2) of
LESS => LESS
| EQUAL => cmp ((p1,p2) :: fs)
| GREATER => GREATER); in fun compare fm1_fm2 = cmp [fm1_fm2]; end;
fun freeIn v = let fun f [] = false
| f (True :: fms) = f fms
| f (False :: fms) = f fms
| f (Metis_Atom atm :: fms) = Metis_Atom.freeIn v atm orelse f fms
| f (Not p :: fms) = f (p :: fms)
| f (And (p,q) :: fms) = f (p :: q :: fms)
| f (Or (p,q) :: fms) = f (p :: q :: fms)
| f (Imp (p,q) :: fms) = f (p :: q :: fms)
| f (Iff (p,q) :: fms) = f (p :: q :: fms)
| f (Forall (w,p) :: fms) = if Metis_Name.equal v w then f fms else f (p :: fms)
| f (Exists (w,p) :: fms) = if Metis_Name.equal v w then f fms else f (p :: fms) in
fn fm => f [fm] end;
local fun fv vs [] = vs
| fv vs ((_,True) :: fms) = fv vs fms
| fv vs ((_,False) :: fms) = fv vs fms
| fv vs ((bv, Metis_Atom atm) :: fms) =
fv (Metis_NameSet.union vs (Metis_NameSet.difference (Metis_Atom.freeVars atm) bv)) fms
| fv vs ((bv, Not p) :: fms) = fv vs ((bv,p) :: fms)
| fv vs ((bv, And (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
| fv vs ((bv, Or (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
| fv vs ((bv, Imp (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
| fv vs ((bv, Iff (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
| fv vs ((bv, Forall (v,p)) :: fms) = fv vs ((Metis_NameSet.add bv v, p) :: fms)
| fv vs ((bv, Exists (v,p)) :: fms) = fv vs ((Metis_NameSet.add bv v, p) :: fms);
fun add (fm,vs) = fv vs [(Metis_NameSet.empty,fm)]; in fun freeVars fm = add (fm,Metis_NameSet.empty);
fun freeVarsList fms = List.foldl add Metis_NameSet.empty fms; end;
fun specialize fm = snd (stripForall fm);
fun generalize fm = listMkForall (Metis_NameSet.toList (freeVars fm), fm);
local fun substCheck sub fm = if Metis_Subst.null subthen fm else substFm sub fm
and substFm sub fm = case fm of True => fm
| False => fm
| Metis_Atom (p,tms) => let val tms' = Metis_Sharing.map (Metis_Subst.subst sub) tms in if Metis_Portable.pointerEqual (tms,tms') then fm else Metis_Atom (p,tms') end
| Not p => let val p' = substFm sub p in if Metis_Portable.pointerEqual (p,p') then fm else Not p' end
| And (p,q) => substConn sub fm And p q
| Or (p,q) => substConn sub fm Or p q
| Imp (p,q) => substConn sub fm Imp p q
| Iff (p,q) => substConn sub fm Iff p q
| Forall (v,p) => substQuant sub fm Forall v p
| Exists (v,p) => substQuant sub fm Exists v p
and substConn sub fm conn p q = let val p' = substFm sub p and q' = substFm sub q in if Metis_Portable.pointerEqual (p,p') andalso
Metis_Portable.pointerEqual (q,q') then fm else conn (p',q') end
and substQuant sub fm quant v p = let val v' = let fun f (w,s) = if Metis_Name.equal w v then s else case Metis_Subst.peek sub w of
NONE => Metis_NameSet.add s w
| SOME tm => Metis_NameSet.union s (Metis_Term.freeVars tm)
val vars = freeVars p val vars = Metis_NameSet.foldl f Metis_NameSet.empty vars in
Metis_Term.variantPrime vars v end
valsub = if Metis_Name.equal v v' then Metis_Subst.remove sub (Metis_NameSet.singleton v) else Metis_Subst.insert sub (v, Metis_Term.Var v')
val p' = substCheck sub p in if Metis_Name.equal v v' andalso Metis_Portable.pointerEqual (p,p') then fm else quant (v',p') end; in val subst = substCheck; end;
val truthName = Metis_Name.fromString "T" and falsityName = Metis_Name.fromString "F" and conjunctionName = Metis_Name.fromString "/\\" and disjunctionName = Metis_Name.fromString "\\/" and implicationName = Metis_Name.fromString "==>" and equivalenceName = Metis_Name.fromString "<=>" and universalName = Metis_Name.fromString "!" and existentialName = Metis_Name.fromString "?";
local fun add_asms asms goal = ifList.null asms then goal else Imp (listMkConj (List.rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
fun split asms pol fm = case (pol,fm) of (* Positive splittables *)
(true,True) => []
| (true, Not f) => split asms false f
| (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
| (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
| (true, Imp (f1,f2)) => split (f1 :: asms) true f2
| (true, Iff (f1,f2)) =>
split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
| (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f) (* Negative splittables *)
| (false,False) => []
| (false, Not f) => split asms true f
| (false, And (f1,f2)) => split (f1 :: asms) false f2
| (false, Or (f1,f2)) =>
split asms false f1 @ split (Not f1 :: asms) false f2
| (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
| (false, Iff (f1,f2)) =>
split (f1 :: asms) false f2 @ split (Not f2 :: asms) true f1
| (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f) (* Unsplittables *)
| _ => [add_asms asms (if pol then fm elseNot fm)]; in fun splitGoal fm = split [] true fm; end;
(*MetisTrace3 val splitGoal = fn fm => let val result = splitGoal fm val () = Metis_Print.trace pp "Metis_Formula.splitGoal: fm" fm val () = Metis_Print.trace (Metis_Print.ppList pp) "Metis_Formula.splitGoal: result" result in result end;
*)
end
structure Metis_FormulaOrdered = structtype t = Metis_Formula.formula val compare = Metis_Formula.compare end
(* ========================================================================= *) (* FIRST ORDER LOGIC LITERALS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Literal = sig
(* ------------------------------------------------------------------------- *) (* A type for storing first order logic literals. *) (* ------------------------------------------------------------------------- *)
val isBinop : Metis_Atom.relationName -> literal -> bool
(* Formulas *)
val toFormula : literal -> Metis_Formula.formula
val fromFormula : Metis_Formula.formula -> literal
(* ------------------------------------------------------------------------- *) (* The size of a literal in symbols. *) (* ------------------------------------------------------------------------- *)
val symbols : literal -> int
(* ------------------------------------------------------------------------- *) (* A total comparison function for literals. *) (* ------------------------------------------------------------------------- *)
val compare : literal * literal -> order (* negative < positive *)
val mkEq : Metis_Term.term * Metis_Term.term -> literal
val destEq : literal -> Metis_Term.term * Metis_Term.term
val isEq : literal -> bool
val mkNeq : Metis_Term.term * Metis_Term.term -> literal
val destNeq : literal -> Metis_Term.term * Metis_Term.term
val isNeq : literal -> bool
val mkRefl : Metis_Term.term -> literal
val destRefl : literal -> Metis_Term.term
val isRefl : literal -> bool
val mkIrrefl : Metis_Term.term -> literal
val destIrrefl : literal -> Metis_Term.term
val isIrrefl : literal -> bool
(* The following work with both equalities and disequalities *)
val sym : literal -> literal (* raises Error if given a refl or irrefl *)
val lhs : literal -> Metis_Term.term
val rhs : literal -> Metis_Term.term
(* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *)
val typedSymbols : literal -> int
val nonVarTypedSubterms : literal -> (Metis_Term.path * Metis_Term.term) list
val parse : Metis_Term.term Metis_Parse.quotation -> literal
end
(**** Original file: src/Literal.sml ****)
(* ========================================================================= *) (* FIRST ORDER LOGIC LITERALS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Literal :> Metis_Literal = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type for storing first order logic literals. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* The size of a literal in symbols. *) (* ------------------------------------------------------------------------- *)
fun symbols ((_,atm) : literal) = Metis_Atom.symbols atm;
(* ------------------------------------------------------------------------- *) (* A total comparison function for literals. *) (* ------------------------------------------------------------------------- *)
val compare = prodCompare boolCompare Metis_Atom.compare;
fun subterm lit path = Metis_Atom.subterm (atom lit) path;
fun subterms lit = Metis_Atom.subterms (atom lit);
fun replace (lit as (pol,atm)) path_tm = let val atm' = Metis_Atom.replace atm path_tm in if Metis_Portable.pointerEqual (atm,atm') then lit else (pol,atm') end;
fun subst sub (lit as (pol,atm)) : literal = let val atm' = Metis_Atom.subst sub atm in if Metis_Portable.pointerEqual (atm',atm) then lit else (pol,atm') end;
fun unify sub ((pol1,atm1) : literal) (pol2,atm2) = let val _ = pol1 = pol2 orelse raise Error "Metis_Literal.unify" in
Metis_Atom.unify sub atm1 atm2 end;
fun sym (pol,atm) : literal = (pol, Metis_Atom.sym atm);
fun lhs ((_,atm) : literal) = Metis_Atom.lhs atm;
fun rhs ((_,atm) : literal) = Metis_Atom.rhs atm;
(* ------------------------------------------------------------------------- *) (* Special support for terms with type annotations. *) (* ------------------------------------------------------------------------- *)
fun typedSymbols ((_,atm) : literal) = Metis_Atom.typedSymbols atm;
fun nonVarTypedSubterms ((_,atm) : literal) = Metis_Atom.nonVarTypedSubterms atm;
local structure S = Metis_ElementSet (Metis_LiteralMap); in open S; end;
fun negateMember lit set = member (Metis_Literal.negate lit) set;
val negate = let fun f (lit,set) = add set (Metis_Literal.negate lit) in
foldl f empty end;
val relations = let fun f (lit,set) = Metis_NameAritySet.add set (Metis_Literal.relation lit) in
foldl f Metis_NameAritySet.empty end;
val functions = let fun f (lit,set) = Metis_NameAritySet.union set (Metis_Literal.functions lit) in
foldl f Metis_NameAritySet.empty end;
fun freeIn v = exists (Metis_Literal.freeIn v);
val freeVars = let fun f (lit,set) = Metis_NameSet.union set (Metis_Literal.freeVars lit) in
foldl f Metis_NameSet.empty end;
val freeVarsList = let fun f (lits,set) = Metis_NameSet.union set (freeVars lits) in List.foldl f Metis_NameSet.empty end;
val symbols = let fun f (lit,z) = Metis_Literal.symbols lit + z in
foldl f 0 end;
val typedSymbols = let fun f (lit,z) = Metis_Literal.typedSymbols lit + z in
foldl f 0 end;
fun subst sub lits = let fun substLit (lit,(eq,lits')) = let val lit' = Metis_Literal.subst sub lit val eq = eq andalso Metis_Portable.pointerEqual (lit,lit') in
(eq, add lits' lit') end
val (eq,lits') = foldl substLit (true,empty) lits in if eq then lits else lits' end;
fun conjoin set =
Metis_Formula.listMkConj (List.map Metis_Literal.toFormula (toList set));
fun disjoin set =
Metis_Formula.listMkDisj (List.map Metis_Literal.toFormula (toList set));
val pp =
Metis_Print.ppMap
toList
(Metis_Print.ppBracket "{""}" (Metis_Print.ppOpList "," Metis_Literal.pp));
end
structure Metis_LiteralSetOrdered = structtype t = Metis_LiteralSet.setval compare = Metis_LiteralSet.compare end
(* ========================================================================= *) (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Thm = sig
(* ------------------------------------------------------------------------- *) (* An abstract type of first order logic theorems. *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* *) (* ----- axiom C *) (* C *) (* ------------------------------------------------------------------------- *)
val axiom : clause -> thm
(* ------------------------------------------------------------------------- *) (* *) (* ----------- assume L *) (* L \/ ~L *) (* ------------------------------------------------------------------------- *)
val assume : Metis_Literal.literal -> thm
(* ------------------------------------------------------------------------- *) (* C *) (* -------- subst s *) (* C[s] *) (* ------------------------------------------------------------------------- *)
val subst : Metis_Subst.subst -> thm -> thm
(* ------------------------------------------------------------------------- *) (* L \/ C ~L \/ D *) (* --------------------- resolve L *) (* C \/ D *) (* *) (* The literal L must occur in the first theorem, and the literal ~L must *) (* occur in the second theorem. *) (* ------------------------------------------------------------------------- *)
val resolve : Metis_Literal.literal -> thm -> thm -> thm
(* ------------------------------------------------------------------------- *) (* *) (* --------- refl t *) (* t = t *) (* ------------------------------------------------------------------------- *)
val refl : Metis_Term.term -> thm
(* ------------------------------------------------------------------------- *) (* *) (* ------------------------ equality L p t *) (* ~(s = t) \/ ~L \/ L' *) (* *) (* where s is the subterm of L at path p, and L' is L with the subterm at *) (* path p being replaced by t. *) (* ------------------------------------------------------------------------- *)
val equality : Metis_Literal.literal -> Metis_Term.path -> Metis_Term.term -> thm
end
(**** Original file: src/Thm.sml ****)
(* ========================================================================= *) (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Thm :> Metis_Thm = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* An abstract type of first order logic theorems. *) (* ------------------------------------------------------------------------- *)
local fun chk (_,NONE) = NONE
| chk ((pol,atm), SOME set) = if (pol andalso Metis_Atom.isRefl atm) orelse Metis_AtomSet.member atm setthen NONE else SOME (Metis_AtomSet.add set atm); in fun isTautology th = case Metis_LiteralSet.foldl chk (SOME Metis_AtomSet.empty) (clause th) of
SOME _ => false
| NONE => true; end;
(* Contradictions *)
fun isContradiction th = Metis_LiteralSet.null (clause th);
(* Unit theorems *)
fun destUnit (Metis_Thm (cl,_)) = if Metis_LiteralSet.size cl = 1 then Metis_LiteralSet.pick cl elseraise Error "Metis_Thm.destUnit";
val isUnit = can destUnit;
(* Unit equality theorems *)
fun destUnitEq th = Metis_Literal.destEq (destUnit th);
val isUnitEq = can destUnitEq;
(* Literals *)
fun member lit (Metis_Thm (cl,_)) = Metis_LiteralSet.member lit cl;
fun negateMember lit (Metis_Thm (cl,_)) = Metis_LiteralSet.negateMember lit cl;
(* ------------------------------------------------------------------------- *) (* A total order. *) (* ------------------------------------------------------------------------- *)
fun compare (th1,th2) = Metis_LiteralSet.compare (clause th1, clause th2);
fun equal th1 th2 = Metis_LiteralSet.equal (clause th1) (clause th2);
(* ------------------------------------------------------------------------- *) (* *) (* ----- axiom C *) (* C *) (* ------------------------------------------------------------------------- *)
fun axiom cl = Metis_Thm (cl,(Axiom,[]));
(* ------------------------------------------------------------------------- *) (* *) (* ----------- assume L *) (* L \/ ~L *) (* ------------------------------------------------------------------------- *)
fun assume lit =
Metis_Thm (Metis_LiteralSet.fromList [lit, Metis_Literal.negate lit], (Assume,[]));
(* ------------------------------------------------------------------------- *) (* C *) (* -------- subst s *) (* C[s] *) (* ------------------------------------------------------------------------- *)
fun subst sub (th as Metis_Thm (cl,inf)) = let val cl' = Metis_LiteralSet.subst sub cl in if Metis_Portable.pointerEqual (cl,cl') then th else case inf of
(Metis_Subst,_) => Metis_Thm (cl',inf)
| _ => Metis_Thm (cl',(Metis_Subst,[th])) end;
(* ------------------------------------------------------------------------- *) (* L \/ C ~L \/ D *) (* --------------------- resolve L *) (* C \/ D *) (* *) (* The literal L must occur in the first theorem, and the literal ~L must *) (* occur in the second theorem. *) (* ------------------------------------------------------------------------- *)
fun resolve lit (th1 as Metis_Thm (cl1,_)) (th2 as Metis_Thm (cl2,_)) = let val cl1' = Metis_LiteralSet.delete cl1 lit and cl2' = Metis_LiteralSet.delete cl2 (Metis_Literal.negate lit) in
Metis_Thm (Metis_LiteralSet.union cl1' cl2', (Resolve,[th1,th2])) end;
(* ------------------------------------------------------------------------- *) (* *) (* --------- refl t *) (* t = t *) (* ------------------------------------------------------------------------- *)
fun refl tm = Metis_Thm (Metis_LiteralSet.singleton (true, Metis_Atom.mkRefl tm), (Refl,[]));
(* ------------------------------------------------------------------------- *) (* *) (* ------------------------ equality L p t *) (* ~(s = t) \/ ~L \/ L' *) (* *) (* where s is the subterm of L at path p, and L' is L with the subterm at *) (* path p being replaced by t. *) (* ------------------------------------------------------------------------- *)
fun equality lit path t = let val s = Metis_Literal.subterm lit path
val lit' = Metis_Literal.replace lit (path,t)
val eqLit = Metis_Literal.mkNeq (s,t)
val cl = Metis_LiteralSet.fromList [eqLit, Metis_Literal.negate lit, lit'] in
Metis_Thm (cl,(Equality,[])) end;
end
(**** Original file: src/Proof.sig ****)
(* ========================================================================= *) (* PROOFS IN FIRST ORDER LOGIC *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Proof = sig
(* ------------------------------------------------------------------------- *) (* A type of first order logic proofs. *) (* ------------------------------------------------------------------------- *)
datatype inference =
Axiom of Metis_LiteralSet.set
| Assume of Metis_Atom.atom
| Metis_Subst of Metis_Subst.subst * Metis_Thm.thm
| Resolve of Metis_Atom.atom * Metis_Thm.thm * Metis_Thm.thm
| Refl of Metis_Term.term
| Equality of Metis_Literal.literal * Metis_Term.path * Metis_Term.term
(* ========================================================================= *) (* PROOFS IN FIRST ORDER LOGIC *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
structure Metis_Proof :> Metis_Proof = struct
open Metis_Useful;
(* ------------------------------------------------------------------------- *) (* A type of first order logic proofs. *) (* ------------------------------------------------------------------------- *)
datatype inference =
Axiom of Metis_LiteralSet.set
| Assume of Metis_Atom.atom
| Metis_Subst of Metis_Subst.subst * Metis_Thm.thm
| Resolve of Metis_Atom.atom * Metis_Thm.thm * Metis_Thm.thm
| Refl of Metis_Term.term
| Equality of Metis_Literal.literal * Metis_Term.path * Metis_Term.term;
fun ppInf ppAxiom ppThm inf = let val infString = Metis_Thm.inferenceTypeToString (inferenceType inf) in
Metis_Print.inconsistentBlock 2
[Metis_Print.ppString infString,
(case inf of
Axiom cl => ppAxiom cl
| Assume x => ppAssume x
| Metis_Subst x => ppSubst ppThm x
| Resolve x => ppResolve ppThm x
| Refl x => ppRefl x
| Equality x => ppEquality x)] end;
fun ppAxiom cl =
Metis_Print.sequence
Metis_Print.break
(Metis_Print.ppMap
Metis_LiteralSet.toList
(Metis_Print.ppBracket "{""}" (Metis_Print.ppOpList "," Metis_Literal.pp)) cl); in val ppInference = ppInf ppAxiom Metis_Thm.pp;
fun pp prf = let fun thmString n = "(" ^ Int.toString n ^ ")"
val prf = enumerate prf
fun ppThm th =
Metis_Print.ppString let val cl = Metis_Thm.clause th
fun pred (_,(th',_)) = Metis_LiteralSet.equal (Metis_Thm.clause th') cl in caseList.find pred prf of
NONE => "(?)"
| SOME (n,_) => thmString n end
fun ppStep (n,(th,inf)) = let val s = thmString n in
Metis_Print.sequence
(Metis_Print.consistentBlock (1 + size s)
[Metis_Print.ppString (s ^ " "),
Metis_Thm.pp th,
Metis_Print.breaks 2,
Metis_Print.ppBracket "[""]" (ppInf (K Metis_Print.skip) ppThm) inf])
Metis_Print.newline end in
Metis_Print.consistentBlock 0
[Metis_Print.ppString "START OF PROOF",
Metis_Print.newline,
Metis_Print.program (List.map ppStep prf),
Metis_Print.ppString "END OF PROOF"] end (*MetisDebug handle Error err => raise Bug ("Metis_Proof.pp: shouldn't fail:\n" ^ err);
*)
end;
val inferenceToString = Metis_Print.toString ppInference;
local fun reconstructSubst cl cl' = let fun recon [] = let (*MetisTrace3 val () = Metis_Print.trace Metis_LiteralSet.pp "reconstructSubst: cl" cl val () = Metis_Print.trace Metis_LiteralSet.pp "reconstructSubst: cl'" cl'
*) in raise Bug "can't reconstruct Metis_Subst rule" end
| recon (([],sub) :: others) = if Metis_LiteralSet.equal (Metis_LiteralSet.subst sub cl) cl' then sub else recon others
| recon ((lit :: lits, sub) :: others) = let fun checkLit (lit',acc) = case total (Metis_Literal.matchsub lit) lit' of
NONE => acc
| SOME sub => (lits,sub) :: acc in
recon (Metis_LiteralSet.foldl checkLit others cl') end in
Metis_Subst.normalize (recon [(Metis_LiteralSet.toList cl, Metis_Subst.empty)]) end (*MetisDebug handle Error err => raise Bug ("Metis_Proof.recontructSubst: shouldn't fail:\n" ^ err);
*)
fun reconstructResolvant cl1 cl2 cl =
(ifnot (Metis_LiteralSet.subset cl1 cl) then
Metis_LiteralSet.pick (Metis_LiteralSet.difference cl1 cl) elseifnot (Metis_LiteralSet.subset cl2 cl) then
Metis_Literal.negate (Metis_LiteralSet.pick (Metis_LiteralSet.difference cl2 cl)) else (* A useless resolution, but we must reconstruct it anyway *) let val cl1' = Metis_LiteralSet.negate cl1 and cl2' = Metis_LiteralSet.negate cl2 val lits = Metis_LiteralSet.intersectList [cl1,cl1',cl2,cl2'] in ifnot (Metis_LiteralSet.null lits) then Metis_LiteralSet.pick lits elseraise Bug "can't reconstruct Resolve rule" end) (*MetisDebug handle Error err => raise Bug ("Metis_Proof.recontructResolvant: shouldn't fail:\n" ^ err);
*)
fun reconstructEquality cl = let (*MetisTrace3 val () = Metis_Print.trace Metis_LiteralSet.pp "Metis_Proof.reconstructEquality: cl" cl
*)
fun sync s t path (f,a) (f',a') = ifnot (Metis_Name.equal f f' andalso length a = length a') then NONE else let val itms = enumerate (zip a a') in caseList.filter (not o uncurry Metis_Term.equal o snd) itms of
[(i,(tm,tm'))] => let val path = i :: path in if Metis_Term.equal tm s andalso Metis_Term.equal tm' t then
SOME (List.rev path) else case (tm,tm') of
(Metis_Term.Fn f_a, Metis_Term.Fn f_a') => sync s t path f_a f_a'
| _ => NONE end
| _ => NONE end
fun recon (neq,(pol,atm),(pol',atm')) = if pol = pol' then NONE else let val (s,t) = Metis_Literal.destNeq neq
val path = ifnot (Metis_Term.equal s t) then sync s t [] atm atm' elseifnot (Metis_Atom.equal atm atm') then NONE else Metis_Atom.find (Metis_Term.equal s) atm in case path of
SOME path => SOME ((pol',atm),path,t)
| NONE => NONE end
local val emptyThms : Metis_Thm.thm Metis_LiteralSetMap.map = Metis_LiteralSetMap.new ();
fun addThms (th,ths) = let val cl = Metis_Thm.clause th in if Metis_LiteralSetMap.inDomain cl ths then ths else let val (_,pars) = Metis_Thm.inference th val ths = List.foldl addThms ths pars in if Metis_LiteralSetMap.inDomain cl ths then ths else Metis_LiteralSetMap.insert ths (cl,th) end end;
fun mkThms th = addThms (th,emptyThms);
fun addProof (th,(ths,acc)) = let val cl = Metis_Thm.clause th in case Metis_LiteralSetMap.peek ths cl of
NONE => (ths,acc)
| SOME th => let val (_,pars) = Metis_Thm.inference th val (ths,acc) = List.foldl addProof (ths,acc) pars val ths = Metis_LiteralSetMap.delete ths cl val acc = (th, thmToInference th) :: acc in
(ths,acc) end end;
fun mkProof ths th = let val (ths,acc) = addProof (th,(ths,[])) (*MetisTrace4 val () = Metis_Print.trace Metis_Print.ppInt "Metis_Proof.proof: unnecessary clauses" (Metis_LiteralSetMap.size ths)
*) in List.rev acc end; in fun proof th = let (*MetisTrace3 val () = Metis_Print.trace Metis_Thm.pp "Metis_Proof.proof: th" th
*) val ths = mkThms th val infs = mkProof ths th (*MetisTrace3 val () = Metis_Print.trace Metis_Print.ppInt "Metis_Proof.proof: size" (length infs)
*) in
infs end; end;
fun freeIn v = let fun free th_inf = case th_inf of
(_, Axiom lits) => Metis_LiteralSet.freeIn v lits
| (_, Assume atm) => Metis_Atom.freeIn v atm
| (th, Metis_Subst _) => Metis_Thm.freeIn v th
| (_, Resolve _) => false
| (_, Refl tm) => Metis_Term.freeIn v tm
| (_, Equality (lit,_,tm)) =>
Metis_Literal.freeIn v lit orelse Metis_Term.freeIn v tm in List.exists free end;
(* ========================================================================= *) (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
signature Metis_Rule = sig
(* ------------------------------------------------------------------------- *) (* An equation consists of two terms (t,u) plus a theorem (stronger than) *) (* t = u \/ C. *) (* ------------------------------------------------------------------------- *)
type equation = (Metis_Term.term * Metis_Term.term) * Metis_Thm.thm
val ppEquation : equation Metis_Print.pp
val equationToString : equation -> string
(* Returns t = u if the equation theorem contains this literal *) val equationLiteral : equation -> Metis_Literal.literal option
val reflEqn : Metis_Term.term -> equation
val symEqn : equation -> equation
val transEqn : equation -> equation -> equation
(* ------------------------------------------------------------------------- *) (* A conversion takes a term t and either: *) (* 1. Returns a term u together with a theorem (stronger than) t = u \/ C. *) (* 2. Raises an Error exception. *) (* ------------------------------------------------------------------------- *)
type conv = Metis_Term.term -> Metis_Term.term * Metis_Thm.thm
val allConv : conv
val noConv : conv
val thenConv : conv -> conv -> conv
val orelseConv : conv -> conv -> conv
val tryConv : conv -> conv
val repeatConv : conv -> conv
val firstConv : conv list -> conv
val everyConv : conv list -> conv
val rewrConv : equation -> Metis_Term.path -> conv
val pathConv : conv -> Metis_Term.path -> conv
val subtermConv : conv -> int -> conv
val subtermsConv : conv -> conv (* All function arguments *)
(* ------------------------------------------------------------------------- *) (* Applying a conversion to every subterm, with some traversal strategy. *) (* ------------------------------------------------------------------------- *)
val bottomUpConv : conv -> conv
val topDownConv : conv -> conv
val repeatTopDownConv : conv -> conv (* useful for rewriting *)
(* ------------------------------------------------------------------------- *) (* A literule (bad pun) takes a literal L and either: *) (* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C. *) (* 2. Raises an Error exception. *) (* ------------------------------------------------------------------------- *)
type literule = Metis_Literal.literal -> Metis_Literal.literal * Metis_Thm.thm
val allLiterule : literule
val noLiterule : literule
val thenLiterule : literule -> literule -> literule
val orelseLiterule : literule -> literule -> literule
val tryLiterule : literule -> literule
val repeatLiterule : literule -> literule
val firstLiterule : literule list -> literule
val everyLiterule : literule list -> literule
val rewrLiterule : equation -> Metis_Term.path -> literule
val pathLiterule : conv -> Metis_Term.path -> literule
val argumentLiterule : conv -> int -> literule
val allArgumentsLiterule : conv -> literule
(* ------------------------------------------------------------------------- *) (* A rule takes one theorem and either deduces another or raises an Error *) (* exception. *) (* ------------------------------------------------------------------------- *)
type rule = Metis_Thm.thm -> Metis_Thm.thm
val allRule : rule
val noRule : rule
val thenRule : rule -> rule -> rule
val orelseRule : rule -> rule -> rule
val tryRule : rule -> rule
val changedRule : rule -> rule
val repeatRule : rule -> rule
val firstRule : rule list -> rule
val everyRule : rule list -> rule
val literalRule : literule -> Metis_Literal.literal -> rule
val rewrRule : equation -> Metis_Literal.literal -> Metis_Term.path -> rule
val pathRule : conv -> Metis_Literal.literal -> Metis_Term.path -> rule
val literalsRule : literule -> Metis_LiteralSet.set -> rule
val allLiteralsRule : literule -> rule
val convRule : conv -> rule (* All arguments of all literals *)
(* ------------------------------------------------------------------------- *) (* *) (* --------- reflexivity *) (* x = x *) (* ------------------------------------------------------------------------- *)
val reflexivityRule : Metis_Term.term -> Metis_Thm.thm
val relationCongruence : Metis_Atom.relation -> Metis_Thm.thm
(* ------------------------------------------------------------------------- *) (* x = y \/ C *) (* -------------- symEq (x = y) *) (* y = x \/ C *) (* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *) (* ~(x = x) \/ C *) (* ----------------- removeIrrefl *) (* C *) (* *) (* where all irreflexive equalities. *) (* ------------------------------------------------------------------------- *)
val removeIrrefl : rule
(* ------------------------------------------------------------------------- *) (* x = y \/ y = x \/ C *) (* ----------------------- removeSym *) (* x = y \/ C *) (* *) (* where all duplicate copies of equalities and disequalities are removed. *) (* ------------------------------------------------------------------------- *)
val removeSym : rule
(* ------------------------------------------------------------------------- *) (* ~(v = t) \/ C *) (* ----------------- expandAbbrevs *) (* C[t/v] *) (* *) (* where t must not contain any occurrence of the variable v. *) (* ------------------------------------------------------------------------- *)
val simplify : Metis_Thm.thm -> Metis_Thm.thm option
(* ------------------------------------------------------------------------- *) (* C *) (* -------- freshVars *) (* C[s] *) (* *) (* where s is a renaming substitution chosen so that all of the variables in *) (* C are replaced by fresh variables. *) (* ------------------------------------------------------------------------- *)
val freshVars : rule
(* ------------------------------------------------------------------------- *) (* C *) (* ---------------------------- factor *) (* C_s_1, C_s_2, ..., C_s_n *) (* *) (* where each s_i is a substitution that factors C, meaning that the theorem *) (* *) (* C_s_i = (removeIrrefl o removeSym o Metis_Thm.subst s_i) C *) (* *) (* has fewer literals than C. *) (* *) (* Also, if s is any substitution that factors C, then one of the s_i will *) (* result in a theorem C_s_i that strictly subsumes the theorem C_s. *) (* ------------------------------------------------------------------------- *)
val factor' : Metis_Thm.clause -> Metis_Subst.subst list
val factor : Metis_Thm.thm -> Metis_Thm.thm list
end
(**** Original file: src/Rule.sml ****)
(* ========================================================================= *) (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
fun symmetryRule x y = let val reflTh = reflexivityRule x val reflLit = Metis_Thm.destUnit reflTh val eqTh = Metis_Thm.equality reflLit [0] y in
Metis_Thm.resolve reflLit reflTh eqTh end;
val transitivity = let val eqTh = Metis_Thm.equality (Metis_Literal.mkEq (yVar,zVar)) [0] xVar in
Metis_Thm.resolve (Metis_Literal.mkEq (yVar,xVar)) symmetry eqTh end;
(* ------------------------------------------------------------------------- *) (* x = y \/ C *) (* -------------- symEq (x = y) *) (* y = x \/ C *) (* ------------------------------------------------------------------------- *)
fun symEq lit th = let val (x,y) = Metis_Literal.destEq lit in if Metis_Term.equal x y then th else let valsub = Metis_Subst.fromList [(xVarName,x),(yVarName,y)]
val symTh = Metis_Thm.subst sub symmetry in
Metis_Thm.resolve lit th symTh end end;
(* ------------------------------------------------------------------------- *) (* An equation consists of two terms (t,u) plus a theorem (stronger than) *) (* t = u \/ C. *) (* ------------------------------------------------------------------------- *)
type equation = (Metis_Term.term * Metis_Term.term) * Metis_Thm.thm;
fun ppEquation ((_,th) : equation) = Metis_Thm.pp th;
val equationToString = Metis_Print.toString ppEquation;
fun equationLiteral (t_u,th) = let val lit = Metis_Literal.mkEq t_u in if Metis_LiteralSet.member lit (Metis_Thm.clause th) then SOME lit else NONE end;
fun reflEqn t = ((t,t), Metis_Thm.refl t);
fun symEqn (eqn as ((t,u), th)) = if Metis_Term.equal t u then eqn else
((u,t), case equationLiteral eqn of
SOME t_u => symEq t_u th
| NONE => th);
fun transEqn (eqn1 as ((x,y), th1)) (eqn2 as ((_,z), th2)) = if Metis_Term.equal x y then eqn2 elseif Metis_Term.equal y z then eqn1 elseif Metis_Term.equal x z then reflEqn x else
((x,z), case equationLiteral eqn1 of
NONE => th1
| SOME x_y => case equationLiteral eqn2 of
NONE => th2
| SOME y_z => let valsub = Metis_Subst.fromList [(xVarName,x),(yVarName,y),(zVarName,z)] val th = Metis_Thm.subst sub transitivity val th = Metis_Thm.resolve x_y th1 th val th = Metis_Thm.resolve y_z th2 th in
th end);
(* ------------------------------------------------------------------------- *) (* A conversion takes a term t and either: *) (* 1. Returns a term u together with a theorem (stronger than) t = u \/ C. *) (* 2. Raises an Error exception. *) (* ------------------------------------------------------------------------- *)
type conv = Metis_Term.term -> Metis_Term.term * Metis_Thm.thm;
fun allConv tm = (tm, Metis_Thm.refl tm);
val noConv : conv = fn _ => raise Error "noConv";
(*MetisDebug fun traceConv s conv tm = let val res as (tm',th) = conv tm val () = trace (s ^ ": " ^ Metis_Term.toString tm ^ " --> " ^ Metis_Term.toString tm' ^ " " ^ Metis_Thm.toString th ^ "\n") in res end handle Error err => (trace (s ^ ": " ^ Metis_Term.toString tm ^ " --> Error: " ^ err ^ "\n"); raise Error (s ^ ": " ^ err));
*)
fun thenConvTrans tm (tm',th1) (tm'',th2) = let val eqn1 = ((tm,tm'),th1) and eqn2 = ((tm',tm''),th2) val (_,th) = transEqn eqn1 eqn2 in
(tm'',th) end;
fun thenConv conv1 conv2 tm = let val res1 as (tm',_) = conv1 tm val res2 = conv2 tm' in
thenConvTrans tm res1 res2 end;
fun rewrConv (eqn as ((x,y), eqTh)) path tm = if Metis_Term.equal x y then allConv tm elseifList.null path then (y,eqTh) else let val reflTh = Metis_Thm.refl tm val reflLit = Metis_Thm.destUnit reflTh val th = Metis_Thm.equality reflLit (1 :: path) y val th = Metis_Thm.resolve reflLit reflTh th val th = case equationLiteral eqn of
NONE => th
| SOME x_y => Metis_Thm.resolve x_y eqTh th val tm' = Metis_Term.replace tm (path,y) in
(tm',th) end;
fun pathConv conv path tm = let val x = Metis_Term.subterm tm path val (y,th) = conv x in
rewrConv ((x,y),th) path tm end;
fun subtermConv conv i = pathConv conv [i];
fun subtermsConv _ (tm as Metis_Term.Var _) = allConv tm
| subtermsConv conv (tm as Metis_Term.Fn (_,a)) =
everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
(* ------------------------------------------------------------------------- *) (* Applying a conversion to every subterm, with some traversal strategy. *) (* ------------------------------------------------------------------------- *)
fun repeatTopDownConv conv = let fun f tm = thenConv (repeatConv conv) g tm and g tm = thenConv (subtermsConv f) h tm and h tm = tryConv (thenConv conv f) tm in
f end;
(* ------------------------------------------------------------------------- *) (* A literule (bad pun) takes a literal L and either: *) (* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C. *) (* 2. Raises an Error exception. *) (* ------------------------------------------------------------------------- *)
type literule = Metis_Literal.literal -> Metis_Literal.literal * Metis_Thm.thm;
fun allLiterule lit = (lit, Metis_Thm.assume lit);
fun thenLiterule literule1 literule2 lit = let val res1 as (lit',th1) = literule1 lit val res2 as (lit'',th2) = literule2 lit' in if Metis_Literal.equal lit lit' then res2 elseif Metis_Literal.equal lit' lit'' then res1 elseif Metis_Literal.equal lit lit''then allLiterule lit else
(lit'', ifnot (Metis_Thm.member lit' th1) then th1 elseifnot (Metis_Thm.negateMember lit' th2) then th2 else Metis_Thm.resolve lit' th1 th2) end;
fun rewrLiterule (eqn as ((x,y),eqTh)) path lit = if Metis_Term.equal x y then allLiterule lit else let val th = Metis_Thm.equality lit path y val th = case equationLiteral eqn of
NONE => th
| SOME x_y => Metis_Thm.resolve x_y eqTh th val lit' = Metis_Literal.replace lit (path,y) in
(lit',th) end;
(* ------------------------------------------------------------------------- *) (* A rule takes one theorem and either deduces another or raises an Error *) (* exception. *) (* ------------------------------------------------------------------------- *)
fun changedRule rule th = let val th' = rule th in ifnot (Metis_LiteralSet.equal (Metis_Thm.clause th) (Metis_Thm.clause th')) then th' elseraise Error "changedRule" end;
fun literalRule literule lit th = let val (lit',litTh) = literule lit in if Metis_Literal.equal lit lit' then th elseifnot (Metis_Thm.negateMember lit litTh) then litTh else Metis_Thm.resolve lit th litTh end;
fun literalsRule literule = let fun f (lit,th) = if Metis_Thm.member lit th then literalRule literule lit th else th in
fn lits => fn th => Metis_LiteralSet.foldl f th lits end;
fun allLiteralsRule literule th = literalsRule literule (Metis_Thm.clause th) th;
fun convRule conv = allLiteralsRule (allArgumentsLiterule conv);
fun functionCongruence (f,n) = let val xs = List.tabulate (n,xIVar) and ys = List.tabulate (n,yIVar)
fun cong ((i,yi),(th,lit)) = let val path = [1,i] val th = Metis_Thm.resolve lit th (Metis_Thm.equality lit path yi) val lit = Metis_Literal.replace lit (path,yi) in
(th,lit) end
val reflTh = Metis_Thm.refl (Metis_Term.Fn (f,xs)) val reflLit = Metis_Thm.destUnit reflTh in
fst (List.foldl cong (reflTh,reflLit) (enumerate ys)) end;
fun relationCongruence (R,n) = let val xs = List.tabulate (n,xIVar) and ys = List.tabulate (n,yIVar)
fun cong ((i,yi),(th,lit)) = let val path = [i] val th = Metis_Thm.resolve lit th (Metis_Thm.equality lit path yi) val lit = Metis_Literal.replace lit (path,yi) in
(th,lit) end
val assumeLit = (false,(R,xs)) val assumeTh = Metis_Thm.assume assumeLit in
fst (List.foldl cong (assumeTh,assumeLit) (enumerate ys)) end;
fun symNeq lit th = let val (x,y) = Metis_Literal.destNeq lit in if Metis_Term.equal x y then th else let valsub = Metis_Subst.fromList [(xVarName,y),(yVarName,x)] val symTh = Metis_Thm.subst sub symmetry in
Metis_Thm.resolve lit th symTh end end;
fun sym (lit as (pol,_)) th = if pol then symEq lit th else symNeq lit th;
(* ------------------------------------------------------------------------- *) (* ~(x = x) \/ C *) (* ----------------- removeIrrefl *) (* C *) (* *) (* where all irreflexive equalities. *) (* ------------------------------------------------------------------------- *)
local fun irrefl ((true,_),th) = th
| irrefl (lit as (false,atm), th) = case total Metis_Atom.destRefl atm of
SOME x => Metis_Thm.resolve lit th (Metis_Thm.refl x)
| NONE => th; in fun removeIrrefl th = Metis_LiteralSet.foldl irrefl th (Metis_Thm.clause th); end;
(* ------------------------------------------------------------------------- *) (* x = y \/ y = x \/ C *) (* ----------------------- removeSym *) (* x = y \/ C *) (* *) (* where all duplicate copies of equalities and disequalities are removed. *) (* ------------------------------------------------------------------------- *)
local fun rem (lit as (pol,atm), eqs_th as (eqs,th)) = case total Metis_Atom.sym atm of
NONE => eqs_th
| SOME atm' => if Metis_LiteralSet.member lit eqs then
(eqs, if pol then symEq lit th else symNeq lit th) else
(Metis_LiteralSet.add eqs (pol,atm'), th); in fun removeSym th =
snd (Metis_LiteralSet.foldl rem (Metis_LiteralSet.empty,th) (Metis_Thm.clause th)); end;
(* ------------------------------------------------------------------------- *) (* ~(v = t) \/ C *) (* ----------------- expandAbbrevs *) (* C[t/v] *) (* *) (* where t must not contain any occurrence of the variable v. *) (* ------------------------------------------------------------------------- *)
local fun expand lit = let val (x,y) = Metis_Literal.destNeq lit val _ = Metis_Term.isTypedVar x orelse Metis_Term.isTypedVar y orelse raise Error "Metis_Rule.expandAbbrevs: no vars" val _ = not (Metis_Term.equal x y) orelse raise Error "Metis_Rule.expandAbbrevs: equal vars" in
Metis_Subst.unify Metis_Subst.empty x y end; in fun expandAbbrevs th = case Metis_LiteralSet.firstl (total expand) (Metis_Thm.clause th) of
NONE => removeIrrefl th
| SOME sub => expandAbbrevs (Metis_Thm.subst sub th); end;
fun simplify th = if Metis_Thm.isTautology th then NONE else let val th' = th val th' = expandAbbrevs th' val th' = removeSym th' in if Metis_Thm.equal th th' then SOME th else simplify th' end;
(* ------------------------------------------------------------------------- *) (* C *) (* -------- freshVars *) (* C[s] *) (* *) (* where s is a renaming substitution chosen so that all of the variables in *) (* C are replaced by fresh variables. *) (* ------------------------------------------------------------------------- *)
fun freshVars th = Metis_Thm.subst (Metis_Subst.freshVars (Metis_Thm.freeVars th)) th;
(* ------------------------------------------------------------------------- *) (* C *) (* ---------------------------- factor *) (* C_s_1, C_s_2, ..., C_s_n *) (* *) (* where each s_i is a substitution that factors C, meaning that the theorem *) (* *) (* C_s_i = (removeIrrefl o removeSym o Metis_Thm.subst s_i) C *) (* *) (* has fewer literals than C. *) (* *) (* Also, if s is any substitution that factors C, then one of the s_i will *) (* result in a theorem C_s_i that strictly subsumes the theorem C_s. *) (* ------------------------------------------------------------------------- *)
local datatype edge =
FactorEdge of Metis_Atom.atom * Metis_Atom.atom
| ReflEdge of Metis_Term.term * Metis_Term.term;
datatype joinStatus =
Joined
| Joinable of Metis_Subst.subst
| Apart;
fun joinEdge sub edge = let val result = case edge of
FactorEdge (atm,atm') => total (Metis_Atom.unify sub atm) atm'
| ReflEdge (tm,tm') => total (Metis_Subst.unify sub tm) tm' in case result of
NONE => Apart
| SOME sub' => if Metis_Portable.pointerEqual (sub,sub') then Joined else Joinable sub' end;
fun updateApart sub = let fun update acc [] = SOME acc
| update acc (edge :: edges) = case joinEdge sub edge of
Joined => NONE
| Joinable _ => update (edge :: acc) edges
| Apart => update acc edges in
update [] end;
fun addFactorEdge (pol,atm) ((pol',atm'),acc) = if pol <> pol' then acc else let val edge = FactorEdge (atm,atm') in case joinEdge Metis_Subst.empty edge of
Joined => raise Bug "addFactorEdge: joined"
| Joinable sub => (sub,edge) :: acc
| Apart => acc end;
fun addReflEdge (false,_) acc = acc
| addReflEdge (true,atm) acc = let val edge = ReflEdge (Metis_Atom.destEq atm) in case joinEdge Metis_Subst.empty edge of
Joined => raise Bug "addRefl: joined"
| Joinable _ => edge :: acc
| Apart => acc end;
fun addIrreflEdge (true,_) acc = acc
| addIrreflEdge (false,atm) acc = let val edge = ReflEdge (Metis_Atom.destEq atm) in case joinEdge Metis_Subst.empty edge of
Joined => raise Bug "addRefl: joined"
| Joinable sub => (sub,edge) :: acc
| Apart => acc end;
fun init_edges acc _ [] = let fun init ((apart,sub,edge),(edges,acc)) =
(edge :: edges, (apart,sub,edges) :: acc) in
snd (List.foldl init ([],[]) acc) end
| init_edges acc apart ((sub,edge) :: sub_edges) = let (*MetisDebug val () = if not (Metis_Subst.null sub) then () else raise Bug "Metis_Rule.factor.init_edges: empty subst"
*) val (acc,apart) = case updateApart sub apart of
SOME apart' => ((apart',sub,edge) :: acc, edge :: apart)
| NONE => (acc,apart) in
init_edges acc apart sub_edges end;
fun mk_edges apart sub_edges [] = init_edges [] apart sub_edges
| mk_edges apart sub_edges (lit :: lits) = let val sub_edges = List.foldl (addFactorEdge lit) sub_edges lits
val (apart,sub_edges) = case total Metis_Literal.sym lit of
NONE => (apart,sub_edges)
| SOME lit' => let val apart = addReflEdge lit apart val sub_edges = addIrreflEdge lit sub_edges val sub_edges = List.foldl (addFactorEdge lit') sub_edges lits in
(apart,sub_edges) end in
mk_edges apart sub_edges lits end;
fun fact acc [] = acc
| fact acc ((_,sub,[]) :: others) = fact (sub :: acc) others
| fact acc ((apart, sub, edge :: edges) :: others) = let val others = case joinEdge sub edge of
Joinable sub' => let val others = (edge :: apart, sub, edges) :: others in case updateApart sub' apart of
NONE => others
| SOME apart' => (apart',sub',edges) :: others end
| _ => (apart,sub,edges) :: others in
fact acc others end; in fun factor' cl = let (*MetisTrace6 val () = Metis_Print.trace Metis_LiteralSet.pp "Metis_Rule.factor': cl" cl
*) val edges = mk_edges [] [] (Metis_LiteralSet.toList cl) (*MetisTrace6 val ppEdgesSize = Metis_Print.ppMap length Metis_Print.ppInt val ppEdgel = Metis_Print.ppList ppEdge val ppEdges = Metis_Print.ppList (Metis_Print.ppTriple ppEdgel Metis_Subst.pp ppEdgel) val () = Metis_Print.trace ppEdgesSize "Metis_Rule.factor': |edges|" edges val () = Metis_Print.trace ppEdges "Metis_Rule.factor': edges" edges
*) val result = fact [] edges (*MetisTrace6 val ppResult = Metis_Print.ppList Metis_Subst.pp val () = Metis_Print.trace ppResult "Metis_Rule.factor': result" result
*) in
result end; end;
fun factor th = let fun fact sub = removeIrrefl (removeSym (Metis_Thm.subst sub th)) in List.map fact (factor' (Metis_Thm.clause th)) end;
end
(**** Original file: src/Normalize.sig ****)
(* ========================================================================= *) (* NORMALIZING FORMULAS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
val nnf : Metis_Formula.formula -> Metis_Formula.formula
(* ------------------------------------------------------------------------- *) (* Conjunctive normal form derivations. *) (* ------------------------------------------------------------------------- *)
type thm
datatype inference =
Axiom of Metis_Formula.formula
| Definition ofstring * Metis_Formula.formula
| Simplify of thm * thm list
| Conjunct of thm
| Specialize of thm
| Skolemize of thm
| Clausify of thm
val mkAxiom : Metis_Formula.formula -> thm
val destThm : thm -> Metis_Formula.formula * inference
val proveThms :
thm list -> (Metis_Formula.formula * inference * Metis_Formula.formula list) list
(* ------------------------------------------------------------------------- *) (* Storing huge real numbers as their log. *) (* ------------------------------------------------------------------------- *)
datatype logReal = LogReal of real;
fun compareLogReal (LogReal logX, LogReal logY) =
Real.compare (logX,logY);
val zeroLogReal = LogReal ~1.0;
val oneLogReal = LogReal 0.0;
local fun isZero logX = logX < 0.0;
(* Assume logX >= logY >= 0.0 *) fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX)); in fun isZeroLogReal (LogReal logX) = isZero logX;
fun multiplyLogReal (LogReal logX) (LogReal logY) = if isZero logX orelse isZero logY then zeroLogReal else LogReal (logX + logY);
fun addLogReal (lx as LogReal logX) (ly as LogReal logY) = if isZero logX then ly elseif isZero logY then lx elseif logX < logY then LogReal (add logY logX) else LogReal (add logX logY);
fun toStringLogReal (LogReal logX) = Real.toString logX;
(* ------------------------------------------------------------------------- *) (* Counting the clauses that would be generated by conjunctive normal form. *) (* ------------------------------------------------------------------------- *)
val countTrue = Count {positive = zeroLogReal, negative = oneLogReal};
val countFalse = Count {positive = oneLogReal, negative = zeroLogReal};
val countLiteral = Count {positive = oneLogReal, negative = oneLogReal};
fun countAnd2 (count1,count2) = let val Count {positive = p1, negative = n1} = count1 and Count {positive = p2, negative = n2} = count2 val p = addLogReal p1 p2 and n = multiplyLogReal n1 n2 in
Count {positive = p, negative = n} end;
fun countOr2 (count1,count2) = let val Count {positive = p1, negative = n1} = count1 and Count {positive = p2, negative = n2} = count2 val p = multiplyLogReal p1 p2 and n = addLogReal n1 n2 in
Count {positive = p, negative = n} end;
(* Whether countXor2 is associative or not is an open question. *)
fun countXor2 (count1,count2) = let val Count {positive = p1, negative = n1} = count1 and Count {positive = p2, negative = n2} = count2 val p = addLogReal (multiplyLogReal p1 p2) (multiplyLogReal n1 n2) and n = addLogReal (multiplyLogReal p1 n2) (multiplyLogReal n1 p2) in
Count {positive = p, negative = n} end;
fun countDefinition body_count = countXor2 (countLiteral,body_count);
val countToString = let val rToS = toStringLogReal in
fn Count {positive = p, negative = n} => "(+" ^ rToS p ^ ",-" ^ rToS n ^ ")" end;
val ppCount = Metis_Print.ppMap countToString Metis_Print.ppString;
(* ------------------------------------------------------------------------- *) (* A type of normalized formula. *) (* ------------------------------------------------------------------------- *)
datatype formula = True
| False
| Metis_Literal of Metis_NameSet.set * Metis_Literal.literal
| Andof Metis_NameSet.set * count * formula Metis_Set.set
| Orof Metis_NameSet.set * count * formula Metis_Set.set
| Xor of Metis_NameSet.set * count * bool * formula Metis_Set.set
| Existsof Metis_NameSet.set * count * Metis_NameSet.set * formula
| Forall of Metis_NameSet.set * count * Metis_NameSet.set * formula;
fun compare f1_f2 = if Metis_Portable.pointerEqual f1_f2 then EQUAL else case f1_f2 of
(True,True) => EQUAL
| (True,_) => LESS
| (_,True) => GREATER
| (False,False) => EQUAL
| (False,_) => LESS
| (_,False) => GREATER
| (Metis_Literal (_,l1), Metis_Literal (_,l2)) => Metis_Literal.compare (l1,l2)
| (Metis_Literal _, _) => LESS
| (_, Metis_Literal _) => GREATER
| (And (_,_,s1), And (_,_,s2)) => Metis_Set.compare (s1,s2)
| (And _, _) => LESS
| (_, And _) => GREATER
| (Or (_,_,s1), Or (_,_,s2)) => Metis_Set.compare (s1,s2)
| (Or _, _) => LESS
| (_, Or _) => GREATER
| (Xor (_,_,p1,s1), Xor (_,_,p2,s2)) =>
(case boolCompare (p1,p2) of
LESS => LESS
| EQUAL => Metis_Set.compare (s1,s2)
| GREATER => GREATER)
| (Xor _, _) => LESS
| (_, Xor _) => GREATER
| (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) =>
(case Metis_NameSet.compare (n1,n2) of
LESS => LESS
| EQUAL => compare (f1,f2)
| GREATER => GREATER)
| (Exists _, _) => LESS
| (_, Exists _) => GREATER
| (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) =>
(case Metis_NameSet.compare (n1,n2) of
LESS => LESS
| EQUAL => compare (f1,f2)
| GREATER => GREATER);
and neg_elt (f,s) = Metis_Set.add s (neg f); in val negate = neg;
val negateSet = neg_set; end;
fun negateMember x s = Metis_Set.member (negate x) s;
local fun member s x = negateMember x s; in fun negateDisjoint s1 s2 = if Metis_Set.size s1 < Metis_Set.size s2 thennot (Metis_Set.exists (member s2) s1) elsenot (Metis_Set.exists (member s1) s2); end;
(*MetisDebug val polarity = fn f => let val res1 = compare (f, negate f) = LESS val res2 = polarity f val _ = res1 = res2 orelse raise Bug "polarity" in res2 end;
*)
fun applyPolarity true fm = fm
| applyPolarity false fm = negate fm;
fun freeIn v fm = Metis_NameSet.member v (freeVars fm);
val freeVarsSet = let fun free (fm,acc) = Metis_NameSet.union (freeVars fm) acc in
Metis_Set.foldl free Metis_NameSet.empty end;
fun count True = countTrue
| count False = countFalse
| count (Metis_Literal _) = countLiteral
| count (And (_,c,_)) = c
| count (Or (_,c,_)) = c
| count (Xor (_,c,p,_)) = if p then c else countNegate c
| count (Exists (_,c,_,_)) = c
| count (Forall (_,c,_,_)) = c;
val countAndSet = let fun countAnd (fm,c) = countAnd2 (count fm, c) in
Metis_Set.foldl countAnd countTrue end;
val countOrSet = let fun countOr (fm,c) = countOr2 (count fm, c) in
Metis_Set.foldl countOr countFalse end;
val countXorSet = let fun countXor (fm,c) = countXor2 (count fm, c) in
Metis_Set.foldl countXor countFalse end;
fun And2 (False,_) = False
| And2 (_,False) = False
| And2 (True,f2) = f2
| And2 (f1,True) = f1
| And2 (f1,f2) = let val (fv1,c1,s1) = case f1 of And fv_c_s => fv_c_s
| _ => (freeVars f1, count f1, singleton f1)
and (fv2,c2,s2) = case f2 of And fv_c_s => fv_c_s
| _ => (freeVars f2, count f2, singleton f2) in ifnot (negateDisjoint s1 s2) thenFalse else let val s = Metis_Set.union s1 s2 in case Metis_Set.size s of
0 => True
| 1 => Metis_Set.pick s
| n => if n = Metis_Set.size s1 + Metis_Set.size s2 then And (Metis_NameSet.union fv1 fv2, countAnd2 (c1,c2), s) else And (freeVarsSet s, countAndSet s, s) end end;
val AndList = List.foldl And2 True;
val AndSet = Metis_Set.foldl And2 True;
fun Or2 (True,_) = True
| Or2 (_,True) = True
| Or2 (False,f2) = f2
| Or2 (f1,False) = f1
| Or2 (f1,f2) = let val (fv1,c1,s1) = case f1 of Or fv_c_s => fv_c_s
| _ => (freeVars f1, count f1, singleton f1)
and (fv2,c2,s2) = case f2 of Or fv_c_s => fv_c_s
| _ => (freeVars f2, count f2, singleton f2) in ifnot (negateDisjoint s1 s2) thenTrue else let val s = Metis_Set.union s1 s2 in case Metis_Set.size s of
0 => False
| 1 => Metis_Set.pick s
| n => if n = Metis_Set.size s1 + Metis_Set.size s2 then Or (Metis_NameSet.union fv1 fv2, countOr2 (c1,c2), s) else Or (freeVarsSet s, countOrSet s, s) end end;
val OrList = List.foldl Or2 False;
val OrSet = Metis_Set.foldl Or2 False;
fun pushOr2 (f1,f2) = let val s1 = case f1 ofAnd (_,_,s) => s | _ => singleton f1 and s2 = case f2 ofAnd (_,_,s) => s | _ => singleton f2
fun g x1 (x2,acc) = And2 (Or2 (x1,x2), acc)
fun f (x1,acc) = Metis_Set.foldl (g x1) acc s2 in
Metis_Set.foldl f True s1 end;
val pushOrList = List.foldl pushOr2 False;
local fun normalize fm = let val p = polarity fm val fm = applyPolarity p fm in
(freeVars fm, count fm, p, singleton fm) end; in fun Xor2 (False,f2) = f2
| Xor2 (f1,False) = f1
| Xor2 (True,f2) = negate f2
| Xor2 (f1,True) = negate f1
| Xor2 (f1,f2) = let val (fv1,c1,p1,s1) = case f1 of Xor x => x | _ => normalize f1 and (fv2,c2,p2,s2) = case f2 of Xor x => x | _ => normalize f2
val s = Metis_Set.symmetricDifference s1 s2
val fm = case Metis_Set.size s of
0 => False
| 1 => Metis_Set.pick s
| n => if n = Metis_Set.size s1 + Metis_Set.size s2 then
Xor (Metis_NameSet.union fv1 fv2, countXor2 (c1,c2), true, s) else
Xor (freeVarsSet s, countXorSet s, true, s)
val p = p1 = p2 in
applyPolarity p fm end; end;
val XorList = List.foldl Xor2 False;
val XorSet = Metis_Set.foldl Xor2 False;
fun XorPolarityList (p,l) = applyPolarity p (XorList l);
fun XorPolaritySet (p,s) = applyPolarity p (XorSet s);
fun destXor (Xor (_,_,p,s)) = let val (fm1,s) = Metis_Set.deletePick s val fm2 = if Metis_Set.size s = 1 then applyPolarity p (Metis_Set.pick s) else Xor (freeVarsSet s, countXorSet s, p, s) in
(fm1,fm2) end
| destXor _ = raise Error "destXor";
fun pushXor fm = let val (f1,f2) = destXor fm val f1' = negate f1 and f2' = negate f2 in
And2 (Or2 (f1,f2), Or2 (f1',f2')) end;
fun Exists1 (v,init_fm) = let fun exists_gen fm = let val fv = Metis_NameSet.delete (freeVars fm) v val c = count fm val n = Metis_NameSet.singleton v in Exists (fv,c,n,fm) end
funexists fm = if freeIn v fm then exists_free fm else fm
and exists_free (Or (_,_,s)) = OrList (Metis_Set.transform exists s)
| exists_free (fm as And (_,_,s)) = let val sv = Metis_Set.filter (freeIn v) s in if Metis_Set.size sv <> 1 then exists_gen fm else let val fm = Metis_Set.pick sv val s = Metis_Set.delete s fm in
And2 (exists_free fm, AndSet s) end end
| exists_free (Exists (fv,c,n,f)) = Exists (Metis_NameSet.delete fv v, c, Metis_NameSet.add n v, f)
| exists_free fm = exists_gen fm in exists init_fm end;
fun ExistsList (vs,f) = List.foldl Exists1 f vs;
fun ExistsSet (n,f) = Metis_NameSet.foldl Exists1 f n;
fun Forall1 (v,init_fm) = let fun forall_gen fm = let val fv = Metis_NameSet.delete (freeVars fm) v val c = count fm val n = Metis_NameSet.singleton v in
Forall (fv,c,n,fm) end
fun forall fm = if freeIn v fm then forall_free fm else fm
and forall_free (And (_,_,s)) = AndList (Metis_Set.transform forall s)
| forall_free (fm as Or (_,_,s)) = let val sv = Metis_Set.filter (freeIn v) s in if Metis_Set.size sv <> 1 then forall_gen fm else let val fm = Metis_Set.pick sv val s = Metis_Set.delete s fm in
Or2 (forall_free fm, OrSet s) end end
| forall_free (Forall (fv,c,n,f)) =
Forall (Metis_NameSet.delete fv v, c, Metis_NameSet.add n v, f)
| forall_free fm = forall_gen fm in
forall init_fm end;
fun ForallList (vs,f) = List.foldl Forall1 f vs;
fun ForallSet (n,f) = Metis_NameSet.foldl Forall1 f n;
fun generalize f = ForallSet (freeVars f, f);
local fun subst_fv fvSub = let fun add_fv (v,s) = Metis_NameSet.union (Metis_NameMap.get fvSub v) s in
Metis_NameSet.foldl add_fv Metis_NameSet.empty end;
fun subst_rename (v,(avoid,bv,sub,domain,fvSub)) = let val v' = Metis_Term.variantPrime avoid v val avoid = Metis_NameSet.add avoid v' val bv = Metis_NameSet.add bv v' valsub = Metis_Subst.insert sub (v, Metis_Term.Var v') val domain = Metis_NameSet.add domain v val fvSub = Metis_NameMap.insert fvSub (v, Metis_NameSet.singleton v') in
(avoid,bv,sub,domain,fvSub) end;
fun subst_check sub domain fvSub fm = let val domain = Metis_NameSet.intersect domain (freeVars fm) in if Metis_NameSet.null domain then fm else subst_domain sub domain fvSub fm end
and subst_domain sub domain fvSub fm = case fm of
Metis_Literal (fv,lit) => let val fv = Metis_NameSet.difference fv domain val fv = Metis_NameSet.union fv (subst_fv fvSub domain) val lit = Metis_Literal.subst sub lit in
Metis_Literal (fv,lit) end
| And (_,_,s) =>
AndList (Metis_Set.transform (subst_check sub domain fvSub) s)
| Or (_,_,s) =>
OrList (Metis_Set.transform (subst_check sub domain fvSub) s)
| Xor (_,_,p,s) =>
XorPolarityList (p, Metis_Set.transform (subst_check sub domain fvSub) s)
| Exists fv_c_n_f => subst_quant Existssub domain fvSub fv_c_n_f
| Forall fv_c_n_f => subst_quant Forall sub domain fvSub fv_c_n_f
| _ => raise Bug "subst_domain"
and subst_quant quant sub domain fvSub (fv,c,bv,fm) = let val sub_fv = subst_fv fvSub domain val fv = Metis_NameSet.union sub_fv (Metis_NameSet.difference fv domain) val captured = Metis_NameSet.intersect bv sub_fv val bv = Metis_NameSet.difference bv captured val avoid = Metis_NameSet.union fv bv val (_,bv,sub,domain,fvSub) =
Metis_NameSet.foldl subst_rename (avoid,bv,sub,domain,fvSub) captured val fm = subst_domain sub domain fvSub fm in
quant (fv,c,bv,fm) end; in fun subst sub = let fun mk_dom (v,tm,(d,fv)) =
(Metis_NameSet.add d v, Metis_NameMap.insert fv (v, Metis_Term.freeVars tm))
val domain_fvSub = (Metis_NameSet.empty, Metis_NameMap.new ()) val (domain,fvSub) = Metis_Subst.foldl mk_dom domain_fvSub sub in
subst_check sub domain fvSub end; end;
local fun lastElt (s : formula Metis_Set.set) = case Metis_Set.findr (K true) s of
NONE => raise Bug "lastElt: empty set"
| SOME fm => fm;
fun negateLastElt s = let val fm = lastElt s in
Metis_Set.add (Metis_Set.delete s fm) (negate fm) end;
fun form fm = case fm of True => Metis_Formula.True
| False => Metis_Formula.False
| Metis_Literal (_,lit) => Metis_Literal.toFormula lit
| And (_,_,s) => Metis_Formula.listMkConj (Metis_Set.transform form s)
| Or (_,_,s) => Metis_Formula.listMkDisj (Metis_Set.transform form s)
| Xor (_,_,p,s) => xorForm p s
| Exists (_,_,n,f) => Metis_Formula.listMkExists (Metis_NameSet.toList n, form f)
| Forall (_,_,n,f) => Metis_Formula.listMkForall (Metis_NameSet.toList n, form f)
(* To convert a Xor set to an Iff list we need to know *) (* whether the size of the set is even or odd: *) (* *) (* b XOR a = b <=> ~a *) (* c XOR b XOR a = c <=> b <=> a *) (* d XOR c XOR b XOR a = d <=> c <=> b <=> ~a *) (* e XOR d XOR c XOR b XOR a = e <=> d <=> c <=> b <=> a *) and xorForm p s = let val p = if Metis_Set.size s mod 2 = 0 thennot p else p val s = if p then s else negateLastElt s in
Metis_Formula.listMkEquiv (Metis_Set.transform form s) end; in val toFormula = form; end;
local fun addLiteral (l,s) = Metis_LiteralSet.add s (toLiteral l); in fun toClause False = Metis_LiteralSet.empty
| toClause (Or (_,_,s)) = Metis_Set.foldl addLiteral Metis_LiteralSet.empty s
| toClause l = Metis_LiteralSet.singleton (toLiteral l); end;
val pp = Metis_Print.ppMap toFormula Metis_Formula.pp;
local val counter : int Metis_StringMap.map Unsynchronized.ref = Unsynchronized.ref (Metis_StringMap.new ());
fun new n () = let val Unsynchronized.ref m = counter val s = Metis_Name.toString n val i = Option.getOpt (Metis_StringMap.peek m s, 0) val () = counter := Metis_StringMap.insert m (s, i + 1) val i = if i = 0 then""else"_" ^ Int.toString i val s = skolemPrefix ^ "_" ^ s ^ i in
Metis_Name.fromString s end; in fun newSkolemFunction n = Metis_Portable.critical (new n) (); end;
fun skolemize fv bv fm = let val fv = Metis_NameSet.transform Metis_Term.Var fv
fun mk (v,s) = Metis_Subst.insert s (v, Metis_Term.Fn (newSkolemFunction v, fv)) in
subst (Metis_NameSet.foldl mk Metis_Subst.empty bv) fm end;
local fun rename avoid fv bv fm = let val captured = Metis_NameSet.intersect avoid bv in if Metis_NameSet.null captured then fm else let fun ren (v,(a,s)) = let val v' = Metis_Term.variantPrime a v in
(Metis_NameSet.add a v', Metis_Subst.insert s (v, Metis_Term.Var v')) end
val avoid = Metis_NameSet.union (Metis_NameSet.union avoid fv) bv
val (_,sub) = Metis_NameSet.foldl ren (avoid,Metis_Subst.empty) captured in
subst sub fm end end;
fun cnfFm avoid fm = (*MetisTrace5 let val fm' = cnfFm' avoid fm val () = Metis_Print.trace pp "Metis_Normalize.cnfFm: fm" fm val () = Metis_Print.trace pp "Metis_Normalize.cnfFm: fm'" fm' in fm' end and cnfFm' avoid fm =
*) case fm of True => True
| False => False
| Metis_Literal _ => fm
| And (_,_,s) => AndList (Metis_Set.transform (cnfFm avoid) s)
| Or (fv,_,s) => let val avoid = Metis_NameSet.union avoid fv val (fms,_) = Metis_Set.foldl cnfOr ([],avoid) s in
pushOrList fms end
| Xor _ => cnfFm avoid (pushXor fm)
| Exists (fv,_,n,f) => cnfFm avoid (skolemize fv n f)
| Forall (fv,_,n,f) => cnfFm avoid (rename avoid fv n f)
and cnfOr (fm,(fms,avoid)) = let val fm = cnfFm avoid fm val fms = fm :: fms val avoid = Metis_NameSet.union avoid (freeVars fm) in
(fms,avoid) end; in val basicCnf = cnfFm Metis_NameSet.empty; end;
(* ------------------------------------------------------------------------- *) (* Finding the formula definition that minimizes the number of clauses. *) (* ------------------------------------------------------------------------- *)
local type best = count * formula option;
fun minBreak countClauses fm best = case fm of True => best
| False => best
| Metis_Literal _ => best
| And (_,_,s) =>
minBreakSet countClauses countAnd2 countTrue AndSet s best
| Or (_,_,s) =>
minBreakSet countClauses countOr2 countFalse OrSet s best
| Xor (_,_,_,s) =>
minBreakSet countClauses countXor2 countFalse XorSet s best
| Exists (_,_,_,f) => minBreak countClauses f best
| Forall (_,_,_,f) => minBreak countClauses f best
and minBreakSet countClauses count2 count0 mkSet fmSet best = let fun cumulatives fms = let fun fwd (fm,(c1,s1,l)) = let val c1' = count2 (count fm, c1) and s1' = Metis_Set.add s1 fm in
(c1', s1', (c1,s1,fm) :: l) end
fun bwd ((c1,s1,fm),(c2,s2,l)) = let val c2' = count2 (count fm, c2) and s2' = Metis_Set.add s2 fm in
(c2', s2', (c1,s1,fm,c2,s2) :: l) end
val (c1,_,fms) = List.foldl fwd (count0,empty,[]) fms val (c2,_,fms) = List.foldl bwd (count0,empty,[]) fms
(*MetisDebug val _ = countEquivish c1 c2 orelse raise Bug ("cumulativeCounts: c1 = " ^ countToString c1 ^ ", c2 = " ^ countToString c2)
*) in
fms end
fun breakSing ((c1,_,fm,c2,_),best) = let val cFms = count2 (c1,c2)
fun countCls cFm = countClauses (count2 (cFms,cFm)) in
minBreak countCls fm best end
val breakSet1 = let fun break c1 s1 fm c2 (best as (bcl,_)) = if Metis_Set.null s1 then best else let val cDef = countDefinition (countXor2 (c1, count fm)) val cFm = count2 (countLiteral,c2) val cl = countAnd2 (cDef, countClauses cFm) val noBetter = countLeqish bcl cl in if noBetter then best else (cl, SOME (mkSet (Metis_Set.add s1 fm))) end in
fn ((c1,s1,fm,c2,s2),best) =>
break c1 s1 fm c2 (break c2 s2 fm c1 best) end
val fms = Metis_Set.toList fmSet
fun breakSet measure best = let val fms = sortMap (measure o count) countCompare fms in List.foldl breakSet1 best (cumulatives fms) end
val best = List.foldl breakSing best (cumulatives fms) val best = breakSet I best val best = breakSet countNegate best val best = breakSet countClauses best in
best end in fun minimumDefinition fm = let val cl = count fm in if countLeqish cl countLiteral then NONE else let val (cl',def) = minBreak I fm (cl,NONE) (*MetisTrace1 val () = case def of NONE => () | SOME d => Metis_Print.trace pp ("defCNF: before = " ^ countToString cl ^ ", after = " ^ countToString cl' ^ ", definition") d
*) in
def end end; end;
(* ------------------------------------------------------------------------- *) (* Conjunctive normal form derivations. *) (* ------------------------------------------------------------------------- *)
datatype thm = Metis_Thm of formula * inference
and inference =
Axiom of Metis_Formula.formula
| Definition ofstring * Metis_Formula.formula
| Simplify of thm * thm list
| Conjunct of thm
| Specialize of thm
| Skolemize of thm
| Clausify of thm;
fun compareThm (Metis_Thm (fm1,_), Metis_Thm (fm2,_)) = compare (fm1,fm2);
fun parentsThm (Metis_Thm (_,inf)) = parentsInference inf;
fun mkAxiom fm = Metis_Thm (fromFormula fm, Axiom fm);
fun destThm (Metis_Thm (fm,inf)) = (toFormula fm, inf);
local val emptyProved : (thm,Metis_Formula.formula) Metis_Map.map = Metis_Map.new compareThm;
fun isProved proved th = Metis_Map.inDomain th proved;
fun isUnproved proved th = not (isProved proved th);
fun lookupProved proved th = case Metis_Map.peek proved th of
SOME fm => fm
| NONE => raise Bug "Metis_Normalize.lookupProved";
fun prove acc proved ths = case ths of
[] => List.rev acc
| th :: ths' => if isProved proved th then prove acc proved ths' else let val pars = parentsThm th
val deps = List.filter (isUnproved proved) pars in ifList.null deps then let val (fm,inf) = destThm th
val fms = List.map (lookupProved proved) pars
val acc = (fm,inf,fms) :: acc
val proved = Metis_Map.insert proved (th,fm) in
prove acc proved ths' end else let val ths = deps @ ths in
prove acc proved ths end end; in val proveThms = prove [] emptyProved; end;
local fun simpler fm s =
Metis_Set.size s <> 1 orelse case Metis_Set.pick s of True => false
| False => false
| Metis_Literal _ => false
| _ => true;
fun addSet set_defs body_def = let fun def_body_size (body,_,_) = Metis_Set.size body
val body_size = def_body_size body_def
val (body,_,_) = body_def
fun add acc [] = List.revAppend (acc,[body_def])
| add acc (l as (bd as (b,_,_)) :: bds) = case Int.compare (def_body_size bd, body_size) of
LESS => List.revAppend (acc, body_def :: l)
| EQUAL => if Metis_Set.equal b body thenList.revAppend (acc,l) else add (bd :: acc) bds
| GREATER => add (bd :: acc) bds in
add [] set_defs end;
fun add simp (body,False,th) = add simp (negate body, True, th)
| add simp (True,_,_) = simp
| add (Simp {formula,andSet,orSet,xorSet}) (And (_,_,s), def, th) = let val andSet = addSet andSet (s,def,th) and orSet = addSet orSet (negateSet s, negate def, th) in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet} end
| add (Simp {formula,andSet,orSet,xorSet}) (Or (_,_,s), def, th) = let val orSet = addSet orSet (s,def,th) and andSet = addSet andSet (negateSet s, negate def, th) in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet} end
| add simp (Xor (_,_,p,s), def, th) = let val simp = addXorSet simp (s, applyPolarity p def, th) in case def of True => let fun addXorLiteral (fm as Metis_Literal _, simp) = let val s = Metis_Set.delete s fm in ifnot (simpler fm s) then simp else addXorSet simp (s, applyPolarity (not p) fm, th) end
| addXorLiteral (_,simp) = simp in
Metis_Set.foldl addXorLiteral simp s end
| _ => simp end
| add (simp as Simp {formula,andSet,orSet,xorSet}) (body,def,th) = if Metis_Map.inDomain body formula then simp else let val formula = Metis_Map.insert formula (body,(def,th)) val formula = Metis_Map.insert formula (negate body, (negate def, th)) in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet} end
and addXorSet (simp as Simp {formula,andSet,orSet,xorSet}) (s,def,th) = if Metis_Set.size s = 1 then add simp (Metis_Set.pick s, def, th) else let val xorSet = addSet xorSet (s,def,th) in
Simp
{formula = formula,
andSet = andSet,
orSet = orSet,
xorSet = xorSet} end; in fun simplifyAdd simp (th as Metis_Thm (fm,_)) = add simp (fm,True,th); end;
local fun simplifySet set_defs set = let fun pred (s,_,_) = Metis_Set.subset s set in caseList.find pred set_defs of
NONE => NONE
| SOME (s,f,th) => let valset = Metis_Set.add (Metis_Set.difference set s) f in
SOME (set,th) end end; in fun simplify (Simp {formula,andSet,orSet,xorSet}) = let fun simp fm inf = case simp_sub fm inf of
NONE => simp_top fm inf
| SOME (fm,inf) => try_simp_top fm inf
and try_simp_top fm inf = case simp_top fm inf of
NONE => SOME (fm,inf)
| x => x
and simp_top fm inf = case fm of And (_,_,s) =>
(case simplifySet andSet s of
NONE => NONE
| SOME (s,th) => let val fm = AndSet s val inf = th :: inf in
try_simp_top fm inf end)
| Or (_,_,s) =>
(case simplifySet orSet s of
NONE => NONE
| SOME (s,th) => let val fm = OrSet s val inf = th :: inf in
try_simp_top fm inf end)
| Xor (_,_,p,s) =>
(case simplifySet xorSet s of
NONE => NONE
| SOME (s,th) => let val fm = XorPolaritySet (p,s) val inf = th :: inf in
try_simp_top fm inf end)
| _ =>
(case Metis_Map.peek formula fm of
NONE => NONE
| SOME (fm,th) => let val inf = th :: inf in
try_simp_top fm inf end)
and simp_sub fm inf = case fm of And (_,_,s) =>
(case simp_set s inf of
NONE => NONE
| SOME (l,inf) => SOME (AndList l, inf))
| Or (_,_,s) =>
(case simp_set s inf of
NONE => NONE
| SOME (l,inf) => SOME (OrList l, inf))
| Xor (_,_,p,s) =>
(case simp_set s inf of
NONE => NONE
| SOME (l,inf) => SOME (XorPolarityList (p,l), inf))
| Exists (_,_,n,f) =>
(case simp f inf of
NONE => NONE
| SOME (f,inf) => SOME (ExistsSet (n,f), inf))
| Forall (_,_,n,f) =>
(case simp f inf of
NONE => NONE
| SOME (f,inf) => SOME (ForallSet (n,f), inf))
| _ => NONE
and simp_set s inf = let val (changed,l,inf) = Metis_Set.foldr simp_set_elt (false,[],inf) s in if changed then SOME (l,inf) else NONE end
and simp_set_elt (fm,(changed,l,inf)) = case simp fm inf of
NONE => (changed, fm :: l, inf)
| SOME (fm,inf) => (true, fm :: l, inf) in
fn th as Metis_Thm (fm,_) => case simp fm [] of
SOME (fm,ths) => let val inf = Simplify (th,ths) in
Metis_Thm (fm,inf) end
| NONE => th end; end;
(*MetisTrace2 val simplify = fn simp => fn th as Metis_Thm (fm,_) => let val th' as Metis_Thm (fm',_) = simplify simp th val () = if compare (fm,fm') = EQUAL then () else (Metis_Print.trace pp "Metis_Normalize.simplify: fm" fm; Metis_Print.trace pp "Metis_Normalize.simplify: fm'" fm') in th' end;
*)
local val counter : int Unsynchronized.ref = Unsynchronized.ref 0;
fun new () = let val Unsynchronized.ref i = counter val () = counter := i + 1 in
definitionPrefix ^ "_" ^ Int.toString i end; in fun newDefinitionRelation () = Metis_Portable.critical new (); end;
fun newDefinition def = let val fv = freeVars def val rel = newDefinitionRelation () val atm = (Metis_Name.fromString rel, Metis_NameSet.transform Metis_Term.Var fv) val fm = Metis_Formula.Iff (Metis_Formula.Metis_Atom atm, toFormula def) val fm = Metis_Formula.setMkForall (fv,fm) val inf = Definition (rel,fm) val lit = Metis_Literal (fv,(false,atm)) val fm = Xor2 (lit,def) in
Metis_Thm (fm,inf) end;
datatype cnf =
ConsistentCnf of simplify
| InconsistentCnf;
val initialCnf = ConsistentCnf simplifyEmpty;
local fun def_cnf_inconsistent th = let val cls = [(Metis_LiteralSet.empty,th)] in
(cls,InconsistentCnf) end;
fun def_cnf_clause inf (fm,acc) = let val cl = toClause fm val th = Metis_Thm (fm,inf) in
(cl,th) :: acc end (*MetisDebug handle Error err => (Metis_Print.trace pp "Metis_Normalize.addCnf.def_cnf_clause: fm" fm; raise Bug ("Metis_Normalize.addCnf.def_cnf_clause: " ^ err));
*)
fun def_cnf cls simp ths = case ths of
[] => (cls, ConsistentCnf simp)
| th :: ths => def_cnf_formula cls simp (simplify simp th) ths
and def_cnf_formula cls simp (th as Metis_Thm (fm,_)) ths = case fm of True => def_cnf cls simp ths
| False => def_cnf_inconsistent th
| And (_,_,s) => let fun add (f,z) = Metis_Thm (f, Conjunct th) :: z in
def_cnf cls simp (Metis_Set.foldr add ths s) end
| Exists (fv,_,n,f) => let val th = Metis_Thm (skolemize fv n f, Skolemize th) in
def_cnf_formula cls simp th ths end
| Forall (_,_,_,f) => let val th = Metis_Thm (f, Specialize th) in
def_cnf_formula cls simp th ths end
| _ => case minimumDefinition fm of
SOME def => let val ths = th :: ths val th = newDefinition def in
def_cnf_formula cls simp th ths end
| NONE => let val simp = simplifyAdd simp th
val fm = basicCnf fm
val inf = Clausify th in case fm of True => def_cnf cls simp ths
| False => def_cnf_inconsistent (Metis_Thm (fm,inf))
| And (_,_,s) => let val inf = Conjunct (Metis_Thm (fm,inf)) val cls = Metis_Set.foldl (def_cnf_clause inf) cls s in
def_cnf cls simp ths end
| fm => def_cnf (def_cnf_clause inf (fm,cls)) simp ths end; in fun addCnf th cnf = case cnf of
ConsistentCnf simp => def_cnf [] simp [th]
| InconsistentCnf => ([],cnf); end;
local fun add (th,(cls,cnf)) = let val (cls',cnf) = addCnf th cnf in
(cls' @ cls, cnf) end; in fun proveCnf ths = let val (cls,_) = List.foldl add ([],initialCnf) ths in List.rev cls end; end;
fun cnf fm = let val cls = proveCnf [mkAxiom fm] in List.map fst cls end;
end
(**** Original file: src/Model.sig ****)
(* ========================================================================= *) (* RANDOM FINITE MODELS *) (* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *)
(* ------------------------------------------------------------------------- *) (* A model of size N has integer elements 0...N-1. *) (* ------------------------------------------------------------------------- *)
type element = int
val zeroElement : element
val incrementElement : size -> element -> element option
(* ------------------------------------------------------------------------- *) (* The parts of the model that are fixed. *) (* ------------------------------------------------------------------------- *)
type fixedFunction = size -> element list -> element option
type fixedRelation = size -> element list -> booloption
val foldValuation :
{size : int} -> Metis_NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a
(* ------------------------------------------------------------------------- *) (* A type of random finite models. *) (* ------------------------------------------------------------------------- *)
type parameters = {size : int, fixed : fixed}
type model
val default : parameters
val new : parameters -> model
valsize : model -> int
(* ------------------------------------------------------------------------- *) (* Interpreting terms and formulas in the model. *) (* ------------------------------------------------------------------------- *)
val interpretFunction : model -> Metis_Term.functionName * element list -> element
val interpretRelation : model -> Metis_Atom.relationName * element list -> bool
val interpretTerm : model -> valuation -> Metis_Term.term -> element
val interpretAtom : model -> valuation -> Metis_Atom.atom -> bool
val interpretFormula : model -> valuation -> Metis_Formula.formula -> bool
val interpretLiteral : model -> valuation -> Metis_Literal.literal -> bool
val interpretClause : model -> valuation -> Metis_Thm.clause -> bool
(* ------------------------------------------------------------------------- *) (* Check whether random groundings of a formula are true in the model. *) (* Note: if it's cheaper, a systematic check will be performed instead. *) (* ------------------------------------------------------------------------- *)
val check :
(model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model ->
Metis_NameSet.set -> 'a -> {T : int, F : int}
val checkAtom :
{maxChecks : int option} -> model -> Metis_Atom.atom -> {T : int, F : int}
val checkFormula :
{maxChecks : int option} -> model -> Metis_Formula.formula -> {T : int, F : int}
val checkLiteral :
{maxChecks : int option} -> model -> Metis_Literal.literal -> {T : int, F : int}
val checkClause :
{maxChecks : int option} -> model -> Metis_Thm.clause -> {T : int, F : int}
val updateFunction :
model -> (Metis_Term.functionName * element list) * element -> unit
val updateRelation :
model -> (Metis_Atom.relationName * element list) * bool -> unit
(* ------------------------------------------------------------------------- *) (* Choosing a random perturbation to make a formula true in the model. *) (* ------------------------------------------------------------------------- *)
val perturbTerm : model -> valuation -> Metis_Term.term * element list -> unit
val perturbAtom : model -> valuation -> Metis_Atom.atom * bool -> unit
val perturbLiteral : model -> valuation -> Metis_Literal.literal -> unit
val perturbClause : model -> valuation -> Metis_Thm.clause -> unit
val multInt = case Int.maxInt of
NONE => (fn x => fn y => SOME (x * y))
| SOME m => let val m = Real.floor (Math.sqrt (Real.fromInt m)) in
fn x => fn y => if x <= m andalso y <= m then SOME (x * y) else NONE end;
local fun iexp x y acc = if y mod 2 = 0 then iexp' x y acc else case multInt acc x of
SOME acc => iexp' x y acc
| NONE => NONE
and iexp' x y acc = if y = 1 then SOME acc else let val y = y div 2 in case multInt x x of
SOME x => iexp x y acc
| NONE => NONE end; in fun expInt x y = if y <= 1 then if y = 0 then SOME 1 elseif y = 1 then SOME x elseraise Bug "expInt: negative exponent" elseif x <= 1 then if 0 <= x then SOME x elseraise Bug "expInt: negative exponand" else iexp x y 1; end;
(* ------------------------------------------------------------------------- *) (* A model of size N has integer elements 0...N-1. *) (* ------------------------------------------------------------------------- *)
type element = int;
val zeroElement = 0;
fun incrementElement {size = N} i = let val i = i + 1 in if i = N then NONE else SOME i end;
fun elementListSpace {size = N} arity = case expInt N arity of
NONE => NONE
| s as SOME m => if m <= maxSpace then s else NONE;
fun elementListIndex {size = N} = let fun f acc elts = case elts of
[] => acc
| elt :: elts => f (N * acc + elt) elts in
f 0 end;
(* ------------------------------------------------------------------------- *) (* The parts of the model that are fixed. *) (* ------------------------------------------------------------------------- *)
type fixedFunction = size -> element list -> element option;
type fixedRelation = size -> element list -> booloption;
val uselessFixedFunction : fixedFunction = K (K NONE);
val uselessFixedRelation : fixedRelation = K (K NONE);
val emptyFunctions : fixedFunction Metis_NameArityMap.map = Metis_NameArityMap.new ();
val emptyRelations : fixedRelation Metis_NameArityMap.map = Metis_NameArityMap.new ();
fun fixed0 f sz elts = case elts of
[] => f sz
| _ => raise Bug "Metis_Model.fixed0: wrong arity";
fun fixed1 f sz elts = case elts of
[x] => f sz x
| _ => raise Bug "Metis_Model.fixed1: wrong arity";
fun fixed2 f sz elts = case elts of
[x,y] => f sz x y
| _ => raise Bug "Metis_Model.fixed2: wrong arity";
val emptyFixed = let val fns = emptyFunctions and rels = emptyRelations in
Fixed
{functions = fns,
relations = rels} end;
fun peekFunctionFixed fix name_arity = let val Fixed {functions = fns, ...} = fix in
Metis_NameArityMap.peek fns name_arity end;
fun peekRelationFixed fix name_arity = let val Fixed {relations = rels, ...} = fix in
Metis_NameArityMap.peek rels name_arity end;
fun getFunctionFixed fix name_arity = case peekFunctionFixed fix name_arity of
SOME f => f
| NONE => uselessFixedFunction;
fun getRelationFixed fix name_arity = case peekRelationFixed fix name_arity of
SOME rel => rel
| NONE => uselessFixedRelation;
fun insertFunctionFixed fix name_arity_fn = let val Fixed {functions = fns, relations = rels} = fix
val fns = Metis_NameArityMap.insert fns name_arity_fn in
Fixed
{functions = fns,
relations = rels} end;
fun insertRelationFixed fix name_arity_rel = let val Fixed {functions = fns, relations = rels} = fix
val rels = Metis_NameArityMap.insert rels name_arity_rel in
Fixed
{functions = fns,
relations = rels} end;
local fun union _ = raise Bug "Metis_Model.unionFixed: nameArity clash"; in fun unionFixed fix1 fix2 = let val Fixed {functions = fns1, relations = rels1} = fix1 and Fixed {functions = fns2, relations = rels2} = fix2
val fns = Metis_NameArityMap.union union fns1 fns2
val rels = Metis_NameArityMap.union union rels1 rels2 in
Fixed
{functions = fns,
relations = rels} end; end;
val unionListFixed = let fun union (fix,acc) = unionFixed acc fix in List.foldl union emptyFixed end;
local fun hasTypeFn _ elts = case elts of
[x,_] => SOME x
| _ => raise Bug "Metis_Model.hasTypeFn: wrong arity";
fun eqRel _ elts = case elts of
[x,y] => SOME (x = y)
| _ => raise Bug "Metis_Model.eqRel: wrong arity"; in val basicFixed = let val fns = Metis_NameArityMap.singleton (Metis_Term.hasTypeFunction,hasTypeFn)
val rels = Metis_NameArityMap.singleton (Metis_Atom.eqRelation,eqRel) in
Fixed
{functions = fns,
relations = rels} end; end;
fun mapFixed fixMap fix = let val {functionMap = fnMap, relationMap = relMap} = fixMap and Fixed {functions = fns, relations = rels} = fix
val fns = Metis_NameArityMap.compose fnMap fns
val rels = Metis_NameArityMap.compose relMap rels in
Fixed
{functions = fns,
relations = rels} end;
local fun mkEntry tag (na,n) = (tag,na,n);
fun mkList tag m = List.map (mkEntry tag) (Metis_NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
Metis_Print.inconsistentBlock 2
[Metis_Print.ppString tag,
Metis_Print.break,
Metis_NameArity.pp source_arity,
Metis_Print.ppString " ->",
Metis_Print.break,
Metis_Name.pp target]; in fun ppFixedMap fixMap = let val {functionMap = fnMap, relationMap = relMap} = fixMap in case mkList "function" fnMap @ mkList "relation" relMap of
[] => Metis_Print.skip
| entry :: entries =>
Metis_Print.consistentBlock 0
(ppEntry entry :: List.map (Metis_Print.sequence Metis_Print.newline o ppEntry) entries) end; end;
(* ------------------------------------------------------------------------- *) (* Standard fixed model parts. *) (* ------------------------------------------------------------------------- *)
(* Projections *)
val projectionMin = 1 and projectionMax = 9;
val projectionList = minMaxInterval projectionMin projectionMax;
fun projectionName i = let val _ = projectionMin <= i orelse raise Bug "Metis_Model.projectionName: less than projectionMin"
val _ = i <= projectionMax orelse raise Bug "Metis_Model.projectionName: greater than projectionMax" in
Metis_Name.fromString ("project" ^ Int.toString i) end;
fun projectionFn i _ elts = SOME (List.nth (elts, i - 1));
fun arityProjectionFixed arity = let fun mkProj i = ((projectionName i, arity), projectionFn i)
fun addProj i acc = if i > arity then acc else addProj (i + 1) (Metis_NameArityMap.insert acc (mkProj i))
val fns = addProj projectionMin emptyFunctions
val rels = emptyRelations in
Fixed
{functions = fns,
relations = rels} end;
val projectionFixed =
unionListFixed (List.map arityProjectionFixed projectionList);
(* Arithmetic *)
val numeralMin = ~100 and numeralMax = 100;
val numeralList = minMaxInterval numeralMin numeralMax;
fun numeralName i = let val _ = numeralMin <= i orelse raise Bug "Metis_Model.numeralName: less than numeralMin"
val _ = i <= numeralMax orelse raise Bug "Metis_Model.numeralName: greater than numeralMax"
val s = if i < 0 then"negative" ^ Int.toString (~i) else Int.toString i in
Metis_Name.fromString s end;
val addName = Metis_Name.fromString "+" and divName = Metis_Name.fromString "div" and dividesName = Metis_Name.fromString "divides" and evenName = Metis_Name.fromString "even" and expName = Metis_Name.fromString "exp" and geName = Metis_Name.fromString ">=" and gtName = Metis_Name.fromString ">" and isZeroName = Metis_Name.fromString "isZero" and leName = Metis_Name.fromString "<=" and ltName = Metis_Name.fromString "<" and modName = Metis_Name.fromString "mod" and multName = Metis_Name.fromString "*" and negName = Metis_Name.fromString "~" and oddName = Metis_Name.fromString "odd" and preName = Metis_Name.fromString "pre" and subName = Metis_Name.fromString "-" and sucName = Metis_Name.fromString "suc";
local (* Support *)
fun modN {size = N} x = x mod N;
fun oneN sz = modN sz 1;
fun multN sz (x,y) = modN sz (x * y);
(* Functions *)
fun numeralFn i sz = SOME (modN sz i);
fun addFn sz x y = SOME (modN sz (x + y));
fun divFn {size = N} x y = let val y = if y = 0 then N else y in
SOME (x div y) end;
fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
fun modFn {size = N} x y = let val y = if y = 0 then N else y in
SOME (x mod y) end;
fun multFn sz x y = SOME (multN sz (x,y));
fun negFn {size = N} x = SOME (if x = 0 then 0 else N - x);
fun preFn {size = N} x = SOME (if x = 0 then N - 1 else x - 1);
fun subFn {size = N} x y = SOME (if x < y then N + x - y else x - y);
fun sucFn {size = N} x = SOME (if x = N - 1 then 0 else x + 1);
(* Relations *)
fun dividesRel _ x y = SOME (divides x y);
fun evenRel _ x = SOME (x mod 2 = 0);
fun geRel _ x y = SOME (x >= y);
fun gtRel _ x y = SOME (x > y);
fun isZeroRel _ x = SOME (x = 0);
fun leRel _ x y = SOME (x <= y);
fun ltRel _ x y = SOME (x < y);
fun oddRel _ x = SOME (x mod 2 = 1); in val modularFixed = let val fns =
Metis_NameArityMap.fromList
(List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
((expName,2), fixed2 expFn),
((modName,2), fixed2 modFn),
((multName,2), fixed2 multFn),
((negName,1), fixed1 negFn),
((preName,1), fixed1 preFn),
((subName,2), fixed2 subFn),
((sucName,1), fixed1 sucFn)])
val cardName = Metis_Name.fromString "card" and complementName = Metis_Name.fromString "complement" and differenceName = Metis_Name.fromString "difference" and emptyName = Metis_Name.fromString "empty" and memberName = Metis_Name.fromString "member" and insertName = Metis_Name.fromString "insert" and intersectName = Metis_Name.fromString "intersect" and singletonName = Metis_Name.fromString "singleton" and subsetName = Metis_Name.fromString "subset" and symmetricDifferenceName = Metis_Name.fromString "symmetricDifference" and unionName = Metis_Name.fromString "union" and universeName = Metis_Name.fromString "universe";
local (* Support *)
fun eltN {size = N} = let fun f 0 acc = acc
| f x acc = f (x div 2) (acc + 1) in
f N ~1 end;
fun posN i = Word.<< (0w1, Word.fromInt i);
fun univN sz = Word.- (posN (eltN sz), 0w1);
fun setN sz x = Word.andb (Word.fromInt x, univN sz);
(* Functions *)
fun cardFn sz x = let fun f 0w0 acc = acc
| f s acc = let val acc = if Word.andb (s,0w1) = 0w0 then acc else acc + 1 in
f (Word.>> (s,0w1)) acc end in
SOME (f (setN sz x) 0) end;
fun complementFn sz x = SOME (Word.toInt (Word.xorb (univN sz, setN sz x)));
fun differenceFn sz x y = let val x = setN sz x and y = setN sz y in
SOME (Word.toInt (Word.andb (x, Word.notb y))) end;
fun emptyFn _ = SOME 0;
fun insertFn sz x y = let val x = x mod eltN sz and y = setN sz y in
SOME (Word.toInt (Word.orb (posN x, y))) end;
fun intersectFn sz x y =
SOME (Word.toInt (Word.andb (setN sz x, setN sz y)));
fun singletonFn sz x = let val x = x mod eltN sz in
SOME (Word.toInt (posN x)) end;
fun symmetricDifferenceFn sz x y = let val x = setN sz x and y = setN sz y in
SOME (Word.toInt (Word.xorb (x,y))) end;
fun unionFn sz x y =
SOME (Word.toInt (Word.orb (setN sz x, setN sz y)));
fun universeFn sz = SOME (Word.toInt (univN sz));
(* Relations *)
fun memberRel sz x y = let val x = x mod eltN sz and y = setN sz y in
SOME (Word.andb (posN x, y) <> 0w0) end;
fun subsetRel sz x y = let val x = setN sz x and y = setN sz y in
SOME (Word.andb (x, Word.notb y) = 0w0) end; in val setFixed = let val fns =
Metis_NameArityMap.fromList
[((cardName,1), fixed1 cardFn),
((complementName,1), fixed1 complementFn),
((differenceName,2), fixed2 differenceFn),
((emptyName,0), fixed0 emptyFn),
((insertName,2), fixed2 insertFn),
((intersectName,2), fixed2 intersectFn),
((singletonName,1), fixed1 singletonFn),
((symmetricDifferenceName,2), fixed2 symmetricDifferenceFn),
((unionName,2), fixed2 unionFn),
((universeName,0), fixed0 universeFn)]
val rels =
Metis_NameArityMap.fromList
[((memberName,2), fixed2 memberRel),
((subsetName,2), fixed2 subsetRel)] in
Fixed
{functions = fns,
relations = rels} end; end;
(* Lists *)
val appendName = Metis_Name.fromString "@" and consName = Metis_Name.fromString "::" and lengthName = Metis_Name.fromString "length" and nilName = Metis_Name.fromString "nil" and nullName = Metis_Name.fromString "null" and tailName = Metis_Name.fromString "tail";
local val baseFix = let val fix = unionFixed projectionFixed overflowFixed
val sucFn = getFunctionFixed fix (sucName,1)
fun suc2Fn sz _ x = sucFn sz [x] in
insertFunctionFixed fix ((sucName,2), fixed2 suc2Fn) end;
datatype valuation = Valuation of element Metis_NameMap.map;
val emptyValuation = Valuation (Metis_NameMap.new ());
fun insertValuation (Valuation m) v_i = Valuation (Metis_NameMap.insert m v_i);
fun peekValuation (Valuation m) v = Metis_NameMap.peek m v;
fun constantValuation i = let fun add (v,V) = insertValuation V (v,i) in
Metis_NameSet.foldl add emptyValuation end;
val zeroValuation = constantValuation zeroElement;
fun getValuation V v = case peekValuation V v of
SOME i => i
| NONE => raise Error "Metis_Model.getValuation: incomplete valuation";
fun randomValuation {size = N} vs = let fun f (v,V) = insertValuation V (v, Metis_Portable.randomInt N) in
Metis_NameSet.foldl f emptyValuation vs end;
fun incrementValuation N vars = let fun inc vs V = case vs of
[] => NONE
| v :: vs => let val (carry,i) = case incrementElement N (getValuation V v) of
SOME i => (false,i)
| NONE => (true,zeroElement)
val V = insertValuation V (v,i) in if carry then inc vs V else SOME V end in
inc (Metis_NameSet.toList vars) end;
fun foldValuation N vars f = let val inc = incrementValuation N vars
fun fold V acc = let val acc = f (V,acc) in case inc V of
NONE => acc
| SOME V => fold V acc end
val zero = zeroValuation vars in
fold zero end;
(* ------------------------------------------------------------------------- *) (* A type of random finite mapping Z^n -> Z. *) (* ------------------------------------------------------------------------- *)
val UNKNOWN = ~1;
datatype table =
ForgetfulTable
| ArrayTable of int Array.array;
fun newTable N arity = case elementListSpace {size = N} arity of
NONE => ForgetfulTable
| SOME space => ArrayTable (Array.array (space,UNKNOWN));
local fun randomResult R = Metis_Portable.randomInt R; in fun lookupTable N R table elts = case table of
ForgetfulTable => randomResult R
| ArrayTable a => let val i = elementListIndex {size = N} elts
val r = Array.sub (a,i) in if r <> UNKNOWN then r else let val r = randomResult R
val () = Array.update (a,i,r) in
r end end; end;
fun updateTable N table (elts,r) = case table of
ForgetfulTable => ()
| ArrayTable a => let val i = elementListIndex {size = N} elts
val () = Array.update (a,i,r) in
() end;
(* ------------------------------------------------------------------------- *) (* A type of random finite mappings name * arity -> Z^arity -> Z. *) (* ------------------------------------------------------------------------- *)
fun newTables N R =
Tables
{domainSize = N,
rangeSize = R,
tableMap = Unsynchronized.ref (Metis_NameArityMap.new ())};
fun getTables tables n_a = let val Tables {domainSize = N, rangeSize = _, tableMap = tm} = tables
val Unsynchronized.ref m = tm in case Metis_NameArityMap.peek m n_a of
SOME t => t
| NONE => let val (_,a) = n_a
val t = newTable N a
val m = Metis_NameArityMap.insert m (n_a,t)
val () = tm := m in
t end end;
fun lookupTables tables (n,elts) = let val Tables {domainSize = N, rangeSize = R, ...} = tables
val a = length elts
val table = getTables tables (n,a) in
lookupTable N R table elts end;
fun updateTables tables ((n,elts),r) = let val Tables {domainSize = N, ...} = tables
val a = length elts
val table = getTables tables (n,a) in
updateTable N table (elts,r) end;
(* ------------------------------------------------------------------------- *) (* A type of random finite models. *) (* ------------------------------------------------------------------------- *)
type parameters = {size : int, fixed : fixed};
datatype model =
Metis_Model of
{size : int,
fixedFunctions : (element list -> element option) Metis_NameArityMap.map,
fixedRelations : (element list -> booloption) Metis_NameArityMap.map,
randomFunctions : tables,
randomRelations : tables};
fun new {size = N, fixed} = let val Fixed {functions = fns, relations = rels} = fixed
val fixFns = Metis_NameArityMap.transform (fn f => f {size = N}) fns and fixRels = Metis_NameArityMap.transform (fn r => r {size = N}) rels
val rndFns = newTables N N and rndRels = newTables N 2 in
Metis_Model
{size = N,
fixedFunctions = fixFns,
fixedRelations = fixRels,
randomFunctions = rndFns,
randomRelations = rndRels} end;
funsize (Metis_Model {size = N, ...}) = N;
fun peekFixedFunction M (n,elts) = let val Metis_Model {fixedFunctions = fixFns, ...} = M in case Metis_NameArityMap.peek fixFns (n, length elts) of
NONE => NONE
| SOME fixFn => fixFn elts end;
fun isFixedFunction M n_elts = Option.isSome (peekFixedFunction M n_elts);
fun peekFixedRelation M (n,elts) = let val Metis_Model {fixedRelations = fixRels, ...} = M in case Metis_NameArityMap.peek fixRels (n, length elts) of
NONE => NONE
| SOME fixRel => fixRel elts end;
fun isFixedRelation M n_elts = Option.isSome (peekFixedRelation M n_elts);
(* A default model *)
val defaultSize = 8;
val defaultFixed =
unionListFixed
[basicFixed,
projectionFixed,
modularFixed,
setFixed,
listFixed];
val default = {size = defaultSize, fixed = defaultFixed};
fun destTerm tm = case tm of
Metis_Term.Var _ => tm
| Metis_Term.Fn f_tms => case Metis_Term.stripApp tm of
(_,[]) => tm
| (v as Metis_Term.Var _, tms) => Metis_Term.Fn (Metis_Term.appName, v :: tms)
| (Metis_Term.Fn (f,tms), tms') => Metis_Term.Fn (f, tms @ tms');
(* ------------------------------------------------------------------------- *) (* Interpreting terms and formulas in the model. *) (* ------------------------------------------------------------------------- *)
fun interpretFunction M n_elts = case peekFixedFunction M n_elts of
SOME r => r
| NONE => let val Metis_Model {randomFunctions = rndFns, ...} = M in
lookupTables rndFns n_elts end;
fun interpretRelation M n_elts = case peekFixedRelation M n_elts of
SOME r => r
| NONE => let val Metis_Model {randomRelations = rndRels, ...} = M in
intToBool (lookupTables rndRels n_elts) end;
fun interpretTerm M V = let fun interpret tm = case destTerm tm of
Metis_Term.Var v => getValuation V v
| Metis_Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms) in
interpret end;
fun interpretAtom M V (r,tms) =
interpretRelation M (r, List.map (interpretTerm M V) tms);
fun interpretFormula M = let val N = size M
fun interpret V fm = case fm of
Metis_Formula.True => true
| Metis_Formula.False => false
| Metis_Formula.Metis_Atom atm => interpretAtom M V atm
| Metis_Formula.Not p => not (interpret V p)
| Metis_Formula.Or (p,q) => interpret V p orelse interpret V q
| Metis_Formula.And (p,q) => interpret V p andalso interpret V q
| Metis_Formula.Imp (p,q) => interpret V (Metis_Formula.Or (Metis_Formula.Not p, q))
| Metis_Formula.Iff (p,q) => interpret V p = interpret V q
| Metis_Formula.Forall (v,p) => interpret' V p v N
| Metis_Formula.Exists (v,p) =>
--> --------------------
--> maximum size reached
--> --------------------
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 1.255 Sekunden
(vorverarbeitet am 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
