remove pamphlets - part 7

1 files changed, 203 insertions, 0 deletions

diff --git a/src/interp/simpbool.boot b/src/interp/simpbool.boot
new file mode 100644
index 00000000..12455d20
--- /dev/null
+++ b/src/interp/simpbool.boot
@@ -0,0 +1,203 @@
+-- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
+-- 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