Skip to content

Commit

Permalink
Reimplemented fresh-name generation for pretty-printing.
Browse files Browse the repository at this point in the history 
Using red-black trees code from Twelf.
  • Loading branch information
@jsacchini
jsacchini committed Jul 13, 2012
1 parent c5b6d9b commit cf5f67a
Show file tree
Hide file tree
Showing 6 changed files with 318 additions and 8 deletions.
27 changes: 20 additions & 7 deletions PrettyPrint.sml
View file
Expand Up @@ -24,6 +24,7 @@ struct
open Syntax

structure RAList = RandomAccessList
structure ST = StringRedBlackTree

val printImpl = ref false
val printLVarCtx = ref 0
Expand All @@ -39,14 +40,26 @@ fun paren false x = x
fun lookup ctx n = RAList.lookup ctx (n-1)
handle RAList.Subscript => Int.toString (n - RAList.length ctx)

(* indexTable keeps track of the largest index used to build a variable name *)
(* indexTable(X) = k means that "X{k+1}" should be a fresh name *)
val indexTable : int ST.Table = ST.new 0

(* add : string -> string RAList.ralist -> (string, string RAList.ralist *)
(* add x ctx = (x', ctx') iff
- x' = x ^ <number> or x' = X ^ <number> when x = ""
- x' is fresh in ctx
- ctx' is obtained by adding x to ctx
*)
fun add x ctx =
let fun eq (x : string) y = x=y
fun add1 n x =
let val tryname = x ^ Int.toString n
in if RAList.exists (eq tryname) ctx then add1 (n+1) x
else (tryname, RAList.cons tryname ctx) end
fun add' x = if RAList.exists (eq x) ctx then add1 1 (x^"_") else (x, RAList.cons x ctx)
in if x="" then add1 1 "X" else add' x end
let
fun fresh x = x ^ Int.toString (case ST.lookup indexTable x of
NONE => (ST.insert indexTable (x, 1); 1)
| SOME n => (ST.insert indexTable (x, n+1); n+1))
fun tryAdd x = if RAList.exists (fn y => x=y) ctx then fresh (x^"_") else x
val varName = if x="" then fresh "X" else tryAdd x
in
(varName, RAList.cons varName ctx)
end

fun addNoOccur ctx = RAList.cons "? Error ?" ctx

Expand Down
254 changes: 254 additions & 0 deletions RedBlackTree.fun
View file
@@ -0,0 +1,254 @@
(* From Twelf *)
(* Red/Black Trees *)
(* Author: Frank Pfenning *)

functor RedBlackTree
(type key'
val compare : key' * key' -> order)
:> TABLE where type key = key' =
struct
type key = key'
type 'a entry = key * 'a

datatype 'a dict =
Empty (* considered black *)
| Red of 'a entry * 'a dict * 'a dict
| Black of 'a entry * 'a dict * 'a dict

type 'a Table = 'a dict ref

(* Representation Invariants *)
(*
1. The tree is ordered: for every node Red((key1,datum1), left, right) or
Black ((key1,datum1), left, right), every key in left is less than
key1 and every key in right is greater than key1.
2. The children of a red node are black (color invariant).
3. Every path from the root to a leaf has the same number of
black nodes, called the black height of the tree.
*)

local

fun lookup dict key =
let
fun lk (Empty) = NONE
| lk (Red tree) = lk' tree
| lk (Black tree) = lk' tree
and lk' ((key1, datum1), left, right) =
(case compare(key,key1)
of EQUAL => SOME(datum1)
| LESS => lk left
| GREATER => lk right)
in
lk dict
end

(* val restore_right : 'a dict -> 'a dict *)
(*
restore_right (Black(e,l,r)) >=> dict
where (1) Black(e,l,r) is ordered,
(2) Black(e,l,r) has black height n,
(3) color invariant may be violated at the root of r:
one of its children might be red.
and dict is a re-balanced red/black tree (satisfying all invariants)
and same black height n.
*)
fun restore_right (Black(e, Red lt, Red (rt as (_,Red _,_)))) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_right (Black(e, Red lt, Red (rt as (_,_,Red _)))) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_right (Black(e, l, Red(re, Red(rle, rll, rlr), rr))) =
(* l is black, deep rotate *)
Black(rle, Red(e, l, rll), Red(re, rlr, rr))
| restore_right (Black(e, l, Red(re, rl, rr as Red _))) =
(* l is black, shallow rotate *)
Black(re, Red(e, l, rl), rr)
| restore_right dict = dict

(* restore_left is like restore_right, except *)
(* the color invariant may be violated only at the root of left child *)
fun restore_left (Black(e, Red (lt as (_,Red _,_)), Red rt)) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_left (Black(e, Red (lt as (_,_,Red _)), Red rt)) =
Red(e, Black lt, Black rt) (* re-color *)
| restore_left (Black(e, Red(le, ll as Red _, lr), r)) =
(* r is black, shallow rotate *)
Black(le, ll, Red(e, lr, r))
| restore_left (Black(e, Red(le, ll, Red(lre, lrl, lrr)), r)) =
(* r is black, deep rotate *)
Black(lre, Red(le, ll, lrl), Red(e, lrr, r))
| restore_left dict = dict

fun insert (dict, entry as (key,datum)) =
let
(* val ins : 'a dict -> 'a dict inserts entry *)
(* ins (Red _) may violate color invariant at root *)
(* ins (Black _) or ins (Empty) will be red/black tree *)
(* ins preserves black height *)
fun ins (Empty) = Red(entry, Empty, Empty)
| ins (Red(entry1 as (key1, datum1), left, right)) =
(case compare(key,key1)
of EQUAL => Red(entry, left, right)
| LESS => Red(entry1, ins left, right)
| GREATER => Red(entry1, left, ins right))
| ins (Black(entry1 as (key1, datum1), left, right)) =
(case compare(key,key1)
of EQUAL => Black(entry, left, right)
| LESS => restore_left (Black(entry1, ins left, right))
| GREATER => restore_right (Black(entry1, left, ins right)))
in
case ins dict
of Red (t as (_, Red _, _)) => Black t (* re-color *)
| Red (t as (_, _, Red _)) => Black t (* re-color *)
| dict => dict
end

(* function below from .../smlnj-lib/Util/int-redblack-set.sml *)
(* Need to check and improve some time *)
(* Sun Mar 13 08:22:53 2005 -fp *)

(* Remove an item. Returns true if old item found, false otherwise *)
local
exception NotFound
datatype 'a zipper
= TOP
| LEFTB of ('a entry * 'a dict * 'a zipper)
| LEFTR of ('a entry * 'a dict * 'a zipper)
| RIGHTB of ('a dict * 'a entry * 'a zipper)
| RIGHTR of ('a dict * 'a entry * 'a zipper)
in
fun delete t key =
let
fun zip (TOP, t) = t
| zip (LEFTB(x, b, z), a) = zip(z, Black(x, a, b))
| zip (LEFTR(x, b, z), a) = zip(z, Red(x, a, b))
| zip (RIGHTB(a, x, z), b) = zip(z, Black(x, a, b))
| zip (RIGHTR(a, x, z), b) = zip(z, Red(x, a, b))
(* bbZip propagates a black deficit up the tree until either the top
* is reached, or the deficit can be covered. It returns a boolean
* that is true if there is still a deficit and the zipped tree.
*)
fun bbZip (TOP, t) = (true, t)
| bbZip (LEFTB(x, Red(y, c, d), z), a) = (* case 1L *)
bbZip (LEFTR(x, c, LEFTB(y, d, z)), a)
| bbZip (LEFTB(x, Black(w, Red(y, c, d), e), z), a) = (* case 3L *)
bbZip (LEFTB(x, Black(y, c, Red(w, d, e)), z), a)
| bbZip (LEFTR(x, Black(w, Red(y, c, d), e), z), a) = (* case 3L *)
bbZip (LEFTR(x, Black(y, c, Red(w, d, e)), z), a)
| bbZip (LEFTB(x, Black(y, c, Red(w, d, e)), z), a) = (* case 4L *)
(false, zip (z, Black(y, Black(x, a, c), Black(w, d, e))))
| bbZip (LEFTR(x, Black(y, c, Red(w, d, e)), z), a) = (* case 4L *)
(false, zip (z, Red(y, Black(x, a, c), Black(w, d, e))))
| bbZip (LEFTR(x, Black(y, c, d), z), a) = (* case 2L *)
(false, zip (z, Black(x, a, Red(y, c, d))))
| bbZip (LEFTB(x, Black(y, c, d), z), a) = (* case 2L *)
bbZip (z, Black(x, a, Red(y, c, d)))
| bbZip (RIGHTB(Red(y, c, d), x, z), b) = (* case 1R *)
bbZip (RIGHTR(d, x, RIGHTB(c, y, z)), b)
| bbZip (RIGHTR(Red(y, c, d), x, z), b) = (* case 1R *)
bbZip (RIGHTR(d, x, RIGHTB(c, y, z)), b)
| bbZip (RIGHTB(Black(y, Red(w, c, d), e), x, z), b) = (* case 3R *)
bbZip (RIGHTB(Black(w, c, Red(y, d, e)), x, z), b)
| bbZip (RIGHTR(Black(y, Red(w, c, d), e), x, z), b) = (* case 3R *)
bbZip (RIGHTR(Black(w, c, Red(y, d, e)), x, z), b)
| bbZip (RIGHTB(Black(y, c, Red(w, d, e)), x, z), b) = (* case 4R *)
(false, zip (z, Black(y, c, Black(x, Red(w, d, e), b))))
| bbZip (RIGHTR(Black(y, c, Red(w, d, e)), x, z), b) = (* case 4R *)
(false, zip (z, Red(y, c, Black(w, Red(w, d, e), b))))
| bbZip (RIGHTR(Black(y, c, d), x, z), b) = (* case 2R *)
(false, zip (z, Black(x, Red(y, c, d), b)))
| bbZip (RIGHTB(Black(y, c, d), x, z), b) = (* case 2R *)
bbZip (z, Black(x, Red(y, c, d), b))
| bbZip (z, t) = (false, zip(z, t))
fun delMin (Red(y, Empty, b), z) = (y, (false, zip(z, b)))
| delMin (Black(y, Empty, b), z) = (y, bbZip(z, b))
| delMin (Black(y, a, b), z) = delMin(a, LEFTB(y, b, z))
| delMin (Red(y, a, b), z) = delMin(a, LEFTR(y, b, z))
| delMin (Empty, _) = raise Match
fun joinRed (Empty, Empty, z) = zip(z, Empty)
| joinRed (a, b, z) = let
val (x, (needB, b')) = delMin(b, TOP)
in
if needB
then #2(bbZip(z, Red(x, a, b')))
else zip(z, Red(x, a, b'))
end
fun joinBlack (a, Empty, z) = #2(bbZip(z, a))
| joinBlack (Empty, b, z) = #2(bbZip(z, b))
| joinBlack (a, b, z) = let
val (x, (needB, b')) = delMin(b, TOP)
in
if needB
then #2(bbZip(z, Black(x, a, b')))
else zip(z, Black(x, a, b'))
end
fun del (Empty, z) = raise NotFound
| del (Black(entry1 as (key1, datum1), a, b), z) =
(case compare(key,key1)
of EQUAL => joinBlack (a, b, z)
| LESS => del (a, LEFTB(entry1, b, z))
| GREATER => del (b, RIGHTB(a, entry1, z)))
| del (Red(entry1 as (key1, datum1), a, b), z) =
(case compare(key,key1)
of EQUAL => joinRed (a, b, z)
| LESS => del (a, LEFTR(entry1, b, z))
| GREATER => del (b, RIGHTR(a, entry1, z)))
in
(del(t, TOP); true) handle NotFound => false
end
end (* local *)

(* use non-imperative version? *)
fun insertShadow (dict, entry as (key,datum)) =
let val oldEntry = ref NONE (* : 'a entry option ref *)
fun ins (Empty) = Red(entry, Empty, Empty)
| ins (Red(entry1 as (key1, datum1), left, right)) =
(case compare(key,key1)
of EQUAL => (oldEntry := SOME(entry1);
Red(entry, left, right))
| LESS => Red(entry1, ins left, right)
| GREATER => Red(entry1, left, ins right))
| ins (Black(entry1 as (key1, datum1), left, right)) =
(case compare(key,key1)
of EQUAL => (oldEntry := SOME(entry1);
Black(entry, left, right))
| LESS => restore_left (Black(entry1, ins left, right))
| GREATER => restore_right (Black(entry1, left, ins right)))
in
(oldEntry := NONE;
((case ins dict
of Red (t as (_, Red _, _)) => Black t (* re-color *)
| Red (t as (_, _, Red _)) => Black t (* re-color *)
| dict => dict),
!oldEntry))
end

fun app f dict =
let fun ap (Empty) = ()
| ap (Red tree) = ap' tree
| ap (Black tree) = ap' tree
and ap' (entry1, left, right) =
(ap left; f entry1; ap right)
in
ap dict
end

in
fun new (n) = ref (Empty) (* ignore size hint *)
val insert = (fn table => fn entry => (table := insert (!table, entry)))
val insertShadow =
(fn table => fn entry =>
let
val (dict, oldEntry) = insertShadow (!table, entry)
in
(table := dict; oldEntry)
end)
val lookup = (fn table => fn key => lookup (!table) key)
val delete = (fn table => fn key => (delete (!table) key; ()))
val clear = (fn table => (table := Empty))
val app = (fn f => fn table => app f (!table))
end

end; (* functor RedBlackTree *)
27 changes: 27 additions & 0 deletions Table.sig
View file
@@ -0,0 +1,27 @@
(* From Twelf *)
(* Hash Tables *)
(* Author: Frank Pfenning *)
(* Modified: Roberto Virga *)

(* This provides a common interface to hash tables *)
(* red/black trees and similar data structures *)

signature TABLE =
sig
type key (* parameter *)
type 'a entry = key * 'a

type 'a Table
val new : int -> 'a Table (* size hint for some implementations *)

val insert : 'a Table -> 'a entry -> unit
(* insert entry, return shadowed entry if there is one *)
val insertShadow : 'a Table -> 'a entry -> ('a entry) option
val lookup : 'a Table -> key -> 'a option
val delete : 'a Table -> key -> unit
val clear : 'a Table -> unit

(* Apply function to all entries in unpredictable order *)
val app : ('a entry -> unit) -> 'a Table -> unit

end; (* signature TABLE *)
10 changes: 10 additions & 0 deletions Table.sml
View file
@@ -0,0 +1,10 @@
(* From Twelf *)

structure StringRedBlackTree =
RedBlackTree (type key' = string
val compare = String.compare)

structure IntRedBlackTree =
RedBlackTree (type key' = int
val compare = Int.compare)

3 changes: 3 additions & 0 deletions celf.mlb
View file
Expand Up @@ -28,6 +28,9 @@ celf.lex.sml
celf.grm.sml
RemDepend.sig
RemDepend.sml
Table.sig
RedBlackTree.fun
Table.sml
PrettyPrint.sig
PrettyPrint.sml
PatternBind.sig
Expand Down
5 changes: 4 additions & 1 deletion sources.cm
View file
Expand Up @@ -29,6 +29,9 @@ celf.lex
celf.grm
RemDepend.sig
RemDepend.sml
Table.sig
RedBlackTree.fun
Table.sml
PrettyPrint.sig
PrettyPrint.sml
PatternBind.sig
Expand All @@ -52,7 +55,7 @@ TypeCheck.sml
Rnd.sig
Rnd-smlnj-mlton.sml
PermuteList.sig
NoPermuteList.sml
PermuteList.sml
SignaturTable.sig
SignaturTable.sml
OpSem.sig
Expand Down

0 comments on commit cf5f67a

Please sign in to comment.