extra/boolean-expr/boolean-expr.factor

   1 ! Copyright (C) 2008 Slava Pestov.
   2 ! See http://factorcode.org/license.txt for BSD license.
   3 USING: accessors arrays classes kernel sequences sets
   4 io prettyprint multi-methods ;
   5 IN: boolean-expr
   6
   7 ! Demonstrates the use of Unicode symbols in source files, and
   8 ! multi-method dispatch.
   9
  10 TUPLE: ⋀ x y ;
  11 TUPLE: ⋁ x y ;
  12 TUPLE: ¬ x ;
  13
  14 SINGLETONS: ⊤ ⊥ ;
  15
  16 SINGLETONS: P Q R S T U V W X Y Z ;
  17
  18 UNION: □ ⋀ ⋁ ¬ ⊤ ⊥ P Q R S T U V W X Y Z ;
  19
  20 GENERIC: ⋀ ( x y -- expr )
  21
  22 METHOD: ⋀ { ⊤ □ } nip ;
  23 METHOD: ⋀ { □ ⊤ } drop ;
  24 METHOD: ⋀ { ⊥ □ } drop ;
  25 METHOD: ⋀ { □ ⊥ } nip ;
  26
  27 METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
  28 METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
  29
  30 METHOD: ⋀ { □ □ } \ ⋀ boa ;
  31
  32 GENERIC: ⋁ ( x y -- expr )
  33
  34 METHOD: ⋁ { ⊤ □ } drop ;
  35 METHOD: ⋁ { □ ⊤ } nip ;
  36 METHOD: ⋁ { ⊥ □ } nip ;
  37 METHOD: ⋁ { □ ⊥ } drop ;
  38
  39 METHOD: ⋁ { □ □ } \ ⋁ boa ;
  40
  41 GENERIC: ¬ ( x -- expr )
  42
  43 METHOD: ¬ { ⊤ } drop ⊥ ;
  44 METHOD: ¬ { ⊥ } drop ⊤ ;
  45
  46 METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
  47 METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
  48
  49 METHOD: ¬ { □ } \ ¬ boa ;
  50
  51 : → ( x y -- expr ) ¬ ⋀ ;
  52 : ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
  53 : ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
  54
  55 GENERIC: (cnf) ( expr -- cnf )
  56
  57 METHOD: (cnf) { ⋀ } [ x>> (cnf) ] [ y>> (cnf) ] bi append ;
  58 METHOD: (cnf) { □ } 1array ;
  59
  60 GENERIC: cnf ( expr -- cnf )
  61
  62 METHOD: cnf { ⋁ } [ x>> cnf ] [ y>> cnf ] bi append ;
  63 METHOD: cnf { □ } (cnf) 1array ;
  64
  65 GENERIC: satisfiable? ( expr -- ? )
  66
  67 METHOD: satisfiable? { ⊤ } drop t ;
  68 METHOD: satisfiable? { ⊥ } drop f ;
  69
  70 : partition ( seq quot -- left right )
  71     [ [ not ] compose filter ] [ filter ] 2bi ; inline
  72
  73 : (satisfiable?) ( seq -- ? )
  74     [ \ ¬ instance? ] partition [ x>> ] map intersect empty? ;
  75
  76 METHOD: satisfiable? { □ }
  77     cnf [ (satisfiable?) ] contains? ;
  78
  79 GENERIC: (expr.) ( expr -- )
  80
  81 METHOD: (expr.) { □ } pprint ;
  82
  83 : op. ( expr -- )
  84     "(" write
  85     [ x>> (expr.) ]
  86     [ bl class pprint bl ]
  87     [ y>> (expr.) ]
  88     tri
  89     ")" write ;
  90
  91 METHOD: (expr.) { ⋀ } op. ;
  92 METHOD: (expr.) { ⋁ } op. ;
  93 METHOD: (expr.) { ¬ } [ class pprint ] [ x>> (expr.) ] bi ;
  94
  95 : expr. ( expr -- ) (expr.) nl ;