Permalink
Browse files

Graphs appear to be implemented, complete with equivalence classes an…

…d filtering of always true/always false props. Not fully tested
  • Loading branch information...
1 parent d52e399 commit 9e9b46b88c765b5917ca109f4020edc1c6fe31fe @jwelch01 committed Dec 8, 2011
View
@@ -1,6 +1,6 @@
structure Basis : sig
val buildGraph : string -> string -> unit
- (* read outcomes & write dot to file "out" *)
+ val buildPropGraph : string -> string -> unit
end =
struct
@@ -85,93 +85,20 @@ fun makeTestSet db =
end)
G.empty sl
- type proposition = (bool * string * string * string * (string * bool) list)
-
- exception AlreadyNegative
-
- fun insertion_sort _ [] = []
- | insertion_sort cmp (x::xs) = insert cmp x (insertion_sort cmp xs)
-and insert _ x [] = [x]
- | insert cmp x (l as y::ys) =
- case cmp (x, y) of GREATER => y :: insert cmp x ys
- | _ => x :: l
-
- fun cmpPropName ((name, _), (name2,_)) = String.compare (name, name2)
-
- val propSort : (string * bool) list -> (string * bool) list =
- insertion_sort cmpPropName
-
- fun propExists prop = foldr (fn ((_,out), flag) => out orelse flag) false prop
-
- fun negateProposition (false, _, _, _, _) = raise AlreadyNegative
- | negateProposition (_, test, num, out, l) =
- let fun neg ((soln, result)::xs) negs = neg xs ((soln, not result)::negs)
- | neg [] negs = negs
- in (false, test, num, out, neg l [])
- end
-
-
- fun makePositivePropositionList testSetList =
- foldr (fn (testList, props) =>
- (Outcome.boolTests (testRep testList)) @ props)
- [] testSetList
-
- fun makePropositionList testSetList =
- foldr (fn (prop, props) =>
- (prop::(negateProposition prop)::props))
- [] (makePositivePropositionList testSetList)
+ infixr 0 $
+ fun f $ x = f x
- fun makePropMapAndSet propList =
- let val (s, m, _) =
- foldr (fn ((b, test, num, out, props), (s, m, c)) =>
- let val name = if b then test ^ " " ^ num ^ " " ^ out
- else test ^ " " ^ num ^ " not " ^ out
- val node = "N" ^ Int.toString(c)
- in (((name,props)::s),
- Map.bind (explode node, name, m),
- c+1)
- end)
- ([], Map.empty, 1) propList
- in (s, m) end
-
- val /->/ : (string * bool) list * (string * bool) list -> bool =
- fn (prop1, prop2) =>
- if (propExists prop1) then
- ListPair.foldr (fn ((_, out1), (_, out2), flag) =>
- if out1 then out2 andalso flag
- else flag)
- true (propSort prop1, propSort prop2)
- else false
-
- infixr 0 /->/
-
- fun filt (node, (soln, p)::props) =
- if p then not (foldr (fn ((_, out), flag) => out andalso flag)
- true props)
- else not (foldr (fn ((_, out), flag) => (not out) andalso flag)
- true props)
- | filt (_, []) = raise Impossible
-
- val filterProps : (string * (string * bool) list) list ->
- (string * (string * bool) list) list
- = List.filter filt
-
-
- fun makePropositionGraph propList =
- foldr (fn ((node, props), impls) =>
- let val impls_ = G.addNode (node, impls)
- in foldr (fn ((node2, props2), impls2) =>
- if props /->/ props2
- then G.addEdge (edge node "" node2, impls2)
- else impls2)
- impls_ propList
- end)
- G.empty propList
-
+ val partitionProps = Prop.partition Prop.eq
+ fun buildPropGraph infile outfile =
+ let val (s, m) = Prop.makePropMapAndSet $
+ partitionProps $ Prop.makePropList $
+ partitionTests $ makeTestSet $
+ FileReader.readToMap $ TextIO.openIn infile
+ val g = Prop.makePropGraph s
+ in FileWriter.printGraph g m (TextIO.openOut outfile)
+ end
- infixr 0 $
- fun f $ x = f x
fun buildGraph infile outfile =
let val (s, m) = buildMapAndSet $ partitionSolns $ makeSolnSet $
@@ -1,14 +1,3 @@
-
-
-fun insertion_sort _ [] = []
- | insertion_sort cmp (x::xs) = insert cmp x (insertion_sort cmp xs)
-and insert _ x [] = [x]
- | insert cmp x (l as y::ys) =
- case cmp (x, y) of GREATER => y :: insert cmp x ys
- | _ => x :: l
-
-
-
(* Turn map into a TestSet *)
fun makeTestSet db =
DB.foldLists (fn (test, testno, rList, set) =>
@@ -83,101 +72,24 @@ fun makeTestSet db =
in foldr (fn (y, g) =>
let val (id2, _) = solnRep y
in if x /<=/ y andalso not (y /<=/ x)
- then G.addEdge (edge id2 "" id1, g)
+ then G.addEdge (edge id1 "" id2, g)
else g
end)
(G.addNode(G.makeNode id1, graph)) sl
end)
G.empty sl
- type proposition = (bool * string * string * string * (string * bool) list)
-
- exception AlreadyNegative
-
- fun negateProposition (false, _, _, _, _) = raise AlreadyNegative
- | negateProposition (_, test, num, out, l) =
- let fun neg ((soln, result)::xs) negs = neg xs ((soln, not result)::negs)
- | neg [] negs = negs
- in (false, test, num, out, neg l [])
- end
-
-
- fun makePositivePropositionList testSetList =
- foldr (fn (testList, props) =>
- (Outcome.boolTests (testRep testList)) @ props)
- [] testSetList
-
- fun makePropositionList testSetList =
- foldr (fn (prop, props) =>
- (prop::(negateProposition prop)::props))
- [] (makePositivePropositionList testSetList)
-
- fun makePropMapAndSet propList =
- let val (s, m, _) =
- foldr (fn ((b, test, num, out, props), (s, m, c)) =>
- let val name = if b then test ^ " " ^ num ^ " " ^ out
- else test ^ " " ^ num ^ " not " ^ out
- val node = "N" ^ Int.toString(c)
- in (((node,props)::s),
- Map.bind (explode node, name, m),
- c+1)
- end)
- ([], Map.empty, 1) propList
- in (s, m) end
-
-
- fun cmpPropName ((name, _), (name2,_)) = String.compare (name, name2)
-
- val propSort : (string * bool) list -> (string * bool) list =
- insertion_sort cmpPropName
-
- fun propExists prop = foldr (fn ((_,out), flag) => out orelse flag) false prop
-
- val /->/ : (string * bool) list * (string * bool) list -> bool =
- fn (prop1, prop2) =>
- if (propExists prop1) then
- ListPair.foldr (fn ((_, out1), (_, out2), flag) =>
- if out1 then out2 andalso flag
- else flag)
- true (propSort prop1, propSort prop2)
- else false
-
- infixr 0 /->/
-
- fun filt (node, (soln, p)::props) =
- if p then not (foldr (fn ((_, out), flag) => out andalso flag)
- true props)
- else not (foldr (fn ((_, out), flag) => (not out) andalso flag)
- true props)
- | filt (_, []) = raise Impossible
-
-
- val filterProps : (string * (string * bool) list) list ->
- (string * (string * bool) list) list
- = List.filter filt
-
-
- fun makePropositionGraph propList =
- foldr (fn ((node, props), impls) =>
- let val impls_ = G.addNode (node, impls)
- in foldr (fn ((node2, props2), impls2) =>
- if props /->/ props2
- then G.addEdge (edge node2 "" node, impls2)
- else impls2)
- impls_ (filterProps propList)
- end)
- G.empty (filterProps propList)
-
-
-
infixr 0 $
fun f $ x = f x
+ val partitionProps = Prop.partition Prop.eq
+
fun buildPropGraph infile outfile =
- let val (s, m) = makePropMapAndSet $ makePropositionList $
+ let val (s, m) = Prop.makePropMapAndSet $
+ partitionProps $ Prop.makePropList $
partitionTests $ makeTestSet $
FileReader.readToMap $ TextIO.openIn infile
- val g = makePropositionGraph s
+ val g = Prop.makePropGraph s
in FileWriter.printGraph g m (TextIO.openOut outfile)
end
@@ -20,6 +20,9 @@ group is $/basis.cm
testset.sml
solnset.sml
+ propositionsig.sml
+ proposition.sml
+
ternarykeychar.sml
ternarystringmap.sml
listmap.sml
@@ -0,0 +1,120 @@
+structure Prop :> PROPOSITION = struct
+ type prop = (bool * string * string * string * (string * bool) list)
+ type simpProp = (string * (string * bool) list)
+
+ exception AlreadyNegative
+ exception Impossible
+
+
+ fun insertion_sort _ [] = []
+ | insertion_sort cmp (x::xs) = insert cmp x (insertion_sort cmp xs)
+and insert _ x [] = [x]
+ | insert cmp x (l as y::ys) =
+ case cmp (x, y) of GREATER => y :: insert cmp x ys
+ | _ => x :: l
+
+ fun cmpPropName ((name, _), (name2,_)) = String.compare (name, name2)
+
+ val propSort : (string * bool) list -> (string * bool) list =
+ insertion_sort cmpPropName
+
+ fun propExists (_,_,_,_, prop) =
+ foldr (fn ((_,out), flag) => out orelse flag) false prop
+ fun testRep s = case TestSet.representative s
+ of SOME y => y
+ | NONE => raise Impossible
+
+ fun negateProposition (false, _, _, _, _) = raise AlreadyNegative
+ | negateProposition (_, test, num, out, l) =
+ let fun neg ((soln, result)::xs) negs = neg xs ((soln, not result)::negs)
+ | neg [] negs = negs
+ in (false, test, num, out, neg l [])
+ end
+
+
+ fun makePositivePropositionList testSetList =
+ foldr (fn (testList, props) =>
+ (Outcome.boolTests (testRep testList)) @ props)
+ [] testSetList
+
+ fun filt (_,_,_,_, (soln, p)::props) =
+ if p then not (foldr (fn ((_, out), flag) => out andalso flag)
+ true props)
+ else not (foldr (fn ((_, out), flag) => (not out) andalso flag)
+ true props)
+ | filt (_,_,_,_, []) = raise Impossible
+
+
+ fun makePropList testSetList = List.filter filt (
+ foldr (fn (prop, props) =>
+ (prop::(negateProposition prop)::props))
+ [] (makePositivePropositionList testSetList))
+
+ fun condenseNames [] = raise Impossible
+ | condenseNames ((b, test, num, out, props)::xs) =
+ let val name = if b then test ^ " " ^ num ^ " " ^ out
+ else test ^ " " ^ num ^ " not " ^ out
+ in (name ^ (foldr (fn ((b, test, num, out, props), n) =>
+ if b then "\\n" ^ test ^ " " ^ num ^ " " ^ out ^ n
+ else "\\n" ^test ^ " " ^ num ^ " not " ^ out ^ n)
+ "" xs), props)
+ end
+
+ fun makePropMapAndSet propList =
+ let val (s, m, _) =
+ foldr (fn (pList, (s, m, c)) =>
+ let val (name, props) = condenseNames pList
+ val node = "N" ^ Int.toString(c)
+ in (((node,props)::s),
+ Map.bind (explode node, name, m),
+ c+1)
+ end)
+ ([], Map.empty, 1) propList
+ in (s, m) end
+
+
+ fun /->/ ((_,prop1), (_,prop2)) =
+ ListPair.foldr (fn ((_, out1), (_, out2), flag) =>
+ if out1 then out2 andalso flag
+ else flag)
+ true (propSort prop1, propSort prop2)
+
+ infixr 0 /->/
+
+ fun eq ((_, _, _, _, prop1), (_, _, _ ,_, prop2)) =
+ ListPair.foldr (fn ((_, out1), (_, out2), flag) =>
+ out1 = out2 andalso flag)
+ true (propSort prop1, propSort prop2)
+
+ fun representative [] = NONE
+ | representative (x::_) = SOME x
+ fun rep x = case representative x of SOME y => y
+ | NONE => raise Impossible
+
+ fun edge id1 label id2 = G.makeEdge (G.makeNode id1, label, G.makeNode id2)
+
+ fun partition f s =
+ let fun partitionOne x l =
+ let fun findEqClass [] = [[x]]
+ | findEqClass (y::ys) = if f (x, (rep y))
+ then (x::y)::ys
+ else y::(findEqClass ys)
+ in findEqClass l
+ end
+ in foldr (fn (elem, classes) => partitionOne elem classes) [] s
+ end
+
+
+ fun makePropGraph propList =
+ foldr (fn ((node, props), impls) =>
+ let val impls_ = G.addNode (node, impls)
+ in foldr (fn ((node2, props2), impls2) =>
+ if (node, props) /->/ (node, props2)
+ then G.addEdge (edge node "" node2, impls2)
+ else impls2)
+ impls_ propList
+ end)
+ G.empty propList
+
+
+end
@@ -0,0 +1,11 @@
+signature PROPOSITION = sig
+ type prop = (bool * string * string * string * (string * bool) list)
+ type simpProp = (string * (string * bool) list)
+
+ val /->/ : simpProp * simpProp -> bool
+ val partition : (prop * prop -> bool) -> prop list -> prop list list
+ val makePropList : TestSet.set list -> prop list
+ val makePropMapAndSet : prop list list -> simpProp list * string Map.map
+ val makePropGraph : simpProp list -> BasicGraph.graph
+ val eq : prop * prop -> bool
+end

0 comments on commit 9e9b46b

Please sign in to comment.