From c09077789df5e36aee23729fe8298e6e4f353cd2 Mon Sep 17 00:00:00 2001 From: Connor Burns Date: Thu, 6 Jan 2022 15:32:04 -0700 Subject: [PATCH 1/6] Docstrings for `LogicalSymbol` --- src/expression.jl | 64 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 63 insertions(+), 1 deletion(-) diff --git a/src/expression.jl b/src/expression.jl index 92639bd..e7b2d25 100644 --- a/src/expression.jl +++ b/src/expression.jl @@ -1,22 +1,72 @@ export ¬, ∧, ∨, →, ⟷ -export LogicalSymbol, istree, isnode, metadata, variables, operation, operations, arguments, parents, left, right, isassociative, iscommutative +export LogicalSymbol, istree, isnode, name, metadata, variables, operation, operations, arguments, parents, left, right, isassociative, iscommutative export isunary, isbinary export @symbols abstract type AbstractExpression end +""" + LogicalSymbol(name::Symbol, metadata::Any) + +Creates a symbol with attached metadata. +""" struct LogicalSymbol <: AbstractExpression name::Symbol metadata::Any end +""" + LogicalSymbol(name::Symbol) + +Represent a logical symbolically with a provided name. +""" LogicalSymbol(name::Symbol) = LogicalSymbol(name, nothing) +""" + istree(expr::T) where {T <: AbstractExpression} + +Returns true when `expr` is a `LogicalExpression` and false otherwise. +""" istree(::LogicalSymbol) = false +""" + isnode(expr::T) where {T <: AbstractExpression} + +Returns true when `expr` is a `LogicalSymbol` and false otherwise. +""" isnode(::LogicalSymbol) = true +""" + name(sym::LogicalSymbol) + +The name of the symbol provided at instantiation. Equivalent to `symbol(sym)`. +""" name(sym::LogicalSymbol) = sym.name +""" + metadata(sym::LogicalSymbol) + +The metadata of the symbol provided at instantiation, if any. Returns `nothing` if none was provided. +""" metadata(sym::LogicalSymbol) = sym.metadata +""" + variables(expr::T) where {T <: AbstractExpression} + +Returns variables present in an entire expression tree. When the first argument is a `LogicalSymbol`, this is singleton +set containing only the provided `LogicalSymbol`. When the argument is a `LogicalExpression`, this is a set containing the union +of all the variables present in each argument. +""" variables(sym::LogicalSymbol) = Set{LogicalSymbol}(LogicalSymbol[sym]) +""" + operations(expr::T) where {T <: AbstractExpression} + +Returns the operations present in an entire expression tree. When given a `LogicalSymbol`, this is an empty set, whereas +when given a `LogicalExpression`, this is a set containing the expression's own `LogicalOperation` and the operations set +of each of its arguments. +""" operations(::LogicalSymbol) = Set{LogicalOperation}([]) +""" + arguments(expr::T) where {T <: AbstractExpression} + +Returns the arguments which an `AbstractExpression` contains. `LogicalSymbols` contain no arguments and `LogicalExpressions` +can contain any number of arguments. +""" arguments(::LogicalSymbol) = AbstractExpression[] Base.show(io::IO, sym::LogicalSymbol) = print(io, string(sym.name)) Base.hash(sym::LogicalSymbol, h::UInt) = hash(sym.name, hash(sym.metadata, h)) @@ -28,6 +78,18 @@ Base.copy(sym::LogicalSymbol) = sym Base.deepcopy(sym::LogicalSymbol) = LogicalSymbol(name(sym), deepcopy(metadata(sym))) # convenience macros +""" +Define any number of `LogicalSymbols` with the names provided. + +# Examples +```julia-repl +julia> @symbols a # defines symbol `a` in the current scope + +julia> @symbols b c d # defines symbols `a`, `b`, and `c` + +julia> @symbols α β γ # defines symbols `α`, `β`, and `γ` +``` +""" macro symbols(syms...) definitions = [:( $(esc(sym)) = LogicalSymbol($(esc(Symbol))($(string(sym)))) From 21dbc6a2560327ebc3b1831d3e5399a8efaee92c Mon Sep 17 00:00:00 2001 From: Connor Burns Date: Thu, 6 Jan 2022 15:55:13 -0700 Subject: [PATCH 2/6] LogicalOperation docs and reformat standard AbstractExpression methods --- src/expression.jl | 171 ++++++++++++++++++++++++++++------------------ 1 file changed, 106 insertions(+), 65 deletions(-) diff --git a/src/expression.jl b/src/expression.jl index e7b2d25..8aaca27 100644 --- a/src/expression.jl +++ b/src/expression.jl @@ -1,38 +1,21 @@ export ¬, ∧, ∨, →, ⟷ export LogicalSymbol, istree, isnode, name, metadata, variables, operation, operations, arguments, parents, left, right, isassociative, iscommutative -export isunary, isbinary +export isunary, isbinary, argument_count export @symbols abstract type AbstractExpression end """ - LogicalSymbol(name::Symbol, metadata::Any) + LogicalSymbol(name::Symbol, metadata::Any=nothing) -Creates a symbol with attached metadata. +Represent a logical symbolically with a provided name. By default the attached metadata is set to `nothing`. """ struct LogicalSymbol <: AbstractExpression name::Symbol metadata::Any end -""" - LogicalSymbol(name::Symbol) - -Represent a logical symbolically with a provided name. -""" LogicalSymbol(name::Symbol) = LogicalSymbol(name, nothing) -""" - istree(expr::T) where {T <: AbstractExpression} - -Returns true when `expr` is a `LogicalExpression` and false otherwise. -""" -istree(::LogicalSymbol) = false -""" - isnode(expr::T) where {T <: AbstractExpression} - -Returns true when `expr` is a `LogicalSymbol` and false otherwise. -""" -isnode(::LogicalSymbol) = true """ name(sym::LogicalSymbol) @@ -45,29 +28,7 @@ name(sym::LogicalSymbol) = sym.name The metadata of the symbol provided at instantiation, if any. Returns `nothing` if none was provided. """ metadata(sym::LogicalSymbol) = sym.metadata -""" - variables(expr::T) where {T <: AbstractExpression} -Returns variables present in an entire expression tree. When the first argument is a `LogicalSymbol`, this is singleton -set containing only the provided `LogicalSymbol`. When the argument is a `LogicalExpression`, this is a set containing the union -of all the variables present in each argument. -""" -variables(sym::LogicalSymbol) = Set{LogicalSymbol}(LogicalSymbol[sym]) -""" - operations(expr::T) where {T <: AbstractExpression} - -Returns the operations present in an entire expression tree. When given a `LogicalSymbol`, this is an empty set, whereas -when given a `LogicalExpression`, this is a set containing the expression's own `LogicalOperation` and the operations set -of each of its arguments. -""" -operations(::LogicalSymbol) = Set{LogicalOperation}([]) -""" - arguments(expr::T) where {T <: AbstractExpression} - -Returns the arguments which an `AbstractExpression` contains. `LogicalSymbols` contain no arguments and `LogicalExpressions` -can contain any number of arguments. -""" -arguments(::LogicalSymbol) = AbstractExpression[] Base.show(io::IO, sym::LogicalSymbol) = print(io, string(sym.name)) Base.hash(sym::LogicalSymbol, h::UInt) = hash(sym.name, hash(sym.metadata, h)) Base.:(==)(sym1::LogicalSymbol, sym2::LogicalSymbol) = sym1.name == sym2.name && isequal(metadata(sym1), metadata(sym2)) @@ -101,6 +62,12 @@ macro symbols(syms...) end +""" + LogicalOperation(bool_fn::Function, name::Symbol, argument_count::Int, associative::Bool, commutative::Bool) + +Defines a logical operator which can be used to form expressions with. Usually you don't need to define your own +operators, just use the ones built-in to the package if possible. +""" struct LogicalOperation bool_fn::Function name::Symbol @@ -108,10 +75,35 @@ struct LogicalOperation associative::Bool commutative::Bool end +""" + argument_count(op::LogicalOperation) + +The number of arguments which the given operation expects to receive. +""" argument_count(op::LogicalOperation) = op.argument_count +""" + isunary(op::LogicalOperation) + +True if the given operation only receives one argument, false otherwise. +""" isunary(op::LogicalOperation) = argument_count(op) == 1 +""" + isbinary(op::LogicalOperation) + +True if the given operation receives two arguments, false otherwise. +""" isbinary(op::LogicalOperation) = argument_count(op) == 2 +""" + isassociative(op::LogicalOperation) + +True if the given operation is associative, false otherwise. +""" isassociative(op::LogicalOperation) = op.associative +""" + iscommutative(op::LogicalOperation) + +True if the given operation is commutative, false otherwise. +""" iscommutative(op::LogicalOperation) = op.commutative Base.show(io::IO, op::LogicalOperation) = print(io, string(op.name)) Base.hash(op::LogicalOperation, h::UInt) = hash(op.name, hash(argument_count(op), hash(op.associative, hash(op.commutative, h)))) @@ -119,6 +111,13 @@ function Base.:(==)(op1::LogicalOperation, op2::LogicalOperation) op1.name == op2.name && argument_count(op1) == argument_count(op2) && isassociative(op1) == isassociative(op2) && iscommutative(op1) == iscommutative(op2) end +""" + (op::LogicalOperation)(args::AbstractExpression...) + +This function is the foundation of expression building, as it allows instances of `LogicalOperations` to be treated as real +Julia functions. When called this function returns a `LogicalExpression` representing the application of the given operator +on the provided arguments. +""" function (op::LogicalOperation)(args::AbstractExpression...) if length(args) != argument_count(op) throw(ErrorException("Invalid argument count $(length(args)). Expected $(argument_count(op)) arguments.")) @@ -131,6 +130,12 @@ end recursivevariables(args::Vector{AbstractExpression}) = reduce(∪, variables.(args)) recursiveoperations(args::Vector{AbstractExpression}, rootop::LogicalOperation) = reduce(∪, operations.(args)) ∪ Set([rootop]) +""" + LogicalExpression(arguments::Vector{AbstractExpression}, operation::LogicalOperation) + +Constructs an expression with given arguments and logical operation. Please refrain from using this syntax, instead using +the "operators as functions" syntax, where a `LogicalOperation` instance can be called to produce a `LogicalExpression`. +""" mutable struct LogicalExpression <: AbstractExpression arguments::Vector{AbstractExpression} operation::LogicalOperation @@ -148,10 +153,7 @@ mutable struct LogicalExpression <: AbstractExpression expr end end -istree(::LogicalExpression) = true -isnode(::LogicalExpression) = false operation(expr::LogicalExpression) = getfield(expr, :operation) -arguments(expr::LogicalExpression) = getfield(expr, :arguments) parents(expr::LogicalExpression) = getfield(expr, :parents) add_to_parents!(expr::LogicalExpression) = add_to_parents!(expr, arguments(expr)) function add_to_parents!(expr::LogicalExpression, relevant_args::Vector{AbstractExpression}) @@ -170,20 +172,6 @@ function remove_from_parents!(expr::LogicalExpression, relevant_args::Vector{Abs end end metadata(::LogicalExpression) = nothing -function variables(expr::LogicalExpression) - if !getfield(expr, :cached_variables_valid) - setfield!(expr, :cached_variables, recursivevariables(arguments(expr))) - expr.cached_variables_valid = true - end - getfield(expr, :cached_variables) -end -function operations(expr::LogicalExpression) - if !getfield(expr, :cached_operations_valid) - setfield!(expr, :cached_operations, recursiveoperations(arguments(expr), operation(expr))) - expr.cached_operations_valid = true - end - getfield(expr, :cached_operations) -end left(expr::LogicalExpression) = isbinary(operation(expr)) ? arguments(expr)[1] : throw(ErrorException("Operation $(operation(expr)) is not binary")) right(expr::LogicalExpression) = isbinary(operation(expr)) ? arguments(expr)[2] : throw(ErrorException("Operation $(operation(expr)) is not binary")) isassociative(expr::LogicalExpression) = length(operations(expr)) == 1 && isassociative(operation(expr)) @@ -247,12 +235,6 @@ function setvectorindex!(expr::LogicalExpression, name::Symbol, x, index::Union{ end end -function set_argument(expr::LogicalExpression, index::Int, new_argument::AbstractExpression) - expr.arguments[index] = new_argument - expr.variables = reduce(∪, variables.(arguments(expr))) - expr -end - function Base.show(io::IO, expr::LogicalExpression) showparens(expr) = (expr isa LogicalExpression) && !isunary(operation(expr)) @@ -293,6 +275,65 @@ function Base.show(io::IO, expr::LogicalExpression) end +# Standard AbstractExpression interface methods +""" + istree(expr::T) where {T <: AbstractExpression} + +Returns true when `expr` is a `LogicalExpression` and false otherwise. +""" +istree(::LogicalSymbol) = false +istree(::LogicalExpression) = true + +""" + isnode(expr::T) where {T <: AbstractExpression} + +Returns true when `expr` is a `LogicalSymbol` and false otherwise. +""" +isnode(::LogicalSymbol) = true +isnode(::LogicalExpression) = false + +""" + variables(expr::T) where {T <: AbstractExpression} + +Returns variables present in an entire expression tree. When the first argument is a `LogicalSymbol`, this is singleton +set containing only the provided `LogicalSymbol`. When the argument is a `LogicalExpression`, this is a set containing the union +of all the variables present in each argument. +""" +variables(sym::LogicalSymbol) = Set{LogicalSymbol}(LogicalSymbol[sym]) +function variables(expr::LogicalExpression) + if !getfield(expr, :cached_variables_valid) + setfield!(expr, :cached_variables, recursivevariables(arguments(expr))) + expr.cached_variables_valid = true + end + getfield(expr, :cached_variables) +end + +""" + operations(expr::T) where {T <: AbstractExpression} + +Returns the operations present in an entire expression tree. When given a `LogicalSymbol`, this is an empty set, whereas +when given a `LogicalExpression`, this is a set containing the expression's own `LogicalOperation` and the operations set +of each of its arguments. +""" +operations(::LogicalSymbol) = Set{LogicalOperation}([]) +function operations(expr::LogicalExpression) + if !getfield(expr, :cached_operations_valid) + setfield!(expr, :cached_operations, recursiveoperations(arguments(expr), operation(expr))) + expr.cached_operations_valid = true + end + getfield(expr, :cached_operations) +end + +""" + arguments(expr::T) where {T <: AbstractExpression} + +Returns the arguments which an `AbstractExpression` contains. `LogicalSymbols` contain no arguments and `LogicalExpressions` +can contain any number of arguments. +""" +arguments(::LogicalSymbol) = AbstractExpression[] +arguments(expr::LogicalExpression) = getfield(expr, :arguments) + + # ASSOCIATION associative_ordering(sym::LogicalSymbol) = [sym] associative_ordering(expr::LogicalExpression) = reduce(vcat, associative_ordering.(arguments(expr))) From 563a81ddef3c5b81e591fee59fcd777a589edd9d Mon Sep 17 00:00:00 2001 From: Connor Burns Date: Thu, 6 Jan 2022 19:48:09 -0700 Subject: [PATCH 3/6] Completed docs for core expression library --- src/expression.jl | 94 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 89 insertions(+), 5 deletions(-) diff --git a/src/expression.jl b/src/expression.jl index 8aaca27..9d8de37 100644 --- a/src/expression.jl +++ b/src/expression.jl @@ -153,8 +153,26 @@ mutable struct LogicalExpression <: AbstractExpression expr end end +""" + operation(expr::LogicalExpression) + +The operation which is performed on the arguments of the given `LogicalExpression`. +""" operation(expr::LogicalExpression) = getfield(expr, :operation) +""" + parents(expr::LogicalExpression) + +The parent expressions of a given subexpression. If an expression is never used within another, it will have no parents. +In most expressions there will only be one parent, but it is possible for an expression assigned to a variable to have +multiple parents by using it as a "named subexpression". +""" parents(expr::LogicalExpression) = getfield(expr, :parents) + +""" + add_to_parents!(expr::LogicalExpression) + +Adds an expression to the `parents` set of all its arguments. For internal use only. +""" add_to_parents!(expr::LogicalExpression) = add_to_parents!(expr, arguments(expr)) function add_to_parents!(expr::LogicalExpression, relevant_args::Vector{AbstractExpression}) for arg ∈ relevant_args @@ -163,6 +181,12 @@ function add_to_parents!(expr::LogicalExpression, relevant_args::Vector{Abstract end end end + +""" + remove_from_parents!(expr::LogicalExpression) + +Removes an expression from the `parents` set of all its arguments. For internal use only. +""" remove_from_parents!(expr::LogicalExpression) = remove_from_parents!(expr, arguments(expr)) function remove_from_parents!(expr::LogicalExpression, relevant_args::Vector{AbstractExpression}) for arg ∈ relevant_args @@ -172,9 +196,29 @@ function remove_from_parents!(expr::LogicalExpression, relevant_args::Vector{Abs end end metadata(::LogicalExpression) = nothing +""" + left(expr::LogicalExpression) + +If the expression is binary, this method returns the left-hand operand. +""" left(expr::LogicalExpression) = isbinary(operation(expr)) ? arguments(expr)[1] : throw(ErrorException("Operation $(operation(expr)) is not binary")) +""" + right(expr::LogicalExpression) + +If the expression is binary, this method returns the right-hand operand. +""" right(expr::LogicalExpression) = isbinary(operation(expr)) ? arguments(expr)[2] : throw(ErrorException("Operation $(operation(expr)) is not binary")) +""" + isassociative(expr::LogicalExpression) + +Checks if the entire expression is associative based on the associative property of its constituent operations. +""" isassociative(expr::LogicalExpression) = length(operations(expr)) == 1 && isassociative(operation(expr)) +""" + iscommutative(expr::LogicalExpression) + +Checks if the entire expression is commutative based on the commutative property of its constituent operations. +""" iscommutative(expr::LogicalExpression) = length(operations(expr)) == 1 && iscommutative(operation(expr)) Base.hash(expr::LogicalExpression, h::UInt) = hash(arguments(expr), hash(operation(expr), h)) Base.:(==)(expr1::LogicalExpression, expr2::LogicalExpression) = operation(expr1) == operation(expr2) && all(arguments(expr1) .== arguments(expr2)) @@ -334,17 +378,33 @@ arguments(::LogicalSymbol) = AbstractExpression[] arguments(expr::LogicalExpression) = getfield(expr, :arguments) -# ASSOCIATION -associative_ordering(sym::LogicalSymbol) = [sym] +# ASSOCIATION (perhaps move this elsewhere eventually?) +""" + associative_ordering(expr::LogicalExpression) + +Descends the expression tree with a left-side-first depth first search. Each symbol encountered is added to a list in +the order it appears in this search and is returned by this function. +""" associative_ordering(expr::LogicalExpression) = reduce(vcat, associative_ordering.(arguments(expr))) +associative_ordering(sym::LogicalSymbol) = [sym] -isequal_associative(sym1::LogicalSymbol, sym2::LogicalSymbol) = isequal(sym1, sym2) +""" + isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression) + +Checks whether an expression is equal with another ignoring the associative ordering of each expression. +""" function isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression) - length(operations(expr1)) == 1 && operations(expr1) == operations(expr2) && associative_ordering(expr1) == associative_ordering(expr2) + length(operations(expr1)) == 1 && isassociative(first(operations(expr1))) && operations(expr1) == operations(expr2) && associative_ordering(expr1) == associative_ordering(expr2) end +isequal_associative(sym1::LogicalSymbol, sym2::LogicalSymbol) = isequal(sym1, sym2) isequal_associative(::AbstractExpression, ::AbstractExpression) = false _associative_tree_count_cache = Dict() +""" + associative_tree_count(nodes::Int) + +Function which calculates how many ways to arrange parenthesis in an expression there are with a given node count. +""" function associative_tree_count(nodes::Int) if nodes == 0 return 1 @@ -369,11 +429,35 @@ end # OPERATORS -# unary operator +""" + ¬(x) + +Logical negation operator, typed with `\\neg`. Boolean equivalent is the `!` operator. +""" const ¬ = LogicalOperation(x -> !x, :¬, 1, false, false) # binary operators +""" + x ∧ y + +Logical conjunction operator, typed with `\\wedge`. Boolean equivalent is the `&&` operator. +""" const ∧ = LogicalOperation((x, y) -> x && y, :∧, 2, true, true) +""" + x ∨ y + +Logical disjunction operator, typed with `\\vee`. Boolean equivalent is the `||` operator. +""" const ∨ = LogicalOperation((x, y) -> x || y, :∨, 2, true, true) +""" + x → y + +Logical implication operator, typed with `\\rightarrow`. +""" const → = LogicalOperation((x, y) -> (¬x ∨ y), :→, 2, false, false) +""" + x ⟷ y + +Logical equivalence operator, typed with `\\longleftrightarrow`. +""" const ⟷ = LogicalOperation((x, y) -> (x ∧ y) ∨ (¬x ∧ ¬y), :⟷, 2, true, true) From 9218ac32e41400badbf05774c35a9f68da9c1b7e Mon Sep 17 00:00:00 2001 From: Connor Burns Date: Thu, 6 Jan 2022 22:17:14 -0700 Subject: [PATCH 4/6] Inference docs --- src/inference.jl | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/inference.jl b/src/inference.jl index 8fc55f9..252a13d 100644 --- a/src/inference.jl +++ b/src/inference.jl @@ -8,6 +8,12 @@ export @logical_calculus, InferenceRule, PropositionalCalculus, ⊢ Statement = AbstractExpression StatementSet = Set{Statement} +""" + InferenceRule(name::String, premise::StatementSet, conclusion::Statement) + +Define a rule which maps a set of statements to a logical conclusion. The name is cited each time +a rule is applied in a proof step. +""" struct InferenceRule name::String premise::StatementSet @@ -28,6 +34,11 @@ function _leaf_symbols(expr::Expr) Set(Iterators.flatten(_leaf_symbols.(args))) end +""" +Defines a logical calculus based on a set of inference rules which can be applied repeatedly to +a given set of statements (premises). See `PropositionalCalculus` for an example definition using +this macro. +""" macro logical_calculus(var, defs) rules_list = defs.args[2].args @@ -59,8 +70,18 @@ macro logical_calculus(var, defs) end +""" + A ⊢ B + +Provability operator used exclusively in calculus definitions. A ⊢ B means that B can be proven using A as the premise. +""" ⊢ = LogicalOperation((a, b) -> true, :⊢, 2, false, false) +""" + PropositionalCalculus + +Default calculus definition for zeroth-order (propositional) logic. +""" @logical_calculus PropositionalCalculus begin "Modus Ponens", ( p → q, From edc0cc9d9b68a5b31e9a8ceb54616829de23ccac Mon Sep 17 00:00:00 2001 From: Connor Burns Date: Thu, 6 Jan 2022 22:25:33 -0700 Subject: [PATCH 5/6] Everything else besides manipulation.jl --- src/atomic.jl | 13 ++++++++++++- src/search.jl | 6 ++++++ src/utils.jl | 11 +++++++++++ 3 files changed, 29 insertions(+), 1 deletion(-) diff --git a/src/atomic.jl b/src/atomic.jl index 264fde0..06eab5f 100644 --- a/src/atomic.jl +++ b/src/atomic.jl @@ -1,9 +1,19 @@ export ⊼, atomize +""" + a ⊼ b + +Not AND operator (NAND for short). The NAND operator is a functionally complete boolean operator, meaning all other boolean +operations can be expressed with only NAND operations. +""" ⊼ = LogicalOperation((x, y) -> !(x && y), :⊼, 2, true, true) +""" + atomize(expr::AbstractExpression) + +Converts an expression into its directly converted NAND-only form. +""" # Reduce an expression to its atomic form using the NAND operation -atomize(s::LogicalSymbol) = s function atomize(expr::LogicalExpression) parts = atomize.(arguments(expr)) expr_op = operation(expr) @@ -24,3 +34,4 @@ function atomize(expr::LogicalExpression) throw(ErrorException("Expression contains unsupported atomic operator $(expr_op)")) end +atomize(s::LogicalSymbol) = s diff --git a/src/search.jl b/src/search.jl index 8dff62e..ea9627c 100644 --- a/src/search.jl +++ b/src/search.jl @@ -3,6 +3,12 @@ export contains_expression # SUBEXPRESSION SEARCH # if haystack is a logical symbol, the kneedle must be equal to be a subexpression +""" + contains_expression(haystack::AbstractExpression, kneedle::AbstractExpression) + +Searches for a subexpression `kneedle` recursively within the `haystack` expression. Returns true if a match can be found +and false otherwise. +""" contains_expression(haystack::LogicalSymbol, kneedle::AbstractExpression) = isequal(haystack, kneedle) # TODO: come up with quicker subexpression algorithm for LogicalExpressions diff --git a/src/utils.jl b/src/utils.jl index 5bbf245..1010789 100644 --- a/src/utils.jl +++ b/src/utils.jl @@ -1,5 +1,16 @@ +""" + flat_repeat(x, n) + +Shortcut for `Iterators.repeat([x], n)` +""" flat_repeat(x, n) = Iterators.repeat([x], n) +""" + FakeVector{X, T}(creator::X, fieldname::Symbol, vec::Vector{T}) + +A utility structure which calls a function `setvectorindex!` when the `Base.setindex!` function is called on it. This +allows for some smart updating of expression trees when mutated. +""" struct FakeVector{X, T} creator::X fieldname::Symbol From d7cdb9ea5db677fc539c5a15366447b95daded63 Mon Sep 17 00:00:00 2001 From: Connor Burns Date: Thu, 6 Jan 2022 22:26:57 -0700 Subject: [PATCH 6/6] Fix broken test --- src/inference.jl | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/inference.jl b/src/inference.jl index 252a13d..9562474 100644 --- a/src/inference.jl +++ b/src/inference.jl @@ -77,11 +77,6 @@ Provability operator used exclusively in calculus definitions. A ⊢ B means tha """ ⊢ = LogicalOperation((a, b) -> true, :⊢, 2, false, false) -""" - PropositionalCalculus - -Default calculus definition for zeroth-order (propositional) logic. -""" @logical_calculus PropositionalCalculus begin "Modus Ponens", ( p → q, @@ -162,6 +157,12 @@ Default calculus definition for zeroth-order (propositional) logic. p ∨ r ), q end +""" + PropositionalCalculus + +Default calculus definition for zeroth-order (propositional) logic. +""" +PropositionalCalculus @logical_calculus ExtendedPropositionalCalculus begin # Rules for negations