diff options
Diffstat (limited to 'src/interp/simpbool.boot')
| -rw-r--r-- | src/interp/simpbool.boot | 205 |
1 files changed, 205 insertions, 0 deletions
diff --git a/src/interp/simpbool.boot b/src/interp/simpbool.boot new file mode 100644 index 00000000..d79829c2 --- /dev/null +++ b/src/interp/simpbool.boot @@ -0,0 +1,205 @@ +-- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. +-- All rights reserved. +-- Copyright (C) 2007, Gabriel Dos Reis. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- - Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- +-- - Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in +-- the documentation and/or other materials provided with the +-- distribution. +-- +-- - Neither the name of The Numerical ALgorithms Group Ltd. nor the +-- names of its contributors may be used to endorse or promote products +-- derived from this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +-- TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +-- PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +-- OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + +)package "BOOT" + +simpBool x == dnf2pf reduceDnf be x + +reduceDnf u == +-- (OR (AND ..b..) b) ==> (OR b ) + atom u => u + for x in u repeat + ok := true + for y in u repeat + x = y => 'skip + dnfContains(x,y) => return (ok := false) + ok = true => acc := [x,:acc] + nreverse acc + +dnfContains([a,b],[c,d]) == fn(a,c) and fn(b,d) where + fn(x,y) == and/[member(u,x) for u in y] + +prove x == + world := [p for y in listOfUserIds x | (p := getPredicate y)] => + 'false = be mkpf([['NOT,x],:world],'AND) => true + 'false = be mkpf([x,:world],'AND) => false + x + 'false = (y := be x) => 'false + y = 'true => true + dnf2pf y + +simpBoolGiven(x,world) == + world => + 'false = be mkpf([['NOT,x],:world],'AND) => true + 'false = (y := be mkpf([x,:world],'AND)) => false + (u := andReduce(dnf2pf y,world)) is ['AND,:v] and + (w := SETDIFFERENCE(v,world)) ^= v => simpBool ['AND,:w] + u + 'false = (y := be x) => false + 'true = y => true + dnf2pf y + +andReduce(x,y) == + x is ['AND,:r] => + y is ['AND,:s] => mkpf(S_-(r,s),'AND) + mkpf(S_-(r,[s]),'AND) + x +dnf2pf(x) == + x = 'true => 'T + x = 'false => nil + atom x => x + mkpf( + [mkpf([:[k for k in b],:[['not,k] for k in a]],'AND) for [a,b] in x],'OR) +be x == b2dnf x +b2dnf x == + x = 'T => 'true + x = NIL => 'false + atom x => bassert x + [op,:argl] := x + MEMQ(op,'(AND and)) => band argl + MEMQ(op,'(OR or)) => bor argl + MEMQ(op,'(NOT not)) => bnot first argl + bassert x +band x == + x is [h,:t] => andDnf(b2dnf h,band t) + 'true +bor x == + x is [a,:b] => orDnf(b2dnf a,bor b) + 'false +bnot x == notDnf b2dnf x +bassert x == [[nil,[x]]] +bassertNot x == [[[x],nil]] +------------------------Disjunctive Normal Form Code----------------------- +-- dnf is true | false | [coaf ... ] +-- coaf is true | false | [item ... ] +-- item is anything + +orDnf(a,b) == -- or: (dnf, dnf) -> dnf + a = 'false => b + b = 'false => a + a = 'true or b = 'true => 'true + null a => b --null list means false + a is [c] = coafOrDnf(c,b) + coafOrDnf(first a,orDnf(rest a,b)) + +andDnf(a,b) == -- and: (dnf, dnf) -> dnf + a = 'true => b + b = 'true => a + a = 'false or b = 'false => 'false + null a => 'false --null list means false + a is [c] => coafAndDnf(c,b) + x := coafAndDnf(first a,b) + y := andDnf(rest a,b) + x = 'false => y + y = 'false => x + ordUnion(x,y) + +notDnf l == -- not: dnf -> dnf + l = 'true => 'false + l = 'false => 'true + null l => 'true --null list means false + l is [x] => notCoaf x + andDnf(notCoaf first l,notDnf rest l) + +coafOrDnf(a,l) == -- or: (coaf, dnf) -> dnf + a = 'true or l = 'true => 'true + a = 'false => l + member(a,l) => l + y := notCoaf a + x := ordIntersection(y,l) + null x => orDel(a,l) + x = l => 'true + x = y => ordSetDiff(l,x) + ordUnion(notDnf ordSetDiff(y,x),l) + +coafAndDnf(a,b) == --and: (coaf, dnf) -> dnf + a = 'true => b + a = 'false => 'false + [c,:r] := b + null r => coafAndCoaf(a,c) + x := coafAndCoaf(a,c) --dnf + y := coafAndDnf(a,r) --dnf + x = 'false => y + y = 'false => x + ordUnion(x,y) + +coafAndCoaf([a,b],[p,q]) == --and: (coaf,coaf) -> dnf + ordIntersection(a,q) or ordIntersection(b,p) => 'false + [[ordUnion(a,p),ordUnion(b,q)]] + +notCoaf [a,b] == [:[[nil,[x]] for x in a],:[[[x],nil] for x in b]] + +list1 l == + l isnt [h,:t] => nil + null h => list1 t + [[h,nil,nil],:list1 t] +list2 l == + l isnt [h,:t] => nil + null h => list2 t + [[nil,h,nil],:list2 t] +list3 l == + l isnt [h,:t] => nil + null h => list3 t + [[nil,nil,h],:list3 t] +orDel(a,l) == + l is [h,:t] => + a = h => t + ?ORDER(a,h) => [a,:l] + [h,:orDel(a,t)] + [a] +ordList l == + l is [h,:t] and t => orDel(h,ordList t) + l +ordUnion(a,b) == + a isnt [c,:r] => b + b isnt [d,:s] => a + c=d => [c,:ordUnion(r,s)] + ?ORDER(a,b) => [c,:ordUnion(r,b)] + [d,:ordUnion(s,a)] +ordIntersection(a,b) == + a isnt [h,:t] => nil + member(h,b) => [h,:ordIntersection(t,b)] + ordIntersection(t,b) +ordSetDiff(a,b) == + b isnt [h,:t] => a + member(h,a) => ordSetDiff(delete(h,a),t) + ordSetDiff(a,t) +------------- +testPredList u == + for x in u repeat + y := simpBool x + x = y => nil + pp x + pp '"==========>" + pp y |