Skip to content

Commit

Permalink
tests pass with decapodes#migrate-diagrammatic-equations
Browse files Browse the repository at this point in the history
  • Loading branch information
@quffaro
quffaro committed Dec 19, 2023
1 parent a8b2291 commit 033334f
Show file tree
Hide file tree
Showing 4 changed files with 153 additions and 159 deletions.
18 changes: 6 additions & 12 deletions src/DiagrammaticEquations.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,26 +3,20 @@
module DiagrammaticEquations

export
DerivOp, append_dot, normalize_unicode, infer_states,
DerivOp, append_dot, normalize_unicode, infer_states, infer_types!,
# Deca
op1_res_rules_1D,
op2_res_rules_1D,
op1_res_rules_2D,
op2_res_rules_2D,
op1_inf_rules_1D,
op2_inf_rules_1D,
op1_inf_rules_2D,
op2_inf_rules_2D,
recursive_delete_parents, findname, spacename, varname, unicode!, apply_inference_rule_op1!, apply_inference_rule_op2!,
op1_res_rules_1D, op2_res_rules_1D, op1_res_rules_2D, op2_res_rules_2D,
op1_inf_rules_1D, op2_inf_rules_1D, op1_inf_rules_2D, op2_inf_rules_2D,
recursive_delete_parents, findname, spacename, varname, unicode!, vec_to_dec!,
## collages
Collage, collate,
## composition
oapply, unique_by, unique_by!, OpenSummationDecapodeOb, OpenSummationDecapode, Open,
## acset
SchDecapode, SchNamedDecapode, AbstractDecapode, AbstractNamedDecapode, NamedDecapode, SummationDecapode,
contract_operators, add_constant!, add_parameter, vec_to_dec!, infer_types!,
fill_names!, dot_rename!, expand_operators, infer_state_names, recognize_types,
contract_operators, add_constant!, add_parameter, fill_names!, dot_rename!, expand_operators, infer_state_names, recognize_types,
resolve_overloads!, replace_names!,
apply_inference_rule_op1!, apply_inference_rule_op2!,
## language
@decapode, Term, parse_decapode, term, Eq, DecaExpr,
# ~~~~~
Expand Down
144 changes: 46 additions & 98 deletions src/acset.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -329,6 +329,52 @@ function infer_summands_and_summations!(d::SummationDecapode)
return applied
end

function apply_inference_rule_op1!(d::SummationDecapode, op1_id, rule)
type_src = d[d[op1_id, :src], :type]
type_tgt = d[d[op1_id, :tgt], :type]

if(type_src != :infer && type_tgt != :infer)
return false
end

score_src = (rule.src_type == type_src)
score_tgt = (rule.tgt_type == type_tgt)
check_op = (d[op1_id, :op1] in rule.op_names)

if(check_op && (score_src + score_tgt == 1))
d[d[op1_id, :src], :type] = rule.src_type
d[d[op1_id, :tgt], :type] = rule.tgt_type
return true
end

return false
end

function apply_inference_rule_op2!(d::SummationDecapode, op2_id, rule)
type_proj1 = d[d[op2_id, :proj1], :type]
type_proj2 = d[d[op2_id, :proj2], :type]
type_res = d[d[op2_id, :res], :type]

if(type_proj1 != :infer && type_proj2 != :infer && type_res != :infer)
return false
end

score_proj1 = (rule.proj1_type == type_proj1)
score_proj2 = (rule.proj2_type == type_proj2)
score_res = (rule.res_type == type_res)
check_op = (d[op2_id, :op2] in rule.op_names)

if(check_op && (score_proj1 + score_proj2 + score_res == 2))
d[d[op2_id, :proj1], :type] = rule.proj1_type
d[d[op2_id, :proj2], :type] = rule.proj2_type
d[d[op2_id, :res], :type] = rule.res_type
return true
end

return false
end


# TODO: Although the big-O complexity is the same, it might be more efficent on
# average to iterate over edges then rules, instead of rules then edges. This
# might result in more un-maintainable code. If you implement this, you might
Expand Down Expand Up @@ -383,105 +429,7 @@ function infer_types!(d::SummationDecapode, op1_rules::Vector{NamedTuple{(:src_t
d
end

# TODO: When SummationDecapodes are annotated with the degree of their space,
# use dispatch to choose the correct set of rules.
infer_types!(d::SummationDecapode) =
infer_types!(d, op1_inf_rules_2D, op2_inf_rules_2D)

# TODO: You could write a method which auto-generates these rules given degree N.

"""
These are the default rules used to do function resolution in the 1D exterior calculus.
"""
op1_res_rules_1D = [
# Rules for d.
(src_type = :Form0, tgt_type = :Form1, resolved_name = :d₀, op = :d),
(src_type = :DualForm0, tgt_type = :DualForm1, resolved_name = :dual_d₀, op = :d),
# Rules for ⋆.
(src_type = :Form0, tgt_type = :DualForm1, resolved_name = :⋆₀, op = :⋆),
(src_type = :Form1, tgt_type = :DualForm0, resolved_name = :⋆₁, op = :⋆),
(src_type = :DualForm1, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :⋆),
(src_type = :DualForm0, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :⋆),
(src_type = :Form0, tgt_type = :DualForm1, resolved_name = :⋆₀, op = :star),
(src_type = :Form1, tgt_type = :DualForm0, resolved_name = :⋆₁, op = :star),
(src_type = :DualForm1, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :star),
(src_type = :DualForm0, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :star),
# Rules for δ.
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :δ),
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :codif)]

# We merge 1D and 2D rules since it seems op2 rules are metric-free. If
# this assumption is false, this needs to change.
op2_res_rules_1D = [
# Rules for ∧.
(proj1_type = :Form0, proj2_type = :Form0, res_type = :Form0, resolved_name = :∧₀₀, op = :∧),
(proj1_type = :Form1, proj2_type = :Form0, res_type = :Form1, resolved_name = :∧₁₀, op = :∧),
(proj1_type = :Form0, proj2_type = :Form1, res_type = :Form1, resolved_name = :∧₀₁, op = :∧),
(proj1_type = :Form0, proj2_type = :Form0, res_type = :Form0, resolved_name = :∧₀₀, op = :wedge),
(proj1_type = :Form1, proj2_type = :Form0, res_type = :Form1, resolved_name = :∧₁₀, op = :wedge),
(proj1_type = :Form0, proj2_type = :Form1, res_type = :Form1, resolved_name = :∧₀₁, op = :wedge),
# Rules for L.
(proj1_type = :Form1, proj2_type = :Form0, res_type = :Form0, resolved_name = :L₀, op = :L),
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form1, resolved_name = :L₁, op = :L),
# Rules for i.
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form0, resolved_name = :i₁, op = :i)]


"""
These are the default rules used to do function resolution in the 2D exterior calculus.
"""
op1_res_rules_2D = [
# Rules for d.
(src_type = :Form0, tgt_type = :Form1, resolved_name = :d₀, op = :d),
(src_type = :Form1, tgt_type = :Form2, resolved_name = :d₁, op = :d),
(src_type = :DualForm0, tgt_type = :DualForm1, resolved_name = :dual_d₀, op = :d),
(src_type = :DualForm1, tgt_type = :DualForm2, resolved_name = :dual_d₁, op = :d),
# Rules for ⋆.
(src_type = :Form0, tgt_type = :DualForm2, resolved_name = :⋆₀, op = :⋆),
(src_type = :Form1, tgt_type = :DualForm1, resolved_name = :⋆₁, op = :⋆),
(src_type = :Form2, tgt_type = :DualForm0, resolved_name = :⋆₂, op = :⋆),
(src_type = :DualForm2, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :⋆),
(src_type = :DualForm1, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :⋆),
(src_type = :DualForm0, tgt_type = :Form2, resolved_name = :⋆₂⁻¹, op = :⋆),
(src_type = :Form0, tgt_type = :DualForm2, resolved_name = :⋆₀, op = :star),
(src_type = :Form1, tgt_type = :DualForm1, resolved_name = :⋆₁, op = :star),
(src_type = :Form2, tgt_type = :DualForm0, resolved_name = :⋆₂, op = :star),
(src_type = :DualForm2, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :star),
(src_type = :DualForm1, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :star),
(src_type = :DualForm0, tgt_type = :Form2, resolved_name = :⋆₂⁻¹, op = :star),
# Rules for δ.
(src_type = :Form2, tgt_type = :Form1, resolved_name = :δ₂, op = :δ),
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :δ),
(src_type = :Form2, tgt_type = :Form1, resolved_name = :δ₂, op = :codif),
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :codif),
# Rules for ∇².
# TODO: Call this :nabla2 in ASCII?
(src_type = :Form0, tgt_type = :Form0, resolved_name = :∇²₀, op = :∇²),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :∇²₁, op = :∇²),
(src_type = :Form2, tgt_type = :Form2, resolved_name = :∇²₂, op = :∇²),
# Rules for Δ.
(src_type = :Form0, tgt_type = :Form0, resolved_name = :Δ₀, op = :Δ),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₁, op = :Δ),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₂, op = :Δ),
(src_type = :Form0, tgt_type = :Form0, resolved_name = :Δ₀, op = :lapl),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₁, op = :lapl),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₂, op = :lapl)]

# We merge 1D and 2D rules directly here since it seems op2 rules
# are metric-free. If this assumption is false, this needs to change.
op2_res_rules_2D = vcat(op2_res_rules_1D, [
# Rules for ∧.
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form2, resolved_name = :∧₁₁, op = :∧),
(proj1_type = :Form2, proj2_type = :Form0, res_type = :Form2, resolved_name = :∧₂₀, op = :∧),
(proj1_type = :Form0, proj2_type = :Form2, res_type = :Form2, resolved_name = :∧₀₂, op = :∧),
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form2, resolved_name = :∧₁₁, op = :wedge),
(proj1_type = :Form2, proj2_type = :Form0, res_type = :Form2, resolved_name = :∧₂₀, op = :wedge),
(proj1_type = :Form0, proj2_type = :Form2, res_type = :Form2, resolved_name = :∧₀₂, op = :wedge),
# Rules for L.
(proj1_type = :Form1, proj2_type = :Form2, res_type = :Form2, resolved_name = :L₂, op = :L),
(proj1_type = :Form1, proj2_type = :DualForm2, res_type = :DualForm2, resolved_name = :L₂ᵈ, op = :L),
# Rules for i.
(proj1_type = :Form1, proj2_type = :Form2, res_type = :Form1, resolved_name = :i₂, op = :i)])

""" function resolve_overloads!(d::SummationDecapode, op1_rules::Vector{NamedTuple{(:src_type, :tgt_type, :resolved_name, :op), NTuple{4, Symbol}}})
Expand Down
16 changes: 6 additions & 10 deletions src/deca/Deca.jl
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,16 @@
module Deca

using DataStructures
using ..DiagrammaticEquations
using Catlab

import ..infer_types!, ..resolve_overloads!

export normalize_unicode, varname, infer_states, infer_types!, resolve_overloads!, typename, spacename, recursive_delete_parents, recursive_delete_parents!, unicode!, op1_res_rules_1D, op2_res_rules_1D, op1_res_rules_2D, op2_res_rules_2D, op1_inf_rules_1D, op2_inf_rules_1D, op1_inf_rules_2D, op2_inf_rules_2D, vec_to_dec!

include("deca_acset.jl")
include("deca_visualization.jl")

export normalize_unicode, varname, infer_states, infer_types!, typename, spacename, recursive_delete_parents, recursive_delete_parents!, unicode!, replace_names!, op1_res_rules_1D,
op2_res_rules_1D,
op1_res_rules_2D,
op2_res_rules_2D,
op1_inf_rules_1D,
op2_inf_rules_1D,
op1_inf_rules_2D,
op2_inf_rules_2D,
apply_inference_rule_op1!, apply_inference_rule_op2!

## TODO: where?
function infer_states(d::SummationDecapode)
filter(parts(d, :Var)) do v
Expand Down
134 changes: 95 additions & 39 deletions src/deca/deca_acset.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,50 +137,106 @@ op2_inf_rules_2D = vcat(op2_inf_rules_1D, [
(proj1_type = :Literal, proj2_type = :Form2, res_type = :Form2, op_names = [:/, :./, :*, :.*]),
(proj1_type = :Form2, proj2_type = :Literal, res_type = :Form2, op_names = [:/, :./, :*, :.*])])

function apply_inference_rule_op1!(d::SummationDecapode, op1_id, rule)
type_src = d[d[op1_id, :src], :type]
type_tgt = d[d[op1_id, :tgt], :type]

if(type_src != :infer && type_tgt != :infer)
return false
end

score_src = (rule.src_type == type_src)
score_tgt = (rule.tgt_type == type_tgt)
check_op = (d[op1_id, :op1] in rule.op_names)

if(check_op && (score_src + score_tgt == 1))
d[d[op1_id, :src], :type] = rule.src_type
d[d[op1_id, :tgt], :type] = rule.tgt_type
return true
end

return false
end
# TODO: You could write a method which auto-generates these rules given degree N.

function apply_inference_rule_op2!(d::SummationDecapode, op2_id, rule)
type_proj1 = d[d[op2_id, :proj1], :type]
type_proj2 = d[d[op2_id, :proj2], :type]
type_res = d[d[op2_id, :res], :type]
"""
These are the default rules used to do function resolution in the 1D exterior calculus.
"""
op1_res_rules_1D = [
# Rules for d.
(src_type = :Form0, tgt_type = :Form1, resolved_name = :d₀, op = :d),
(src_type = :DualForm0, tgt_type = :DualForm1, resolved_name = :dual_d₀, op = :d),
# Rules for ⋆.
(src_type = :Form0, tgt_type = :DualForm1, resolved_name = :⋆₀, op = :⋆),
(src_type = :Form1, tgt_type = :DualForm0, resolved_name = :⋆₁, op = :⋆),
(src_type = :DualForm1, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :⋆),
(src_type = :DualForm0, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :⋆),
(src_type = :Form0, tgt_type = :DualForm1, resolved_name = :⋆₀, op = :star),
(src_type = :Form1, tgt_type = :DualForm0, resolved_name = :⋆₁, op = :star),
(src_type = :DualForm1, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :star),
(src_type = :DualForm0, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :star),
# Rules for δ.
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :δ),
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :codif)]

# We merge 1D and 2D rules since it seems op2 rules are metric-free. If
# this assumption is false, this needs to change.
op2_res_rules_1D = [
# Rules for ∧.
(proj1_type = :Form0, proj2_type = :Form0, res_type = :Form0, resolved_name = :∧₀₀, op = :∧),
(proj1_type = :Form1, proj2_type = :Form0, res_type = :Form1, resolved_name = :∧₁₀, op = :∧),
(proj1_type = :Form0, proj2_type = :Form1, res_type = :Form1, resolved_name = :∧₀₁, op = :∧),
(proj1_type = :Form0, proj2_type = :Form0, res_type = :Form0, resolved_name = :∧₀₀, op = :wedge),
(proj1_type = :Form1, proj2_type = :Form0, res_type = :Form1, resolved_name = :∧₁₀, op = :wedge),
(proj1_type = :Form0, proj2_type = :Form1, res_type = :Form1, resolved_name = :∧₀₁, op = :wedge),
# Rules for L.
(proj1_type = :Form1, proj2_type = :Form0, res_type = :Form0, resolved_name = :L₀, op = :L),
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form1, resolved_name = :L₁, op = :L),
# Rules for i.
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form0, resolved_name = :i₁, op = :i)]

if(type_proj1 != :infer && type_proj2 != :infer && type_res != :infer)
return false
end

score_proj1 = (rule.proj1_type == type_proj1)
score_proj2 = (rule.proj2_type == type_proj2)
score_res = (rule.res_type == type_res)
check_op = (d[op2_id, :op2] in rule.op_names)
"""
These are the default rules used to do function resolution in the 2D exterior calculus.
"""
op1_res_rules_2D = [
# Rules for d.
(src_type = :Form0, tgt_type = :Form1, resolved_name = :d₀, op = :d),
(src_type = :Form1, tgt_type = :Form2, resolved_name = :d₁, op = :d),
(src_type = :DualForm0, tgt_type = :DualForm1, resolved_name = :dual_d₀, op = :d),
(src_type = :DualForm1, tgt_type = :DualForm2, resolved_name = :dual_d₁, op = :d),
# Rules for ⋆.
(src_type = :Form0, tgt_type = :DualForm2, resolved_name = :⋆₀, op = :⋆),
(src_type = :Form1, tgt_type = :DualForm1, resolved_name = :⋆₁, op = :⋆),
(src_type = :Form2, tgt_type = :DualForm0, resolved_name = :⋆₂, op = :⋆),
(src_type = :DualForm2, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :⋆),
(src_type = :DualForm1, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :⋆),
(src_type = :DualForm0, tgt_type = :Form2, resolved_name = :⋆₂⁻¹, op = :⋆),
(src_type = :Form0, tgt_type = :DualForm2, resolved_name = :⋆₀, op = :star),
(src_type = :Form1, tgt_type = :DualForm1, resolved_name = :⋆₁, op = :star),
(src_type = :Form2, tgt_type = :DualForm0, resolved_name = :⋆₂, op = :star),
(src_type = :DualForm2, tgt_type = :Form0, resolved_name = :⋆₀⁻¹, op = :star),
(src_type = :DualForm1, tgt_type = :Form1, resolved_name = :⋆₁⁻¹, op = :star),
(src_type = :DualForm0, tgt_type = :Form2, resolved_name = :⋆₂⁻¹, op = :star),
# Rules for δ.
(src_type = :Form2, tgt_type = :Form1, resolved_name = :δ₂, op = :δ),
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :δ),
(src_type = :Form2, tgt_type = :Form1, resolved_name = :δ₂, op = :codif),
(src_type = :Form1, tgt_type = :Form0, resolved_name = :δ₁, op = :codif),
# Rules for ∇².
# TODO: Call this :nabla2 in ASCII?
(src_type = :Form0, tgt_type = :Form0, resolved_name = :∇²₀, op = :∇²),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :∇²₁, op = :∇²),
(src_type = :Form2, tgt_type = :Form2, resolved_name = :∇²₂, op = :∇²),
# Rules for Δ.
(src_type = :Form0, tgt_type = :Form0, resolved_name = :Δ₀, op = :Δ),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₁, op = :Δ),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₂, op = :Δ),
(src_type = :Form0, tgt_type = :Form0, resolved_name = :Δ₀, op = :lapl),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₁, op = :lapl),
(src_type = :Form1, tgt_type = :Form1, resolved_name = :Δ₂, op = :lapl)]

# We merge 1D and 2D rules directly here since it seems op2 rules
# are metric-free. If this assumption is false, this needs to change.
op2_res_rules_2D = vcat(op2_res_rules_1D, [
# Rules for ∧.
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form2, resolved_name = :∧₁₁, op = :∧),
(proj1_type = :Form2, proj2_type = :Form0, res_type = :Form2, resolved_name = :∧₂₀, op = :∧),
(proj1_type = :Form0, proj2_type = :Form2, res_type = :Form2, resolved_name = :∧₀₂, op = :∧),
(proj1_type = :Form1, proj2_type = :Form1, res_type = :Form2, resolved_name = :∧₁₁, op = :wedge),
(proj1_type = :Form2, proj2_type = :Form0, res_type = :Form2, resolved_name = :∧₂₀, op = :wedge),
(proj1_type = :Form0, proj2_type = :Form2, res_type = :Form2, resolved_name = :∧₀₂, op = :wedge),
# Rules for L.
(proj1_type = :Form1, proj2_type = :Form2, res_type = :Form2, resolved_name = :L₂, op = :L),
(proj1_type = :Form1, proj2_type = :DualForm2, res_type = :DualForm2, resolved_name = :L₂ᵈ, op = :L),
# Rules for i.
(proj1_type = :Form1, proj2_type = :Form2, res_type = :Form1, resolved_name = :i₂, op = :i)])

if(check_op && (score_proj1 + score_proj2 + score_res == 2))
d[d[op2_id, :proj1], :type] = rule.proj1_type
d[d[op2_id, :proj2], :type] = rule.proj2_type
d[d[op2_id, :res], :type] = rule.res_type
return true
end
# TODO: When SummationDecapodes are annotated with the degree of their space,
# use dispatch to choose the correct set of rules.
infer_types!(d::SummationDecapode) =
infer_types!(d, op1_inf_rules_2D, op2_inf_rules_2D)

return false
end

ascii_to_unicode_op1 = Pair{Symbol, Any}[
(:dt => :∂ₜ),
Expand Down

0 comments on commit 033334f

Please sign in to comment.