extra/boolean-expr/boolean-expr-docs.factor

   1 ! Copyright (C) 2018 Alexander Ilin.
   2 ! See http://factorcode.org/license.txt for BSD license.
   3 USING: arrays help.markup help.syntax kernel ;
   4 IN: boolean-expr
   5
   6 ABOUT: "boolean-expr"
   7
   8 ARTICLE: "boolean-expr" "Boolean expressions"
   9 "The " { $vocab-link "boolean-expr" } " vocab demonstrates the use of Unicode symbols in source files and multi-method dispatch."
  10 ;
  11
  12 HELP: dnf
  13 { $values
  14     { "expr" □ }
  15     { "dnf" array }
  16 }
  17 { $description "Convert the " { $snippet "expr" } " to Disjunctive Normal Form (DNF), i.e. an array of subexpressions, each not containing disjunctions. See " { $url "https://en.wikipedia.org/wiki/Disjunctive_normal_form" } "." }
  18 { $examples
  19     { $example "USING: boolean-expr prettyprint ;"
  20         "X Y Z ⋀ ⋀ dnf ."
  21         "{ { X Y Z } }"
  22     }
  23     { $example "USING: boolean-expr prettyprint ;"
  24         "X Y Z ⋁ ⋁ dnf ."
  25         "{ { X } { Y } { Z } }"
  26     }
  27 } ;
  28
  29 HELP: expr.
  30 { $values
  31     { "expr" □ }
  32 }
  33 { $description "Print the expression followed by newline." }
  34 { $examples
  35     { $example "USING: boolean-expr ;"
  36         "X Y ⋁ X ¬ Y ⋀ ⋀ op."
  37         "((X ⋀ (¬X ⋀ Y)) ⋁ (Y ⋀ (¬X ⋀ Y)))"
  38     }
  39 } ;
  40
  41 HELP: op.
  42 { $values
  43     { "expr" □ }
  44 }
  45 { $description "Print the expression." }
  46 { $examples
  47     { $example "USING: boolean-expr ;"
  48         "X Y ⋁ X ¬ Y ⋀ ⋀ op."
  49         "((X ⋀ (¬X ⋀ Y)) ⋁ (Y ⋀ (¬X ⋀ Y)))"
  50     }
  51 } ;
  52
  53 { expr. op. } related-words
  54
  55 HELP: satisfiable?
  56 { $values
  57     { "expr" □ }
  58     { "?" boolean }
  59 }
  60 { $description "Return " { $link t } " if the " { $snippet "expr" } " can be true." }
  61 { $examples
  62     { $example "USING: boolean-expr prettyprint ;"
  63         "⊤ satisfiable? ."
  64         "t"
  65     }
  66     { $example "USING: boolean-expr prettyprint ;"
  67         "⊥ satisfiable? ."
  68         "f"
  69     }
  70     { $example "USING: boolean-expr prettyprint ;"
  71         "X X ¬ ⋀ satisfiable? ."
  72         "f"
  73     }
  74     { $example "USING: boolean-expr prettyprint ;"
  75         "X Y ⋁ X ¬ Y ¬ ⋀ ⋀ satisfiable? ."
  76         "f"
  77     }
  78     { $example "USING: boolean-expr prettyprint ;"
  79         "X Y ⋁ X ¬ Y ⋀ ⋀ satisfiable? ."
  80         "t"
  81     }
  82 } ;
  83
  84 HELP: ¬
  85 { $class-description "Logical negation (NOT)." $nl
  86     { $snippet "¬(¬A) " { $link ≣ } " A" } "."
  87 } ;
  88
  89 HELP: →
  90 { $values
  91     { "x" □ } { "y" □ }
  92     { "expr" □ }
  93 }
  94 { $description "Material implication (if..then)." $nl
  95     { $snippet "x→y" } " " { $link ≣ } " " { $link ¬ } "x" { $link ⋁ } "y"
  96 } ;
  97
  98 HELP: ≣
  99 { $values
 100     { "x" □ } { "y" □ }
 101     { "expr" □ }
 102 }
 103 { $description "Material equivalence (if and only if)." $nl
 104     { $snippet "(x≣y) ≣ ((x" } { $link ⋀ } { $snippet "y) " }
 105     { $link ⋁ } { $snippet " (" } { $link ¬ } { $snippet "x" } { $link ⋀ } { $link ¬ } { $snippet "y))" }
 106 } ;
 107
 108 HELP: ⊕
 109 { $values
 110     { "x" □ } { "y" □ }
 111     { "expr" □ }
 112 }
 113 { $description "Exclusive disjunction (XOR)." } ;
 114
 115 HELP: ⊤
 116 { $class-description "Logical tautology. This statement is unconditionally true." } ;
 117
 118 HELP: ⊥
 119 { $class-description "Logical contradiction. This statement is unconditionally false." } ;
 120
 121 HELP: ⋀
 122 { $class-description "Logical conjunction (AND)." } ;
 123
 124 HELP: ⋁
 125 { $class-description "Logical disjunction (OR)." } ;
 126
 127 HELP: □
 128 { $class-description "A union class of all classes defined in this vocab. In methods signatures it stands for \"any variable or expression\"." } ;