--- a/src/Tools/Metis/metis.ML Thu Sep 16 08:02:32 2010 +0200
+++ b/src/Tools/Metis/metis.ML Thu Sep 16 08:27:10 2010 +0200
@@ -17,7 +17,7 @@
print_depth 0;
-(**** Original file: Random.sig ****)
+(**** Original file: src/Random.sig ****)
(* Title: Tools/random_word.ML
Author: Makarius
@@ -29,6 +29,7 @@
signature Metis_Random =
sig
+
val nextWord : unit -> word
val nextBool : unit -> bool
@@ -39,7 +40,7 @@
end;
-(**** Original file: Random.sml ****)
+(**** Original file: src/Random.sml ****)
(* Title: Tools/random_word.ML
Author: Makarius
@@ -90,11 +91,11 @@
end;
-(**** Original file: Portable.sig ****)
-
-(* ========================================================================= *)
-(* ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(**** Original file: src/Portable.sig ****)
+
+(* ========================================================================= *)
+(* ML COMPILER SPECIFIC FUNCTIONS *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Portable =
@@ -113,17 +114,10 @@
val pointerEqual : 'a * 'a -> bool
(* ------------------------------------------------------------------------- *)
-(* Timing function applications. *)
-(* ------------------------------------------------------------------------- *)
-
-val time : ('a -> 'b) -> 'a -> 'b
-
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-(* MODIFIED by Jasmin Blanchette *)
-val CRITICAL: (unit -> 'a) -> 'a
+(* Marking critical sections of code. *)
+(* ------------------------------------------------------------------------- *)
+
+val critical : (unit -> 'a) -> unit -> 'a
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
@@ -137,97 +131,44 @@
val randomWord : unit -> Word.word
-end
-
-(**** Original file: PortablePolyml.sml ****)
-
-(* ========================================================================= *)
-(* POLY/ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications. *)
+(* ------------------------------------------------------------------------- *)
+
+val time : ('a -> 'b) -> 'a -> 'b
+
+end
+
+(**** Original file: PortableIsabelle.sml ****)
+
+(* Title: Tools/Metis/PortableIsabelle.sml
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010
+
+Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml".
+*)
structure Metis_Portable :> Metis_Portable =
struct
-(* ------------------------------------------------------------------------- *)
-(* The ML implementation. *)
-(* ------------------------------------------------------------------------- *)
-
-val ml = "polyml";
-
-(* ------------------------------------------------------------------------- *)
-(* Pointer equality using the run-time system. *)
-(* ------------------------------------------------------------------------- *)
-
-fun pointerEqual (x : 'a, y : 'a) = pointer_eq(x,y);
-
-(* ------------------------------------------------------------------------- *)
-(* Timing function applications. *)
-(* ------------------------------------------------------------------------- *)
-
-fun time f x =
- let
- fun p t =
- let
- val s = Time.fmt 3 t
- in
- case size (List.last (String.fields (fn x => x = #".") s)) of
- 3 => s
- | 2 => s ^ "0"
- | 1 => s ^ "00"
- | _ => raise Fail "Metis_Portable.time"
- end
-
- val c = Timer.startCPUTimer ()
-
- val r = Timer.startRealTimer ()
-
- fun pt () =
- let
- val {usr,sys} = Timer.checkCPUTimer c
- val real = Timer.checkRealTimer r
- in
- TextIO.print (* MODIFIED by Jasmin Blanchette *)
- ("User: " ^ p usr ^ " System: " ^ p sys ^
- " Real: " ^ p real ^ "\n")
- end
-
- val y = f x handle e => (pt (); raise e)
-
- val () = pt ()
- in
- y
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
-
-
-(* ------------------------------------------------------------------------- *)
-(* Generating random values. *)
-(* ------------------------------------------------------------------------- *)
-
-val randomWord = Metis_Random.nextWord;
-
-val randomBool = Metis_Random.nextBool;
-
-val randomInt = Metis_Random.nextInt;
-
-val randomReal = Metis_Random.nextReal;
-
-end
-
-(* ------------------------------------------------------------------------- *)
-(* Quotations a la Moscow ML. *)
-(* ------------------------------------------------------------------------- *)
-
-datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a;
-
-(**** Original file: Useful.sig ****)
+val ml = "isabelle"
+
+fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
+
+fun critical e () = NAMED_CRITICAL "metis" e
+
+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 *)
@@ -253,8 +194,6 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val print : string -> unit (* MODIFIED by Jasmin Blanchette *)
-
val tracePrint : (string -> unit) Unsynchronized.ref
val trace : string -> unit
@@ -340,10 +279,6 @@
(* Lists: note we count elements from 0. *)
(* ------------------------------------------------------------------------- *)
-val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
-
-val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
-
val cons : 'a -> 'a list -> 'a list
val hdTl : 'a list -> 'a * 'a list
@@ -448,10 +383,6 @@
(* Strings. *)
(* ------------------------------------------------------------------------- *)
-val implode : char list -> string (* MODIFIED by Jasmin Blanchette *)
-
-val explode : string -> char list (* MODIFIED by Jasmin Blanchette *)
-
val rot : int -> char -> char
val charToInt : char -> int option
@@ -554,7 +485,9 @@
val try : ('a -> 'b) -> 'a -> 'b
-val chat : string -> unit
+val chat : string -> unit (* stdout *)
+
+val chide : string -> unit (* stderr *)
val warn : string -> unit
@@ -568,7 +501,7 @@
end
-(**** Original file: Useful.sml ****)
+(**** Original file: src/Useful.sml ****)
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
@@ -622,9 +555,7 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val print = TextIO.print; (* MODIFIED by Jasmin Blanchette *)
-
-val tracePrint = Unsynchronized.ref print;
+val tracePrint = Unsynchronized.ref TextIO.print;
fun trace mesg = !tracePrint mesg;
@@ -744,10 +675,6 @@
(* Lists. *)
(* ------------------------------------------------------------------------- *)
-val foldl = List.foldl; (* MODIFIED by Jasmin Blanchette *)
-
-val foldr = List.foldr; (* MODIFIED by Jasmin Blanchette *)
-
fun cons x y = x :: y;
fun hdTl l = (hd l, tl l);
@@ -783,19 +710,22 @@
fun zip xs ys = zipWith pair xs ys;
-fun unzip ab =
- foldl (fn ((x, y), (xs, ys)) => (x :: xs, y :: ys)) ([], []) (rev ab);
+local
+ fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
+in
+ fun unzip ab = List.foldl inc ([],[]) (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 =>
- let val xs' = rev xs in aux xs' [] xs' (rev ys) end
- end;
+ 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 =>
+ let val xs' = rev xs in aux xs' [] xs' (rev ys) end
+ end;
fun cart xs ys = cartwith pair xs ys;
@@ -914,15 +844,32 @@
fun delete x s = List.filter (not o equal x) s;
-fun setify s = rev (foldl (fn (v,x) => if mem v x then x else v :: x) [] s);
-
-fun union s t = foldl (fn (v,x) => if mem v t then x else v :: x) t (rev s);
+local
+ fun inc (v,x) = if mem v x then x else v :: x;
+in
+ fun setify s = rev (List.foldl inc [] s);
+end;
+
+fun union s t =
+ let
+ fun inc (v,x) = if mem v t then x else v :: x
+ in
+ List.foldl inc t (rev s)
+ end;
fun intersect s t =
- foldl (fn (v,x) => if mem v t then v :: x else x) [] (rev s);
+ let
+ fun inc (v,x) = if mem v t then v :: x else x
+ in
+ List.foldl inc [] (rev s)
+ end;
fun difference s t =
- foldl (fn (v,x) => if mem v t then x else v :: x) [] (rev s);
+ let
+ fun inc (v,x) = if mem v t then x else v :: x
+ in
+ List.foldl inc [] (rev s)
+ end;
fun subset s t = List.all (fn x => mem x t) s;
@@ -1032,8 +979,7 @@
val primesList = Unsynchronized.ref [2];
in
- (* MODIFIED by Jasmin Blanchette *)
- fun primes n = CRITICAL (fn () =>
+ fun primes n = Metis_Portable.critical (fn () =>
let
val Unsynchronized.ref ps = primesList
@@ -1048,11 +994,10 @@
in
ps
end
- end);
-end;
-
-(* MODIFIED by Jasmin Blanchette *)
-fun primesUpTo n = CRITICAL (fn () =>
+ end) ();
+end;
+
+fun primesUpTo n = Metis_Portable.critical (fn () =>
let
fun f k =
let
@@ -1064,22 +1009,18 @@
end
in
f 8
- end);
+ end) ();
(* ------------------------------------------------------------------------- *)
(* Strings. *)
(* ------------------------------------------------------------------------- *)
-val implode = String.implode (* MODIFIED by Jasmin Blanchette *)
-
-val explode = String.explode (* MODIFIED by Jasmin Blanchette *)
-
local
fun len l = (length l, l)
- val upper = len (explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
-
- val lower = len (explode "abcdefghijklmnopqrstuvwxyz");
+ 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);
@@ -1118,7 +1059,7 @@
let
fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
in
- fn n => implode (dup n [])
+ fn n => String.implode (dup n [])
end;
fun chomp s =
@@ -1130,14 +1071,15 @@
end;
local
- fun chop [] = []
- | chop (l as (h :: t)) = if Char.isSpace h then chop t else l;
-in
- val trim = implode o chop o rev o chop o rev o explode;
-end;
-
-fun join _ [] = ""
- | join s (h :: t) = foldl (fn (x,y) => y ^ s ^ x) h t;
+ 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 rev o chop o rev o String.explode;
+end;
+
+val join = String.concatWith;
local
fun match [] l = SOME l
@@ -1145,18 +1087,19 @@
| match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
fun stringify acc [] = acc
- | stringify acc (h :: t) = stringify (implode h :: acc) t;
+ | 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 [] (rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
| SOME rest => div1 (rev recent :: prev) [] rest
in
- fn s => div1 [] [] (explode s)
+ fn s => div1 [] [] (String.explode s)
end;
end;
@@ -1286,24 +1229,22 @@
local
val generator = Unsynchronized.ref 0
in
- (* MODIFIED by Jasmin Blanchette *)
- fun newInt () = CRITICAL (fn () =>
+ fun newInt () = Metis_Portable.critical (fn () =>
let
val n = !generator
val () = generator := n + 1
in
n
- end);
+ end) ();
fun newInts 0 = []
- (* MODIFIED by Jasmin Blanchette *)
- | newInts k = CRITICAL (fn () =>
+ | newInts k = Metis_Portable.critical (fn () =>
let
val n = !generator
val () = generator := n + k
in
interval n k
- end);
+ end) ();
end;
fun withRef (r,new) f x =
@@ -1383,10 +1324,12 @@
(* Profiling and error reporting. *)
(* ------------------------------------------------------------------------- *)
-fun chat s = TextIO.output (TextIO.stdErr, s ^ "\n");
-
-local
- fun err x s = chat (x ^ ": " ^ s);
+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
fun try f x = f x
handle e as Error _ => (err "try" (errorToString e); raise e)
@@ -1431,7 +1374,7 @@
end
-(**** Original file: Lazy.sig ****)
+(**** Original file: src/Lazy.sig ****)
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
@@ -1453,7 +1396,7 @@
end
-(**** Original file: Lazy.sml ****)
+(**** Original file: src/Lazy.sml ****)
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
@@ -1494,11 +1437,11 @@
end
-(**** Original file: Ordered.sig ****)
+(**** Original file: src/Ordered.sig ****)
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Ordered =
@@ -1530,11 +1473,11 @@
end
-(**** Original file: Ordered.sml ****)
+(**** Original file: src/Ordered.sml ****)
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_IntOrdered =
@@ -1556,7 +1499,7 @@
structure Metis_StringOrdered =
struct type t = string val compare = String.compare end;
-(**** Original file: Map.sig ****)
+(**** Original file: src/Map.sig ****)
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
@@ -1749,7 +1692,7 @@
end
-(**** Original file: Map.sml ****)
+(**** Original file: src/Map.sml ****)
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
@@ -2632,38 +2575,40 @@
(* ------------------------------------------------------------------------- *)
datatype ('key,'value) iterator =
- LR of ('key * 'value) * ('key,'value) tree * ('key,'value) node list
- | Metis_RL of ('key * 'value) * ('key,'value) tree * ('key,'value) node list;
-
-fun fromSpineLR nodes =
+ 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 (LR ((key,value),right,nodes));
-
-fun fromSpineRL nodes =
+ SOME (LeftToRightIterator ((key,value),right,nodes));
+
+fun fromSpineRightToLeftIterator nodes =
case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
- SOME (Metis_RL ((key,value),left,nodes));
-
-fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
-
-fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
-
-fun treeMkIterator tree = addLR [] tree;
-
-fun treeMkRevIterator tree = addRL [] tree;
+ 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
- LR (key_value,_,_) => key_value
- | Metis_RL (key_value,_,_) => key_value;
+ LeftToRightIterator (key_value,_,_) => key_value
+ | RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter =
case iter of
- LR (_,tree,nodes) => addLR nodes tree
- | Metis_RL (_,tree,nodes) => addRL nodes tree;
+ LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
+ | RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io =
case io of
@@ -3177,7 +3122,7 @@
end
-(**** Original file: KeyMap.sig ****)
+(**** Original file: src/KeyMap.sig ****)
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
@@ -3376,7 +3321,7 @@
end
-(**** Original file: KeyMap.sml ****)
+(**** Original file: src/KeyMap.sml ****)
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
@@ -4267,38 +4212,40 @@
(* ------------------------------------------------------------------------- *)
datatype 'value iterator =
- LR of (key * 'value) * 'value tree * 'value node list
- | Metis_RL of (key * 'value) * 'value tree * 'value node list;
-
-fun fromSpineLR nodes =
+ 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 (LR ((key,value),right,nodes));
-
-fun fromSpineRL nodes =
+ SOME (LeftToRightIterator ((key,value),right,nodes));
+
+fun fromSpineRightToLeftIterator nodes =
case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
- SOME (Metis_RL ((key,value),left,nodes));
-
-fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
-
-fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
-
-fun treeMkIterator tree = addLR [] tree;
-
-fun treeMkRevIterator tree = addRL [] tree;
+ 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
- LR (key_value,_,_) => key_value
- | Metis_RL (key_value,_,_) => key_value;
+ LeftToRightIterator (key_value,_,_) => key_value
+ | RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter =
case iter of
- LR (_,tree,nodes) => addLR nodes tree
- | Metis_RL (_,tree,nodes) => addRL nodes tree;
+ LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
+ | RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io =
case io of
@@ -4821,7 +4768,7 @@
structure Metis_StringMap =
Metis_KeyMap (Metis_StringOrdered);
-(**** Original file: Set.sig ****)
+(**** Original file: src/Set.sig ****)
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
@@ -4993,7 +4940,7 @@
end
-(**** Original file: Set.sml ****)
+(**** Original file: src/Set.sml ****)
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
@@ -5327,7 +5274,7 @@
end
-(**** Original file: ElementSet.sig ****)
+(**** Original file: src/ElementSet.sig ****)
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
@@ -5505,7 +5452,7 @@
end
-(**** Original file: ElementSet.sml ****)
+(**** Original file: src/ElementSet.sml ****)
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
@@ -5855,11 +5802,11 @@
structure Metis_StringSet =
Metis_ElementSet (Metis_StringMap);
-(**** Original file: Sharing.sig ****)
+(**** Original file: src/Sharing.sig ****)
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Sharing =
@@ -5903,11 +5850,11 @@
end
-(**** Original file: Sharing.sml ****)
+(**** Original file: src/Sharing.sml ****)
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Sharing :> Metis_Sharing =
@@ -6064,11 +6011,11 @@
end
-(**** Original file: Stream.sig ****)
+(**** Original file: src/Stream.sig ****)
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Stream =
@@ -6176,18 +6123,16 @@
end
-(**** Original file: Stream.sml ****)
+(**** Original file: src/Stream.sml ****)
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Stream :> Metis_Stream =
struct
-open Metis_Useful; (* MODIFIED by Jasmin Blanchette *)
-
val K = Metis_Useful.K;
val pair = Metis_Useful.pair;
@@ -6381,9 +6326,9 @@
fun listConcat s = concat (map fromList s);
-fun toString s = implode (toList s);
-
-fun fromString s = fromList (explode s);
+fun toString s = String.implode (toList s);
+
+fun fromString s = fromList (String.explode s);
fun toTextFile {filename = f} s =
let
@@ -6415,11 +6360,11 @@
end
-(**** Original file: Heap.sig ****)
+(**** Original file: src/Heap.sig ****)
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Heap =
@@ -6449,11 +6394,11 @@
end
-(**** Original file: Heap.sml ****)
+(**** Original file: src/Heap.sml ****)
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Heap :> Metis_Heap =
@@ -6529,32 +6474,44 @@
end
-(**** Original file: Print.sig ****)
+(**** Original file: src/Print.sig ****)
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Print =
sig
(* ------------------------------------------------------------------------- *)
+(* Escaping strings. *)
+(* ------------------------------------------------------------------------- *)
+
+val escapeString : {escape : char list} -> string -> string
+
+(* ------------------------------------------------------------------------- *)
+(* A type of strings annotated with their size. *)
+(* ------------------------------------------------------------------------- *)
+
+type stringSize = string * int
+
+val mkStringSize : string -> stringSize
+
+(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
datatype breakStyle = Consistent | Inconsistent
-datatype ppStep =
+datatype step =
BeginBlock of breakStyle * int
| EndBlock
- | AddString of string
+ | AddString of stringSize
| AddBreak of int
| AddNewline
-type ppstream = ppStep Metis_Stream.stream
-
-type 'a pp = 'a -> ppstream
+type ppstream = step Metis_Stream.stream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer primitives. *)
@@ -6564,7 +6521,7 @@
val endBlock : ppstream
-val addString : string -> ppstream
+val addString : stringSize -> ppstream
val addBreak : int -> ppstream
@@ -6584,18 +6541,24 @@
val blockProgram : breakStyle -> int -> ppstream list -> ppstream
-val bracket : string -> string -> ppstream -> ppstream
-
-val field : string -> ppstream -> ppstream
-
-val record : (string * ppstream) list -> ppstream
+(* ------------------------------------------------------------------------- *)
+(* Executing pretty-printers to generate lines. *)
+(* ------------------------------------------------------------------------- *)
+
+val execute :
+ {lineLength : int} -> ppstream ->
+ {indent : int, line : string} Metis_Stream.stream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
+type 'a pp = 'a -> ppstream
+
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
+val ppString : string pp
+
val ppBracket : string -> string -> 'a pp -> 'a pp
val ppOp : string -> ppstream
@@ -6614,8 +6577,6 @@
val ppChar : char pp
-val ppString : string pp
-
val ppEscapeString : {escape : char list} -> string pp
val ppUnit : unit pp
@@ -6644,7 +6605,7 @@
val ppBreakStyle : breakStyle pp
-val ppPpStep : ppStep pp
+val ppStep : step pp
val ppPpstream : ppstream pp
@@ -6652,28 +6613,27 @@
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
+type token = string
+
+datatype assoc =
+ LeftAssoc
+ | NonAssoc
+ | RightAssoc
+
datatype infixes =
Infixes of
- {token : string,
+ {token : token,
precedence : int,
- leftAssoc : bool} list
+ assoc : assoc} list
val tokensInfixes : infixes -> Metis_StringSet.set
-val layerInfixes :
- infixes ->
- {tokens : {leftSpaces : int, token : string, rightSpaces : int} list,
- leftAssoc : bool} list
+val layerInfixes : infixes -> {tokens : Metis_StringSet.set, assoc : assoc} list
val ppInfixes :
- infixes -> ('a -> (string * 'a * 'a) option) -> ('a * bool) pp ->
- ('a * bool) pp
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
-(* ------------------------------------------------------------------------- *)
-
-val execute : {lineLength : int} -> ppstream -> string Metis_Stream.stream
+ infixes ->
+ ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
+ ('a * bool) pp -> ('a * bool) pp
(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers with a global line length. *)
@@ -6689,11 +6649,11 @@
end
-(**** Original file: Print.sml ****)
+(**** Original file: src/Print.sml ****)
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Print :> Metis_Print =
@@ -6722,47 +6682,69 @@
| Metis_Stream.Cons (h,t) => revAppend h (revConcat o t);
local
- fun join current prev = (prev ^ "\n", current);
-in
- fun joinNewline strm =
- case strm of
- Metis_Stream.Nil => Metis_Stream.Nil
- | Metis_Stream.Cons (h,t) => Metis_Stream.maps join Metis_Stream.singleton h (t ());
-end;
-
-local
fun calcSpaces n = nChars #" " n;
- val cachedSpaces = Vector.tabulate (initialLineLength,calcSpaces);
+ val cacheSize = 2 * initialLineLength;
+
+ val cachedSpaces = Vector.tabulate (cacheSize,calcSpaces);
in
fun nSpaces n =
- if n < initialLineLength then Vector.sub (cachedSpaces,n)
+ if n < cacheSize then Vector.sub (cachedSpaces,n)
else calcSpaces n;
end;
(* ------------------------------------------------------------------------- *)
+(* Escaping strings. *)
+(* ------------------------------------------------------------------------- *)
+
+fun escapeString {escape} =
+ let
+ val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
+
+ fun escapeChar c =
+ case c of
+ #"\\" => "\\\\"
+ | #"\n" => "\\n"
+ | #"\t" => "\\t"
+ | _ =>
+ case List.find (equal c o fst) escapeMap of
+ SOME (_,s) => s
+ | NONE => str c
+ in
+ String.translate escapeChar
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of strings annotated with their size. *)
+(* ------------------------------------------------------------------------- *)
+
+type stringSize = string * int;
+
+fun mkStringSize s = (s, size s);
+
+val emptyStringSize = mkStringSize "";
+
+(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
datatype breakStyle = Consistent | Inconsistent;
-datatype ppStep =
+datatype step =
BeginBlock of breakStyle * int
| EndBlock
- | AddString of string
+ | AddString of stringSize
| AddBreak of int
| AddNewline;
-type ppstream = ppStep Metis_Stream.stream;
-
-type 'a pp = 'a -> ppstream;
+type ppstream = step Metis_Stream.stream;
fun breakStyleToString style =
case style of
Consistent => "Consistent"
| Inconsistent => "Inconsistent";
-fun ppStepToString step =
+fun stepToString step =
case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
@@ -6802,330 +6784,6 @@
fun blockProgram style indent pps = block style indent (program pps);
-fun bracket l r pp =
- blockProgram Inconsistent (size l)
- [addString l,
- pp,
- addString r];
-
-fun field f pp =
- blockProgram Inconsistent 2
- [addString (f ^ " ="),
- addBreak 1,
- pp];
-
-val record =
- let
- val sep = sequence (addString ",") (addBreak 1)
-
- fun recordField (f,pp) = field f pp
-
- fun sepField f = sequence sep (recordField f)
-
- fun fields [] = []
- | fields (f :: fs) = recordField f :: map sepField fs
- in
- bracket "{" "}" o blockProgram Consistent 0 o fields
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer combinators. *)
-(* ------------------------------------------------------------------------- *)
-
-fun ppMap f ppB a : ppstream = ppB (f a);
-
-fun ppBracket l r ppA a = bracket l r (ppA a);
-
-fun ppOp s = sequence (if s = "" then skip else addString s) (addBreak 1);
-
-fun ppOp2 ab ppA ppB (a,b) =
- blockProgram Inconsistent 0
- [ppA a,
- ppOp ab,
- ppB b];
-
-fun ppOp3 ab bc ppA ppB ppC (a,b,c) =
- blockProgram Inconsistent 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 => blockProgram Inconsistent 0 (ppA h :: 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) =>
- blockProgram Inconsistent 0
- [ppA h,
- Metis_Stream.concat (Metis_Stream.map ppOpA (t ()))]
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printers for common types. *)
-(* ------------------------------------------------------------------------- *)
-
-fun ppChar c = addString (str c);
-
-val ppString = addString;
-
-fun ppEscapeString {escape} =
- let
- val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
-
- fun escapeChar c =
- case c of
- #"\\" => "\\\\"
- | #"\n" => "\\n"
- | #"\t" => "\\t"
- | _ =>
- case List.find (equal c o fst) escapeMap of
- SOME (_,s) => s
- | NONE => str c
- in
- fn s => addString (String.translate escapeChar s)
- end;
-
-val ppUnit : unit pp = K (addString "()");
-
-fun ppBool b = addString (if b then "true" else "false");
-
-fun ppInt i = addString (Int.toString i);
-
-local
- val ppNeg = addString "~"
- and ppSep = addString ","
- and ppZero = addString "0"
- and ppZeroZero = addString "00";
-
- fun ppIntBlock i =
- if i < 10 then sequence ppZeroZero (ppInt i)
- else if 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;
-
-fun ppReal r = addString (Real.toString r);
-
-fun ppPercent p = addString (percentToString p);
-
-fun ppOrder x =
- addString
- (case x of
- LESS => "Less"
- | EQUAL => "Equal"
- | GREATER => "Greater");
-
-fun ppList ppA = ppBracket "[" "]" (ppOpList "," ppA);
-
-fun ppStream ppA = ppBracket "[" "]" (ppOpStream "," ppA);
-
-fun ppOption ppA ao =
- case ao of
- SOME a => ppA a
- | NONE => addString "-";
-
-fun ppPair ppA ppB = ppBracket "(" ")" (ppOp2 "," ppA ppB);
-
-fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppOp3 "," "," ppA ppB ppC);
-
-fun ppBreakStyle style = addString (breakStyleToString style);
-
-fun ppPpStep step =
- let
- val cmd = ppStepToString step
- in
- blockProgram Inconsistent 2
- (addString cmd ::
- (case step of
- BeginBlock style_indent =>
- [addBreak 1,
- ppPair ppBreakStyle ppInt style_indent]
- | EndBlock => []
- | AddString s =>
- [addBreak 1,
- addString ("\"" ^ s ^ "\"")]
- | AddBreak n =>
- [addBreak 1,
- ppInt n]
- | AddNewline => []))
- end;
-
-val ppPpstream = ppStream ppPpStep;
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printing infix operators. *)
-(* ------------------------------------------------------------------------- *)
-
-datatype infixes =
- Infixes of
- {token : string,
- precedence : int,
- leftAssoc : bool} list;
-
-local
- fun chop l =
- case l of
- #" " :: l => let val (n,l) = chop l in (n + 1, l) end
- | _ => (0,l);
-in
- fun opSpaces tok =
- let
- val tok = explode tok
- val (r,tok) = chop (rev tok)
- val (l,tok) = chop (rev tok)
- val tok = implode tok
- in
- {leftSpaces = l, token = tok, rightSpaces = r}
- end;
-end;
-
-fun ppOpSpaces {leftSpaces,token,rightSpaces} =
- let
- val leftSpacesToken =
- if leftSpaces = 0 then token else nSpaces leftSpaces ^ token
- in
- sequence
- (addString leftSpacesToken)
- (addBreak rightSpaces)
- end;
-
-local
- fun new t l acc = {tokens = [opSpaces t], leftAssoc = l} :: acc;
-
- fun add t l acc =
- case acc of
- [] => raise Bug "Metis_Print.layerInfixOps.layer"
- | {tokens = ts, leftAssoc = l'} :: acc =>
- if l = l' then {tokens = opSpaces t :: ts, leftAssoc = l} :: acc
- else raise Bug "Metis_Print.layerInfixOps: mixed assocs";
-
- fun layer ({token = t, precedence = p, leftAssoc = l}, (acc,p')) =
- let
- val acc = if p = p' then add t l acc else new t l acc
- in
- (acc,p)
- end;
-in
- fun layerInfixes (Infixes i) =
- case sortMap #precedence Int.compare i of
- [] => []
- | {token = t, precedence = p, leftAssoc = l} :: i =>
- let
- val acc = new t l []
-
- val (acc,_) = List.foldl layer (acc,p) i
- in
- acc
- end;
-end;
-
-val tokensLayeredInfixes =
- let
- fun addToken ({leftSpaces = _, token = t, rightSpaces = _}, s) =
- Metis_StringSet.add s t
-
- fun addTokens ({tokens = t, leftAssoc = _}, s) =
- List.foldl addToken s t
- in
- List.foldl addTokens Metis_StringSet.empty
- end;
-
-val tokensInfixes = tokensLayeredInfixes o layerInfixes;
-
-local
- val mkTokenMap =
- let
- fun add (token,m) =
- let
- val {leftSpaces = _, token = t, rightSpaces = _} = token
- in
- Metis_StringMap.insert m (t, ppOpSpaces token)
- end
- in
- List.foldl add (Metis_StringMap.new ())
- end;
-in
- fun ppGenInfix {tokens,leftAssoc} =
- let
- val tokenMap = mkTokenMap tokens
- in
- fn dest => fn ppSub =>
- let
- fun dest' tm =
- case dest tm of
- NONE => NONE
- | SOME (t,a,b) =>
- case Metis_StringMap.peek tokenMap t of
- NONE => NONE
- | SOME p => SOME (p,a,b)
-
- fun ppGo (tmr as (tm,r)) =
- case dest' tm of
- NONE => ppSub tmr
- | SOME (p,a,b) =>
- program
- [(if leftAssoc then ppGo else ppSub) (a,true),
- p,
- (if leftAssoc then ppSub else ppGo) (b,r)]
- in
- fn tmr as (tm,_) =>
- if Option.isSome (dest' tm) then
- block Inconsistent 0 (ppGo tmr)
- else
- ppSub tmr
- end
- end;
-end
-
-fun ppInfixes ops =
- let
- val layeredOps = layerInfixes ops
-
- val toks = tokensLayeredInfixes layeredOps
-
- val iprinters = List.map ppGenInfix layeredOps
- in
- fn dest => fn ppSub =>
- let
- fun printer sub = foldl (fn (ip,p) => ip dest p) sub iprinters
-
- fun isOp t =
- case dest t of
- SOME (x,_,_) => Metis_StringSet.member x toks
- | NONE => false
-
- fun subpr (tmr as (tm,_)) =
- if isOp tm then
- blockProgram Inconsistent 1
- [addString "(",
- printer subpr (tm,false),
- addString ")"]
- else
- ppSub tmr
- in
- fn tmr => block Inconsistent 0 (printer subpr tmr)
- end
- end;
-
(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers to generate lines. *)
(* ------------------------------------------------------------------------- *)
@@ -7189,18 +6847,22 @@
val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
local
- fun render acc [] = acc
- | render acc (chunk :: chunks) =
- case chunk of
- StringChunk {string = s, ...} => render (acc ^ s) chunks
- | BreakChunk n => render (acc ^ nSpaces n) chunks
- | BlockChunk (Block {chunks = l, ...}) =>
- render acc (List.revAppend (l,chunks));
-in
- fun renderChunks indent chunks = render (nSpaces indent) (rev chunks);
-
- fun renderChunk indent chunk = renderChunks indent [chunk];
-end;
+ fun flatten acc chunks =
+ case chunks of
+ [] => rev acc
+ | chunk :: chunks =>
+ case chunk of
+ StringChunk {string = s, ...} => flatten (s :: acc) chunks
+ | BreakChunk n => flatten (nSpaces n :: acc) chunks
+ | BlockChunk (Block {chunks = l, ...}) =>
+ flatten acc (List.revAppend (l,chunks));
+in
+ fun renderChunks indent chunks =
+ {indent = indent,
+ line = String.concat (flatten [] (rev chunks))};
+end;
+
+fun renderChunk indent chunk = renderChunks indent [chunk];
fun isEmptyBlock block =
let
@@ -7216,6 +6878,7 @@
empty
end;
+(*BasicDebug
fun checkBlock ind block =
let
val Block {indent, style = _, size, chunks} = block
@@ -7251,6 +6914,7 @@
in
check initialIndent o rev
end;
+*)
val initialBlock =
let
@@ -7662,12 +7326,10 @@
(lines,state)
end;
- fun executeAddString lineLength s lines state =
+ fun executeAddString lineLength (s,n) lines state =
let
val State {blocks,lineIndent,lineSize} = state
- val n = size s
-
val blocks =
case blocks of
[] => raise Bug "Metis_Print.executeAddString: no block"
@@ -7754,10 +7416,13 @@
fun executeAddNewline lineLength lines state =
let
- val (lines,state) = executeAddString lineLength "" lines state
- val (lines,state) = executeBigBreak lineLength lines state
- in
- executeAddString lineLength "" lines state
+ val (lines,state) =
+ executeAddString lineLength emptyStringSize lines state
+
+ val (lines,state) =
+ executeBigBreak lineLength lines state
+ in
+ executeAddString lineLength emptyStringSize lines state
end;
fun final lineLength lines state =
@@ -7801,7 +7466,7 @@
(lines,state)
end
handle Bug bug =>
- raise Bug ("Metis_Print.advance: after " ^ ppStepToString step ^
+ raise Bug ("Metis_Print.advance: after " ^ stepToString step ^
" command:\n" ^ bug)
*)
in
@@ -7810,26 +7475,377 @@
end;
(* ------------------------------------------------------------------------- *)
+(* Pretty-printer combinators. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a pp = 'a -> ppstream;
+
+fun ppMap f ppB a : ppstream = ppB (f a);
+
+fun ppBracket' l r ppA a =
+ let
+ val (_,n) = l
+ in
+ blockProgram Inconsistent n
+ [addString l,
+ ppA a,
+ addString r]
+ end;
+
+fun ppOp' s = sequence (addString s) (addBreak 1);
+
+fun ppOp2' ab ppA ppB (a,b) =
+ blockProgram Inconsistent 0
+ [ppA a,
+ ppOp' ab,
+ ppB b];
+
+fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
+ blockProgram Inconsistent 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 => blockProgram Inconsistent 0 (ppA h :: 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) =>
+ blockProgram Inconsistent 0
+ [ppA h,
+ Metis_Stream.concat (Metis_Stream.map ppOpA (t ()))]
+ end;
+
+fun ppBracket l r = ppBracket' (mkStringSize l) (mkStringSize r);
+
+fun ppOp s = ppOp' (mkStringSize s);
+
+fun ppOp2 ab = ppOp2' (mkStringSize ab);
+
+fun ppOp3 ab bc = ppOp3' (mkStringSize ab) (mkStringSize bc);
+
+fun ppOpList s = ppOpList' (mkStringSize s);
+
+fun ppOpStream s = ppOpStream' (mkStringSize s);
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printers for common types. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppChar c = addString (str c, 1);
+
+fun ppString s = addString (mkStringSize 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)
+ else if 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 =
+ case ord of
+ LESS => ppLess
+ | EQUAL => ppEqual
+ | GREATER => ppGreater;
+end;
+
+local
+ val left = mkStringSize "["
+ and right = mkStringSize "]"
+ and sep = mkStringSize ",";
+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 = mkStringSize "("
+ and right = mkStringSize ")"
+ and sep = mkStringSize ",";
+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;
+
+val ppBreakStyle = ppMap breakStyleToString ppString;
+
+val ppStep = ppMap stepToString ppString;
+
+val ppStringSize =
+ let
+ val left = mkStringSize "\""
+ and right = mkStringSize "\""
+ and escape = {escape = [#"\""]}
+
+ val pp = ppBracket' left right (ppEscapeString escape)
+ in
+ fn (s,n) => if size s = n then pp s else ppPair pp ppInt (s,n)
+ end;
+
+fun ppStep step =
+ blockProgram Inconsistent 2
+ (ppStep step ::
+ (case step of
+ BeginBlock style_indent =>
+ [addBreak 1,
+ ppPair ppBreakStyle ppInt style_indent]
+ | EndBlock => []
+ | AddString s =>
+ [addBreak 1,
+ ppStringSize s]
+ | AddBreak n =>
+ [addBreak 1,
+ ppInt n]
+ | AddNewline => []));
+
+val ppPpstream = ppStream ppStep;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing infix operators. *)
+(* ------------------------------------------------------------------------- *)
+
+type token = string;
+
+datatype assoc =
+ LeftAssoc
+ | NonAssoc
+ | RightAssoc;
+
+datatype infixes =
+ Infixes of
+ {token : token,
+ precedence : int,
+ assoc : assoc} list;
+
+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
+ else raise 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 block Inconsistent 0 (ppLayer tm_t_a_b_r)
+ else ppLower tm_t_a_b_r
+ end;
+
+local
+ val leftBrack = mkStringSize "("
+ and rightBrack = mkStringSize ")";
+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;
+
+(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers with a global line length. *)
(* ------------------------------------------------------------------------- *)
val lineLength = Unsynchronized.ref initialLineLength;
fun toStream ppA a =
- Metis_Stream.map (fn s => s ^ "\n")
+ Metis_Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
(execute {lineLength = !lineLength} (ppA a));
-fun toString ppA a =
- case execute {lineLength = !lineLength} (ppA a) of
- Metis_Stream.Nil => ""
- | Metis_Stream.Cons (h,t) => Metis_Stream.foldl (fn (s,z) => z ^ "\n" ^ s) h (t ());
-
-fun trace ppX nameX x =
- Metis_Useful.trace (toString (ppOp2 " =" ppString ppX) (nameX,x) ^ "\n");
-
-end
-
-(**** Original file: Parse.sig ****)
+local
+ fun inc {indent,line} acc = line :: nSpaces indent :: acc;
+
+ fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
+in
+ fun toString ppA a =
+ case execute {lineLength = !lineLength} (ppA a) of
+ Metis_Stream.Nil => ""
+ | Metis_Stream.Cons (h,t) =>
+ let
+ val lines = Metis_Stream.foldl incn (inc h []) (t ())
+ in
+ String.concat (rev lines)
+ end;
+end;
+
+local
+ val sep = mkStringSize " =";
+in
+ fun trace ppX nameX x =
+ Metis_Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
+end;
+
+end
+
+(**** Original file: src/Parse.sig ****)
(* ========================================================================= *)
(* PARSING *)
@@ -7932,8 +7948,9 @@
(* ------------------------------------------------------------------------- *)
val parseInfixes :
- Metis_Print.infixes -> (string * 'a * 'a -> 'a) -> (string,'a) parser ->
- (string,'a) parser
+ Metis_Print.infixes ->
+ (Metis_Print.token * 'a * 'a -> 'a) -> ('b,Metis_Print.token) parser ->
+ ('b,'a) parser -> ('b,'a) parser
(* ------------------------------------------------------------------------- *)
(* Quotations. *)
@@ -7945,7 +7962,7 @@
end
-(**** Original file: Parse.sml ****)
+(**** Original file: src/Parse.sml ****)
(* ========================================================================= *)
(* PARSING *)
@@ -8083,7 +8100,7 @@
val Unsynchronized.ref (n,_,l2,l3) = lastLine
val () = lastLine := (n + 1, l2, l3, line)
in
- explode line
+ String.explode line
end
in
Metis_Stream.memoize (Metis_Stream.map saveLast lines)
@@ -8109,7 +8126,7 @@
[] => nothing
| c :: cs => (exactChar c ++ exactCharList cs) >> snd;
-fun exactString s = exactCharList (explode s);
+fun exactString s = exactCharList (String.explode s);
fun escapeString {escape} =
let
@@ -8132,7 +8149,7 @@
((exactChar #"\\" ++ escapeParser) >> snd) ||
some isNormal
in
- many charParser >> implode
+ many charParser >> String.implode
end;
local
@@ -8145,46 +8162,51 @@
val atLeastOneSpace = atLeastOne space >> K ();
end;
-fun fromString parser s = fromList parser (explode s);
+fun fromString parser s = fromList parser (String.explode s);
(* ------------------------------------------------------------------------- *)
(* Infix operators. *)
(* ------------------------------------------------------------------------- *)
-fun parseGenInfix update sof toks parse inp =
- let
- val (e,rest) = parse inp
-
- val continue =
- case rest of
- Metis_Stream.Nil => NONE
- | Metis_Stream.Cons (h_t as (h,_)) =>
- if Metis_StringSet.member h toks then SOME h_t else NONE
- in
- case continue of
- NONE => (sof e, rest)
- | SOME (h,t) => parseGenInfix update (update sof h e) toks parse (t ())
- end;
-
-local
- fun add ({leftSpaces = _, token = t, rightSpaces = _}, s) = Metis_StringSet.add s t;
-
- fun parse leftAssoc toks con =
- let
- val update =
- if leftAssoc then (fn f => fn t => fn a => fn b => con (t, f a, b))
- else (fn f => fn t => fn a => fn b => f (con (t, a, b)))
- in
- parseGenInfix update I toks
- end;
-in
- fun parseLayeredInfixes {tokens,leftAssoc} =
- let
- val toks = List.foldl add Metis_StringSet.empty tokens
- in
- parse leftAssoc toks
- end;
-end;
+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
+ else raise 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 =>
+ (case 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
@@ -8192,7 +8214,8 @@
val iparsers = List.map parseLayeredInfixes layeredOps
in
- fn con => fn subparser => foldl (fn (p,sp) => p con sp) subparser iparsers
+ fn mk => fn tokParser => fn subParser =>
+ List.foldr (fn (p,sp) => p mk tokParser sp) subParser iparsers
end;
(* ------------------------------------------------------------------------- *)
@@ -8206,14 +8229,14 @@
fun expand (QUOTE q, s) = s ^ q
| expand (ANTIQUOTE a, s) = s ^ printer a
- val string = foldl expand "" quote
+ val string = List.foldl expand "" quote
in
parser string
end;
end
-(**** Original file: Name.sig ****)
+(**** Original file: src/Name.sig ****)
(* ========================================================================= *)
(* NAMES *)
@@ -8261,7 +8284,7 @@
end
-(**** Original file: Name.sml ****)
+(**** Original file: src/Name.sml ****)
(* ========================================================================= *)
(* NAMES *)
@@ -8349,24 +8372,24 @@
structure Metis_NameSet =
struct
- 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: NameArity.sig ****)
+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-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_NameArity =
@@ -8412,11 +8435,11 @@
end
-(**** Original file: NameArity.sml ****)
+(**** Original file: src/NameArity.sml ****)
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_NameArity :> Metis_NameArity =
@@ -8462,7 +8485,7 @@
fun pp (n,i) =
Metis_Print.blockProgram Metis_Print.Inconsistent 0
[Metis_Name.pp n,
- Metis_Print.addString "/",
+ Metis_Print.ppString "/",
Metis_Print.ppInt i];
end
@@ -8473,40 +8496,41 @@
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;
+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: Term.sig ****)
+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 *)
@@ -8696,7 +8720,7 @@
end
-(**** Original file: Term.sml ****)
+(**** Original file: src/Term.sml ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
@@ -9048,7 +9072,7 @@
val isApp = can destApp;
-fun listMkApp (f,l) = foldl mkApp f l;
+fun listMkApp (f,l) = List.foldl mkApp f l;
local
fun strip tms tm =
@@ -9068,38 +9092,38 @@
val infixes =
(Unsynchronized.ref o Metis_Print.Infixes)
[(* ML symbols *)
- {token = " / ", precedence = 7, leftAssoc = true},
- {token = " div ", precedence = 7, leftAssoc = true},
- {token = " mod ", precedence = 7, leftAssoc = true},
- {token = " * ", precedence = 7, leftAssoc = true},
- {token = " + ", precedence = 6, leftAssoc = true},
- {token = " - ", precedence = 6, leftAssoc = true},
- {token = " ^ ", precedence = 6, leftAssoc = true},
- {token = " @ ", precedence = 5, leftAssoc = false},
- {token = " :: ", precedence = 5, leftAssoc = false},
- {token = " = ", precedence = 4, leftAssoc = true},
- {token = " <> ", precedence = 4, leftAssoc = true},
- {token = " <= ", precedence = 4, leftAssoc = true},
- {token = " < ", precedence = 4, leftAssoc = true},
- {token = " >= ", precedence = 4, leftAssoc = true},
- {token = " > ", precedence = 4, leftAssoc = true},
- {token = " o ", precedence = 3, leftAssoc = true},
- {token = " -> ", precedence = 2, leftAssoc = false}, (* inferred prec *)
- {token = " : ", precedence = 1, leftAssoc = false}, (* inferred prec *)
- {token = ", ", precedence = 0, leftAssoc = false}, (* inferred prec *)
+ {token = "/", precedence = 7, assoc = Metis_Print.LeftAssoc},
+ {token = "div", precedence = 7, assoc = Metis_Print.LeftAssoc},
+ {token = "mod", precedence = 7, assoc = Metis_Print.LeftAssoc},
+ {token = "*", precedence = 7, assoc = Metis_Print.LeftAssoc},
+ {token = "+", precedence = 6, assoc = Metis_Print.LeftAssoc},
+ {token = "-", precedence = 6, assoc = Metis_Print.LeftAssoc},
+ {token = "^", precedence = 6, assoc = Metis_Print.LeftAssoc},
+ {token = "@", precedence = 5, assoc = Metis_Print.RightAssoc},
+ {token = "::", precedence = 5, assoc = Metis_Print.RightAssoc},
+ {token = "=", precedence = 4, assoc = Metis_Print.NonAssoc},
+ {token = "<>", precedence = 4, assoc = Metis_Print.NonAssoc},
+ {token = "<=", precedence = 4, assoc = Metis_Print.NonAssoc},
+ {token = "<", precedence = 4, assoc = Metis_Print.NonAssoc},
+ {token = ">=", precedence = 4, assoc = Metis_Print.NonAssoc},
+ {token = ">", precedence = 4, assoc = Metis_Print.NonAssoc},
+ {token = "o", precedence = 3, assoc = Metis_Print.LeftAssoc},
+ {token = "->", precedence = 2, assoc = Metis_Print.RightAssoc},
+ {token = ":", precedence = 1, assoc = Metis_Print.NonAssoc},
+ {token = ",", precedence = 0, assoc = Metis_Print.RightAssoc},
(* Logical connectives *)
- {token = " /\\ ", precedence = ~1, leftAssoc = false},
- {token = " \\/ ", precedence = ~2, leftAssoc = false},
- {token = " ==> ", precedence = ~3, leftAssoc = false},
- {token = " <=> ", precedence = ~4, leftAssoc = false},
+ {token = "/\\", precedence = ~1, assoc = Metis_Print.RightAssoc},
+ {token = "\\/", precedence = ~2, assoc = Metis_Print.RightAssoc},
+ {token = "==>", precedence = ~3, assoc = Metis_Print.RightAssoc},
+ {token = "<=>", precedence = ~4, assoc = Metis_Print.RightAssoc},
(* Other symbols *)
- {token = " . ", precedence = 9, leftAssoc = true}, (* function app *)
- {token = " ** ", precedence = 8, leftAssoc = true},
- {token = " ++ ", precedence = 6, leftAssoc = true},
- {token = " -- ", precedence = 6, leftAssoc = true},
- {token = " == ", precedence = 4, leftAssoc = true}];
+ {token = ".", precedence = 9, assoc = Metis_Print.LeftAssoc},
+ {token = "**", precedence = 8, assoc = Metis_Print.LeftAssoc},
+ {token = "++", precedence = 6, assoc = Metis_Print.LeftAssoc},
+ {token = "--", precedence = 6, assoc = Metis_Print.LeftAssoc},
+ {token = "==", precedence = 4, assoc = Metis_Print.NonAssoc}];
(* The negation symbol *)
@@ -9122,9 +9146,14 @@
and neg = !negation
and bracks = !brackets
- val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
-
- val bTokens = map #2 bracks @ map #3 bracks
+ 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
@@ -9138,7 +9167,15 @@
end
| _ => NONE
- val iPrinter = Metis_Print.ppInfixes iOps destI
+ 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.addBreak 1];
+
+ val iPrinter = Metis_Print.ppInfixes iOps destI iToken
val specialTokens =
Metis_StringSet.addList iTokens (neg :: quants @ ["$","(",")"] @ bTokens)
@@ -9166,8 +9203,6 @@
fun functionName bv = Metis_Print.ppMap (checkFunctionName bv) Metis_Print.ppString
- fun isI tm = Option.isSome (destI tm)
-
fun stripNeg tm =
case tm of
Fn (f,[a]) =>
@@ -9194,7 +9229,7 @@
let
val s = Metis_Name.toString b
in
- case List.find (fn (n,_,_) => n = s) bracks of
+ case List.find (fn (n,_,_) => n = s) bMap of
NONE => NONE
| SOME (_,b1,b2) => SOME (b1,tm,b2)
end
@@ -9227,11 +9262,11 @@
val bv = Metis_StringSet.addList bv (map Metis_Name.toString (v :: vs))
in
Metis_Print.program
- [Metis_Print.addString q,
+ [Metis_Print.ppString q,
varName bv v,
Metis_Print.program
(map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
- Metis_Print.addString ".",
+ Metis_Print.ppString ".",
Metis_Print.addBreak 1,
innerQuant bv tm]
end
@@ -9245,7 +9280,7 @@
val (n,tm) = stripNeg tm
in
Metis_Print.blockProgram Metis_Print.Inconsistent n
- [Metis_Print.duplicate n (Metis_Print.addString neg),
+ [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
@@ -9271,31 +9306,32 @@
val isAlphaNum =
let
- val alphaNumChars = explode "_'"
+ val alphaNumChars = String.explode "_'"
in
fn c => mem c alphaNumChars orelse Char.isAlphaNum c
end;
local
- val alphaNumToken = atLeastOne (some isAlphaNum) >> implode;
+ val alphaNumToken = atLeastOne (some isAlphaNum) >> String.implode;
val symbolToken =
let
fun isNeg c = str c = !negation
- val symbolChars = explode "<>=-*+/\\?@|!$%&#^:;~"
+ 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)) >> (implode o op::)
+ (some isNonNegSymbol ++ many (some isSymbol)) >>
+ (String.implode o op::)
end;
val punctToken =
let
- val punctChars = explode "()[]{}.,"
+ val punctChars = String.explode "()[]{}.,"
fun isPunct c = mem c punctChars
in
@@ -9327,8 +9363,9 @@
val iTokens = Metis_Print.tokensInfixes iOps
- val iParser =
- parseInfixes iOps (fn (f,a,b) => Fn (Metis_Name.fromString f, [a,b]))
+ fun iMk (f,a,b) = Fn (Metis_Name.fromString f, [a,b])
+
+ val iParser = parseInfixes iOps iMk any
val specialTokens =
Metis_StringSet.addList iTokens (neg :: quants @ ["$"] @ bTokens)
@@ -9367,7 +9404,7 @@
some (Metis_Useful.equal ".")) >>++
(fn (_,(vs,_)) =>
term (Metis_StringSet.addList bv vs) >>
- (fn body => foldr bind body vs))
+ (fn body => List.foldr bind body vs))
end
in
var ||
@@ -9396,7 +9433,7 @@
in
fun fromString input =
let
- val chars = Metis_Stream.fromList (explode input)
+ val chars = Metis_Stream.fromList (String.explode input)
val tokens = everything (lexer >> singleton) chars
@@ -9409,7 +9446,8 @@
end;
local
- val antiquotedTermToString = Metis_Print.toString (Metis_Print.ppBracket "(" ")" pp);
+ val antiquotedTermToString =
+ Metis_Print.toString (Metis_Print.ppBracket "(" ")" pp);
in
val parse = Metis_Parse.parseQuotation antiquotedTermToString fromString;
end;
@@ -9423,11 +9461,11 @@
structure Metis_TermSet = Metis_ElementSet (Metis_TermMap);
-(**** Original file: Subst.sig ****)
+(**** Original file: src/Subst.sig ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Subst =
@@ -9545,11 +9583,11 @@
end
-(**** Original file: Subst.sml ****)
+(**** Original file: src/Subst.sml ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Subst :> Metis_Subst =
@@ -9797,11 +9835,11 @@
end
-(**** Original file: Atom.sig ****)
+(**** Original file: src/Atom.sig ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Atom =
@@ -9941,11 +9979,11 @@
end
-(**** Original file: Atom.sml ****)
+(**** Original file: src/Atom.sml ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Atom :> Metis_Atom =
@@ -9979,14 +10017,14 @@
let
fun f (tm,acc) = Metis_NameAritySet.union (Metis_Term.functions tm) acc
in
- fn atm => foldl f Metis_NameAritySet.empty (arguments atm)
+ 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 => foldl f Metis_NameSet.empty (arguments atm)
+ fn atm => List.foldl f Metis_NameSet.empty (arguments atm)
end;
(* Binary relations *)
@@ -10003,7 +10041,8 @@
(* The size of an atom in symbols. *)
(* ------------------------------------------------------------------------- *)
-fun symbols atm = foldl (fn (tm,z) => Metis_Term.symbols tm + z) 1 (arguments atm);
+fun symbols atm =
+ List.foldl (fn (tm,z) => Metis_Term.symbols tm + z) 1 (arguments atm);
(* ------------------------------------------------------------------------- *)
(* A total comparison function for atoms. *)
@@ -10030,7 +10069,7 @@
let
fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
in
- foldl f [] (enumerate tms)
+ List.foldl f [] (enumerate tms)
end;
fun replace _ ([],_) = raise Bug "Metis_Atom.replace: empty path"
@@ -10065,7 +10104,7 @@
let
fun f (tm,acc) = Metis_NameSet.union (Metis_Term.freeVars tm) acc
in
- fn atm => foldl f Metis_NameSet.empty (arguments atm)
+ fn atm => List.foldl f Metis_NameSet.empty (arguments atm)
end;
(* ------------------------------------------------------------------------- *)
@@ -10091,7 +10130,7 @@
val _ = (Metis_Name.equal p1 p2 andalso length tms1 = length tms2) orelse
raise Error "Metis_Atom.match"
in
- foldl matchArg sub (zip tms1 tms2)
+ List.foldl matchArg sub (zip tms1 tms2)
end;
end;
@@ -10107,7 +10146,7 @@
val _ = (Metis_Name.equal p1 p2 andalso length tms1 = length tms2) orelse
raise Error "Metis_Atom.unify"
in
- foldl unifyArg sub (zip tms1 tms2)
+ List.foldl unifyArg sub (zip tms1 tms2)
end;
end;
@@ -10156,7 +10195,7 @@
(* ------------------------------------------------------------------------- *)
fun typedSymbols ((_,tms) : atom) =
- foldl (fn (tm,z) => Metis_Term.typedSymbols tm + z) 1 tms;
+ List.foldl (fn (tm,z) => Metis_Term.typedSymbols tm + z) 1 tms;
fun nonVarTypedSubterms (_,tms) =
let
@@ -10164,10 +10203,10 @@
let
fun addTm ((path,tm),acc) = (n :: path, tm) :: acc
in
- foldl addTm acc (Metis_Term.nonVarTypedSubterms arg)
- end
- in
- foldl addArg [] (enumerate tms)
+ List.foldl addTm acc (Metis_Term.nonVarTypedSubterms arg)
+ end
+ in
+ List.foldl addArg [] (enumerate tms)
end;
(* ------------------------------------------------------------------------- *)
@@ -10191,11 +10230,11 @@
structure Metis_AtomSet = Metis_ElementSet (Metis_AtomMap);
-(**** Original file: Formula.sig ****)
+(**** Original file: src/Formula.sig ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Formula =
@@ -10391,11 +10430,11 @@
end
-(**** Original file: Formula.sml ****)
+(**** Original file: src/Formula.sml ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Formula :> Metis_Formula =
@@ -10540,7 +10579,7 @@
(* Conjunctions *)
fun listMkConj fms =
- case rev fms of [] => True | fm :: fms => foldl And fm fms;
+ case rev fms of [] => True | fm :: fms => List.foldl And fm fms;
local
fun strip cs (And (p,q)) = strip (p :: cs) q
@@ -10563,7 +10602,7 @@
(* Disjunctions *)
fun listMkDisj fms =
- case rev fms of [] => False | fm :: fms => foldl Or fm fms;
+ case rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
local
fun strip cs (Or (p,q)) = strip (p :: cs) q
@@ -10586,7 +10625,7 @@
(* Equivalences *)
fun listMkEquiv fms =
- case rev fms of [] => True | fm :: fms => foldl Iff fm fms;
+ case rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
local
fun strip cs (Iff (p,q)) = strip (p :: cs) q
@@ -10995,11 +11034,11 @@
structure Metis_FormulaSet = Metis_ElementSet (Metis_FormulaMap);
-(**** Original file: Literal.sig ****)
+(**** Original file: src/Literal.sig ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Literal =
@@ -11163,11 +11202,11 @@
end
-(**** Original file: Literal.sml ****)
+(**** Original file: src/Literal.sml ****)
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Literal :> Metis_Literal =
@@ -11459,7 +11498,7 @@
structure Metis_LiteralSetSet = Metis_ElementSet (Metis_LiteralSetMap);
-(**** Original file: Thm.sig ****)
+(**** Original file: src/Thm.sig ****)
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
@@ -11610,7 +11649,7 @@
end
-(**** Original file: Thm.sml ****)
+(**** Original file: src/Thm.sml ****)
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
@@ -11725,7 +11764,7 @@
in
fun pp th =
Metis_Print.blockProgram Metis_Print.Inconsistent 3
- [Metis_Print.addString "|- ",
+ [Metis_Print.ppString "|- ",
Metis_Formula.pp (toFormula th)];
end;
@@ -11827,11 +11866,11 @@
end
-(**** Original file: Proof.sig ****)
+(**** Original file: src/Proof.sig ****)
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Proof =
@@ -11891,11 +11930,11 @@
end
-(**** Original file: Proof.sml ****)
+(**** Original file: src/Proof.sml ****)
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Proof :> Metis_Proof =
@@ -11934,40 +11973,40 @@
fun ppSubst ppThm (sub,thm) =
Metis_Print.sequence (Metis_Print.addBreak 1)
(Metis_Print.blockProgram Metis_Print.Inconsistent 1
- [Metis_Print.addString "{",
+ [Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Subst.pp ("sub",sub),
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("thm",thm),
- Metis_Print.addString "}"]);
+ Metis_Print.ppString "}"]);
fun ppResolve ppThm (res,pos,neg) =
Metis_Print.sequence (Metis_Print.addBreak 1)
(Metis_Print.blockProgram Metis_Print.Inconsistent 1
- [Metis_Print.addString "{",
+ [Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Atom.pp ("res",res),
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("pos",pos),
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("neg",neg),
- Metis_Print.addString "}"]);
+ Metis_Print.ppString "}"]);
fun ppRefl tm = Metis_Print.sequence (Metis_Print.addBreak 1) (Metis_Term.pp tm);
fun ppEquality (lit,path,res) =
Metis_Print.sequence (Metis_Print.addBreak 1)
(Metis_Print.blockProgram Metis_Print.Inconsistent 1
- [Metis_Print.addString "{",
+ [Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Literal.pp ("lit",lit),
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Term.ppPath ("path",path),
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Term.pp ("res",res),
- Metis_Print.addString "}"]);
+ Metis_Print.ppString "}"]);
fun ppInf ppAxiom ppThm inf =
let
@@ -11975,7 +12014,7 @@
in
Metis_Print.block Metis_Print.Inconsistent 2
(Metis_Print.sequence
- (Metis_Print.addString infString)
+ (Metis_Print.ppString infString)
(case inf of
Axiom cl => ppAxiom cl
| Assume x => ppAssume x
@@ -12001,7 +12040,7 @@
val prf = enumerate prf
fun ppThm th =
- Metis_Print.addString
+ Metis_Print.ppString
let
val cl = Metis_Thm.clause th
@@ -12018,7 +12057,7 @@
in
Metis_Print.sequence
(Metis_Print.blockProgram Metis_Print.Consistent (1 + size s)
- [Metis_Print.addString (s ^ " "),
+ [Metis_Print.ppString (s ^ " "),
Metis_Thm.pp th,
Metis_Print.addBreak 2,
Metis_Print.ppBracket "[" "]" (ppInf (K Metis_Print.skip) ppThm) inf])
@@ -12026,10 +12065,10 @@
end
in
Metis_Print.blockProgram Metis_Print.Consistent 0
- [Metis_Print.addString "START OF PROOF",
+ [Metis_Print.ppString "START OF PROOF",
Metis_Print.addNewline,
Metis_Print.program (map ppStep prf),
- Metis_Print.addString "END OF PROOF"]
+ Metis_Print.ppString "END OF PROOF"]
end
(*MetisDebug
handle Error err => raise Bug ("Metis_Proof.pp: shouldn't fail:\n" ^ err);
@@ -12346,11 +12385,11 @@
end
-(**** Original file: Rule.sig ****)
+(**** Original file: src/Rule.sig ****)
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Rule =
@@ -12623,11 +12662,11 @@
end
-(**** Original file: Rule.sml ****)
+(**** Original file: src/Rule.sml ****)
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Rule :> Metis_Rule =
@@ -12783,17 +12822,19 @@
val noConv : conv = fn _ => raise Error "noConv";
+(*MetisDebug
fun traceConv s conv tm =
let
val res as (tm',th) = conv tm
- val () = print (s ^ ": " ^ Metis_Term.toString tm ^ " --> " ^
+ val () = trace (s ^ ": " ^ Metis_Term.toString tm ^ " --> " ^
Metis_Term.toString tm' ^ " " ^ Metis_Thm.toString th ^ "\n")
in
res
end
handle Error err =>
- (print (s ^ ": " ^ Metis_Term.toString tm ^ " --> Error: " ^ err ^ "\n");
+ (trace (s ^ ": " ^ Metis_Term.toString tm ^ " --> Error: " ^ err ^ "\n");
raise Error (s ^ ": " ^ err));
+*)
fun thenConvTrans tm (tm',th1) (tm'',th2) =
let
@@ -13082,7 +13123,7 @@
val reflTh = Metis_Thm.refl (Metis_Term.Fn (f,xs))
val reflLit = Metis_Thm.destUnit reflTh
in
- fst (foldl cong (reflTh,reflLit) (enumerate ys))
+ fst (List.foldl cong (reflTh,reflLit) (enumerate ys))
end;
(* ------------------------------------------------------------------------- *)
@@ -13109,7 +13150,7 @@
val assumeLit = (false,(R,xs))
val assumeTh = Metis_Thm.assume assumeLit
in
- fst (foldl cong (assumeTh,assumeLit) (enumerate ys))
+ fst (List.foldl cong (assumeTh,assumeLit) (enumerate ys))
end;
(* ------------------------------------------------------------------------- *)
@@ -13409,11 +13450,11 @@
end
-(**** Original file: Normalize.sig ****)
+(**** Original file: src/Normalize.sig ****)
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001-2009 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Normalize =
@@ -13467,11 +13508,11 @@
end
-(**** Original file: Normalize.sml ****)
+(**** Original file: src/Normalize.sml ****)
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Normalize :> Metis_Normalize =
@@ -14159,19 +14200,20 @@
val newSkolemFunction =
let
val counter : int Metis_StringMap.map Unsynchronized.ref = Unsynchronized.ref (Metis_StringMap.new ())
- in
- (* MODIFIED by Jasmin Blanchette *)
- fn n => CRITICAL (fn () =>
- 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)
+
+ 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
+ fn n => Metis_Portable.critical (new n) ()
end;
fun skolemize fv bv fm =
@@ -14286,8 +14328,8 @@
(c2', s2', (c1,s1,fm,c2,s2) :: l)
end
- val (c1,_,fms) = foldl fwd (count0,empty,[]) fms
- val (c2,_,fms) = foldl bwd (count0,empty,[]) fms
+ val (c1,_,fms) = List.foldl fwd (count0,empty,[]) fms
+ val (c2,_,fms) = List.foldl bwd (count0,empty,[]) fms
(*MetisDebug
val _ = countEquivish c1 c2 orelse
@@ -14332,10 +14374,10 @@
let
val fms = sortMap (measure o count) countCompare fms
in
- foldl breakSet1 best (cumulatives fms)
- end
-
- val best = foldl breakSing best (cumulatives fms)
+ 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
@@ -14715,14 +14757,13 @@
let
val counter : int Unsynchronized.ref = Unsynchronized.ref 0
in
- (* MODIFIED by Jasmin Blanchette *)
- fn () => CRITICAL (fn () =>
+ fn () => Metis_Portable.critical (fn () =>
let
val Unsynchronized.ref i = counter
val () = counter := i + 1
in
definitionPrefix ^ "_" ^ Int.toString i
- end)
+ end) ()
end;
fun newDefinition def =
@@ -14858,7 +14899,7 @@
end
-(**** Original file: Model.sig ****)
+(**** Original file: src/Model.sig ****)
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
@@ -15138,7 +15179,7 @@
end
-(**** Original file: Model.sml ****)
+(**** Original file: src/Model.sml ****)
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
@@ -15414,10 +15455,10 @@
fun ppEntry (tag,source_arity,target) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString tag,
+ [Metis_Print.ppString tag,
Metis_Print.addBreak 1,
Metis_NameArity.pp source_arity,
- Metis_Print.addString " ->",
+ Metis_Print.ppString " ->",
Metis_Print.addBreak 1,
Metis_Name.pp target];
in
@@ -16332,7 +16373,7 @@
let
fun add (y,acc) = FunctionPerturbation (func_xs,y) :: acc
in
- foldl add acc target
+ List.foldl add acc target
end
in
pertTerms M onTarget tms xs acc
@@ -16413,17 +16454,17 @@
fun pp M =
Metis_Print.program
- [Metis_Print.addString "Metis_Model{",
+ [Metis_Print.ppString "Metis_Model{",
Metis_Print.ppInt (size M),
- Metis_Print.addString "}"];
-
-end
-
-(**** Original file: Problem.sig ****)
+ Metis_Print.ppString "}"];
+
+end
+
+(**** Original file: src/Problem.sig ****)
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Problem =
@@ -16485,11 +16526,11 @@
end
-(**** Original file: Problem.sml ****)
+(**** Original file: src/Problem.sml ****)
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Problem :> Metis_Problem =
@@ -16518,9 +16559,9 @@
val cls = toClauses prob
in
{clauses = length cls,
- literals = foldl lits 0 cls,
- symbols = foldl syms 0 cls,
- typedSymbols = foldl typedSyms 0 cls}
+ literals = List.foldl lits 0 cls,
+ symbols = List.foldl syms 0 cls,
+ typedSymbols = List.foldl typedSyms 0 cls}
end;
fun freeVars {axioms,conjecture} =
@@ -16648,11 +16689,11 @@
end
-(**** Original file: TermNet.sig ****)
+(**** Original file: src/TermNet.sig ****)
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_TermNet =
@@ -16701,11 +16742,11 @@
end
-(**** Original file: TermNet.sml ****)
+(**** Original file: src/TermNet.sml ****)
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_TermNet :> Metis_TermNet =
@@ -16863,7 +16904,7 @@
fun null net = size net = 0;
-fun singles qtms a = foldr Single a qtms;
+fun singles qtms a = List.foldr Single a qtms;
local
fun pre NONE = (0,NONE)
@@ -16893,7 +16934,7 @@
handle Error _ => raise Bug "Metis_TermNet.insert: should never fail";
end;
-fun fromList parm l = foldl (fn (tm_a,n) => insert n tm_a) (new parm) l;
+fun fromList parm l = List.foldl (fn (tm_a,n) => insert n tm_a) (new parm) l;
fun filter pred =
let
@@ -17146,7 +17187,7 @@
local
fun inc (qtm, Result l, acc) =
- foldl (fn ((n,a),acc) => (n,(qtm,a)) :: acc) acc l
+ List.foldl (fn ((n,a),acc) => (n,(qtm,a)) :: acc) acc l
| inc _ = raise Bug "Metis_TermNet.pp.inc";
fun toList (Net (_,_,NONE)) = []
@@ -17159,11 +17200,11 @@
end
-(**** Original file: AtomNet.sig ****)
+(**** Original file: src/AtomNet.sig ****)
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_AtomNet =
@@ -17210,11 +17251,11 @@
end
-(**** Original file: AtomNet.sml ****)
+(**** Original file: src/AtomNet.sml ****)
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_AtomNet :> Metis_AtomNet =
@@ -17249,7 +17290,7 @@
fun insert net (atm,a) = Metis_TermNet.insert net (atomToTerm atm, a);
-fun fromList parm l = foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
+fun fromList parm l = List.foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
val filter = Metis_TermNet.filter;
@@ -17272,11 +17313,11 @@
end
-(**** Original file: LiteralNet.sig ****)
+(**** Original file: src/LiteralNet.sig ****)
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_LiteralNet =
@@ -17325,11 +17366,11 @@
end
-(**** Original file: LiteralNet.sml ****)
+(**** Original file: src/LiteralNet.sml ****)
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_LiteralNet :> Metis_LiteralNet =
@@ -17368,7 +17409,7 @@
| insert {positive,negative} ((false,atm),a) =
{positive = positive, negative = Metis_AtomNet.insert negative (atm,a)};
-fun fromList parm l = foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
+fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
fun filter pred {positive,negative} =
{positive = Metis_AtomNet.filter pred positive,
@@ -17402,11 +17443,11 @@
end
-(**** Original file: Subsume.sig ****)
+(**** Original file: src/Subsume.sig ****)
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Subsume =
@@ -17456,11 +17497,11 @@
end
-(**** Original file: Subsume.sml ****)
+(**** Original file: src/Subsume.sml ****)
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Subsume :> Metis_Subsume =
@@ -17793,11 +17834,11 @@
end
-(**** Original file: KnuthBendixOrder.sig ****)
+(**** Original file: src/KnuthBendixOrder.sig ****)
(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_KnuthBendixOrder =
@@ -17818,11 +17859,11 @@
end
-(**** Original file: KnuthBendixOrder.sml ****)
+(**** Original file: src/KnuthBendixOrder.sml ****)
(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_KnuthBendixOrder :> Metis_KnuthBendixOrder =
@@ -17921,7 +17962,7 @@
val ppWeightList =
let
fun ppCoeff n =
- if n < 0 then Metis_Print.sequence (Metis_Print.addString "~") (ppCoeff (~n))
+ if n < 0 then Metis_Print.sequence (Metis_Print.ppString "~") (ppCoeff (~n))
else if n = 1 then Metis_Print.skip
else Metis_Print.ppInt n
@@ -18020,11 +18061,11 @@
end
-(**** Original file: Rewrite.sig ****)
+(**** Original file: src/Rewrite.sig ****)
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Rewrite =
@@ -18122,11 +18163,11 @@
end
-(**** Original file: Rewrite.sml ****)
+(**** Original file: src/Rewrite.sml ****)
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Rewrite :> Metis_Rewrite =
@@ -18333,7 +18374,7 @@
rw
end;
-val addList = foldl (fn (eqn,rw) => add rw eqn);
+val addList = List.foldl (fn (eqn,rw) => add rw eqn);
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
@@ -18394,7 +18435,7 @@
val th = Metis_Rule.symmetryRule l r
in
fn tm =>
- if Metis_Term.equal tm r then (l,th) else raise Error "mkNeqConv: Metis_RL"
+ if Metis_Term.equal tm r then (l,th) else raise Error "mkNeqConv: RL"
end
| SOME EQUAL => raise Error "irreflexive"
| SOME GREATER =>
@@ -18560,8 +18601,9 @@
let
fun addSubterm b ((path,tm),net) = Metis_TermNet.insert net (tm,(id,b,path))
- val subterms = foldl (addSubterm true) subterms (Metis_Term.subterms l)
- val subterms = foldl (addSubterm false) subterms (Metis_Term.subterms r)
+ val subterms = List.foldl (addSubterm true) subterms (Metis_Term.subterms l)
+
+ val subterms = List.foldl (addSubterm false) subterms (Metis_Term.subterms r)
in
subterms
end;
@@ -18786,7 +18828,7 @@
in
fun orderedRewrite order ths =
let
- val rw = foldl addEqn (new order) (enumerate ths)
+ val rw = List.foldl addEqn (new order) (enumerate ths)
in
rewriteRule rw order
end;
@@ -18796,11 +18838,11 @@
end
-(**** Original file: Units.sig ****)
+(**** Original file: src/Units.sig ****)
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Units =
@@ -18848,11 +18890,11 @@
end
-(**** Original file: Units.sml ****)
+(**** Original file: src/Units.sml ****)
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Units :> Metis_Units =
@@ -18899,7 +18941,7 @@
end
end;
-val addList = foldl (fn (th,u) => add u th);
+val addList = List.foldl (fn (th,u) => add u th);
(* ------------------------------------------------------------------------- *)
(* Matching. *)
@@ -18957,11 +18999,11 @@
end
-(**** Original file: Clause.sig ****)
+(**** Original file: src/Clause.sig ****)
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Clause =
@@ -19067,11 +19109,11 @@
end
-(**** Original file: Clause.sml ****)
+(**** Original file: src/Clause.sml ****)
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002-2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Clause :> Metis_Clause =
@@ -19086,10 +19128,17 @@
val newId =
let
val r = Unsynchronized.ref 0
- in
- (* MODIFIED by Jasmin Blanchette *)
- fn () => CRITICAL (fn () =>
- case r of Unsynchronized.ref n => let val () = r := n + 1 in n end)
+
+ fun new () =
+ let
+ val Unsynchronized.ref n = r
+
+ val () = r := n + 1
+ in
+ n
+ end
+ in
+ fn () => Metis_Portable.critical new ()
end;
(* ------------------------------------------------------------------------- *)
@@ -19133,7 +19182,7 @@
val default : parameters =
{ordering = Metis_KnuthBendixOrder.default,
- orderLiterals = UnsignedLiteralOrder (* PositiveLiteralOrder *) (* MODIFIED by Jasmin Blanchette *),
+ orderLiterals = UnsignedLiteralOrder,
orderTerms = true};
fun mk info = Metis_Clause info
@@ -19252,7 +19301,7 @@
let
fun addTm ((path,tm),acc) = (lit,path,tm) :: acc
in
- foldl addTm acc (Metis_Literal.nonVarTypedSubterms lit)
+ List.foldl addTm acc (Metis_Literal.nonVarTypedSubterms lit)
end;
in
fun largestSubterms cl = Metis_LiteralSet.foldl addLit [] (largestLiterals cl);
@@ -19432,11 +19481,11 @@
end
-(**** Original file: Active.sig ****)
+(**** Original file: src/Active.sig ****)
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Active =
@@ -19490,11 +19539,11 @@
end
-(**** Original file: Active.sml ****)
+(**** Original file: src/Active.sml ****)
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Active :> Metis_Active =
@@ -19519,7 +19568,7 @@
| NONE => rw
end
in
- foldl add (Metis_Rewrite.new (Metis_KnuthBendixOrder.compare ordering))
+ List.foldl add (Metis_Rewrite.new (Metis_KnuthBendixOrder.compare ordering))
end;
fun allFactors red =
@@ -19787,8 +19836,8 @@
end
val cls = clauses active
- val (cls,_) = foldl remove ([], Metis_Subsume.new ()) cls
- val (cls,subs) = foldl remove ([], Metis_Subsume.new ()) cls
+ val (cls,_) = List.foldl remove ([], Metis_Subsume.new ()) cls
+ val (cls,subs) = List.foldl remove ([], Metis_Subsume.new ()) cls
(*MetisDebug
val Metis_Active {parameters,...} = active
@@ -19815,7 +19864,7 @@
local
fun ppField f ppA a =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString (f ^ " ="),
+ [Metis_Print.ppString (f ^ " ="),
Metis_Print.addBreak 1,
ppA a];
@@ -19836,21 +19885,21 @@
in
fun pp (Metis_Active {clauses,rewrite,subterms,...}) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString "Metis_Active",
+ [Metis_Print.ppString "Metis_Active",
Metis_Print.addBreak 1,
Metis_Print.blockProgram Metis_Print.Inconsistent 1
- [Metis_Print.addString "{",
+ [Metis_Print.ppString "{",
ppClauses clauses,
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppRewrite rewrite,
(*MetisTrace5
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppSubterms subterms,
*)
Metis_Print.skip],
- Metis_Print.addString "}"];
+ Metis_Print.ppString "}"];
end;
*)
@@ -19968,7 +20017,7 @@
fun add ((lit,ort,tm),equations) =
Metis_TermNet.insert equations (tm,(cl,lit,ort,tm))
in
- foldl add equations (Metis_Clause.largestEquations cl)
+ List.foldl add equations (Metis_Clause.largestEquations cl)
end;
fun addSubterms subterms cl =
@@ -19976,7 +20025,7 @@
fun add ((lit,path,tm),subterms) =
Metis_TermNet.insert subterms (tm,(cl,lit,path,tm))
in
- foldl add subterms (Metis_Clause.largestSubterms cl)
+ List.foldl add subterms (Metis_Clause.largestSubterms cl)
end;
fun addAllSubterms allSubterms cl =
@@ -19984,7 +20033,7 @@
fun add ((_,_,tm),allSubterms) =
Metis_TermNet.insert allSubterms (tm,(cl,tm))
in
- foldl add allSubterms (Metis_Clause.allSubterms cl)
+ List.foldl add allSubterms (Metis_Clause.allSubterms cl)
end;
fun addClause active cl =
@@ -20035,7 +20084,8 @@
*)
in
if Metis_Atom.isEq atm then acc
- else foldl resolve acc (Metis_LiteralNet.unify literals (Metis_Literal.negate lit))
+ else
+ List.foldl resolve acc (Metis_LiteralNet.unify literals (Metis_Literal.negate lit))
end;
fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =
@@ -20045,7 +20095,7 @@
SOME cl' => cl' :: acc
| NONE => acc
in
- foldl para acc (Metis_TermNet.unify subterms tm)
+ List.foldl para acc (Metis_TermNet.unify subterms tm)
end;
fun deduceParamodulationInto equations cl ((lit,path,tm),acc) =
@@ -20055,7 +20105,7 @@
SOME cl' => cl' :: acc
| NONE => acc
in
- foldl para acc (Metis_TermNet.unify equations tm)
+ List.foldl para acc (Metis_TermNet.unify equations tm)
end;
fun deduce active cl =
@@ -20081,8 +20131,8 @@
val acc = []
val acc = Metis_LiteralSet.foldl (deduceResolution literals cl) acc lits
- val acc = foldl (deduceParamodulationWith subterms cl) acc eqns
- val acc = foldl (deduceParamodulationInto equations cl) acc subtms
+ val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
+ val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
val acc = rev acc
(*MetisTrace5
@@ -20328,7 +20378,7 @@
let
val cls = sort_utilitywise (cl :: Metis_Clause.factor cl)
in
- foldl factor_add active_subsume_acc cls
+ List.foldl factor_add active_subsume_acc cls
end;
fun factor' active acc [] = (active, rev acc)
@@ -20336,7 +20386,7 @@
let
val cls = sort_utilitywise cls
val subsume = getSubsume active
- val (active,_,acc) = foldl factor1 (active,subsume,acc) cls
+ val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
val (active,cls) = extract_rewritables active
in
factor' active acc cls
@@ -20404,11 +20454,11 @@
end
-(**** Original file: Waiting.sig ****)
+(**** Original file: src/Waiting.sig ****)
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Waiting =
@@ -20484,11 +20534,11 @@
end
-(**** Original file: Waiting.sml ****)
+(**** Original file: src/Waiting.sml ****)
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Waiting :> Metis_Waiting =
@@ -20528,17 +20578,16 @@
(* ------------------------------------------------------------------------- *)
val defaultModels : modelParameters list =
- [(* MODIFIED by Jasmin Blanchette
- {model = Metis_Model.default,
+ [{model = Metis_Model.default,
initialPerturbations = 100,
maxChecks = SOME 20,
perturbations = 0,
- weight = 1.0} *)];
+ weight = 1.0}];
val default : parameters =
{symbolsWeight = 1.0,
- literalsWeight = (* 1.0 *) 0.0, (* MODIFIED by Jasmin Blanchette *)
- variablesWeight = (* 1.0 *) 0.0, (* MODIFIED by Jasmin Blanchette *)
+ literalsWeight = 1.0,
+ variablesWeight = 1.0,
models = defaultModels};
fun size (Metis_Waiting {clauses,...}) = Metis_Heap.size clauses;
@@ -20651,7 +20700,7 @@
val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight)
val variablesW = Math.pow (clauseVariables lits, variablesWeight)
val literalsW = Math.pow (clauseLiterals lits, literalsWeight)
- val modelsW = (* checkModels models mods mcl *) 1.0 (* MODIFIED by Jasmin Blanchette *)
+ val modelsW = checkModels models mods mcl
(*MetisTrace4
val () = trace ("Metis_Waiting.clauseWeight: dist = " ^
Real.toString dist ^ "\n")
@@ -20758,11 +20807,11 @@
end
-(**** Original file: Resolution.sig ****)
+(**** Original file: src/Resolution.sig ****)
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Resolution =
@@ -20812,11 +20861,11 @@
end
-(**** Original file: Resolution.sml ****)
+(**** Original file: src/Resolution.sml ****)
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Resolution :> Metis_Resolution =