aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/disjoint.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-08 13:15:00 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-08 13:15:00 -0500
commit901b6d55e625be136ddd677a3d8a36e5068de2ae (patch)
treee8e154d621a2dcea385de57280730d135b25466e /src/disjoint.sml
parent91ac4dd03f4130e5e416d495d53237b74a37efc1 (diff)
Some small changes while failing to write [restrict]
Diffstat (limited to 'src/disjoint.sml')
-rw-r--r--src/disjoint.sml8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 808d8413..c6a8d50f 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -53,6 +53,8 @@ fun p2s p =
fun pp p = print (p2s p ^ "\n")
+fun rp2s (p, ns) = String.concatWith " " (p2s p :: map Int.toString ns)
+
structure PK = struct
type ord_key = piece
@@ -104,6 +106,12 @@ structure PM = BinaryMapFn(PK)
type env = PS.set PM.map
+fun p_env x =
+ (print "\nDENV:\n";
+ PM.appi (fn (p1, ps) =>
+ PS.app (fn p2 =>
+ print (rp2s p1 ^ " ~ " ^ rp2s p2 ^ "\n")) ps) x)
+
structure E = ElabEnv
type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con