From a0ae6d15cf211d1f46797a3611d977e3dd807c13 Mon Sep 17 00:00:00 2001 From: Owen Lynch Date: Wed, 13 Mar 2024 09:52:02 -0400 Subject: [PATCH] fixup: make more things work for the trie refactor --- docs/src/concepts/theory_composition.md | 51 +++++++++ docs/src/examples/springs.md | 5 + src/nonstdlib/dynamics/ResourceSharers.jl | 129 ++++++++++++++++++---- src/syntax/Tries.jl | 48 ++++---- src/syntax/gats/ast.jl | 35 +++--- src/syntax/gats/closures.jl | 12 +- src/syntax/gats/exprinterop.jl | 14 ++- test/Project.toml | 3 + test/nonstdlib/ResourceSharers.jl | 80 +++++++++----- 9 files changed, 286 insertions(+), 91 deletions(-) create mode 100644 docs/src/concepts/theory_composition.md create mode 100644 docs/src/examples/springs.md diff --git a/docs/src/concepts/theory_composition.md b/docs/src/concepts/theory_composition.md new file mode 100644 index 00000000..e0be15e0 --- /dev/null +++ b/docs/src/concepts/theory_composition.md @@ -0,0 +1,51 @@ +# Theory Composition + +As theories get larger, it becomes more and more important to not build the +entire theory from scratch. Not only is this tedious, it is also error-prone. +From the beginning, Catlab and GATlab have supported single inheritance, which +helps to some extent. In this document, we lay out other approaches to composing +theories. + +## Multiple Inheritance + +In a GATlab `@theory`, one can use `using` to take the *union* of one theory +with another theory. + +The way this works is the following. Every time a new theory is created, the new +definitions for that theory form a new scope, with a unique UUID. Union of +theories operates on a scope tag level, taking the union of the sets of UUIDs +and then producing a theory with all the bindings from the scopes tagged by +those UUIDs. + +If we never had to parse user-supplied expressions, then the names of the +operations in the theories wouldn't matter, because identifiers come with scope +tags. However, as a practical matter, we disallow unioning two theories with the +same name declaration. + +That being said, it is fine to union two theories which *overload* the same +declaration. That is, if two theories have the declaration of a name in common, +then they can overload that name as long as they don't give conflicting +overloads, in the same way that overloading methods in Julia works. + +This is akin to the way multiple inheritance works in frameworks such as + +- Haskell typeclasses +- [Object-oriented systems with multiple inheritance, like Scala](https://docs.scala-lang.org/scala3/book/domain-modeling-tools.html#traits) +- [Module inclusion in OCaml](https://cs3110.github.io/textbook/chapters/modules/includes.html) + +## Nesting + +However, there are other ways of composing things like GATlab theories. In +dependently typed languages used for theorem proving, algebraic structures are +often represented by dependent records. For instance, in the agda unimath +library, the [definition of a group](https://github.com/UniMath/agda-unimath/blob/master/src/group-theory/groups.lagda.md) is + +```agda +Semigroup : + (l : Level) → UU (lsuc l) +Semigroup l = Σ (Set l) has-associative-mul-Set + +Group : + (l : Level) → UU (lsuc l) +Group l = Σ (Semigroup l) is-group +``` diff --git a/docs/src/examples/springs.md b/docs/src/examples/springs.md new file mode 100644 index 00000000..f5d2d593 --- /dev/null +++ b/docs/src/examples/springs.md @@ -0,0 +1,5 @@ +# Composition of resource sharers + +```julia + +``` diff --git a/src/nonstdlib/dynamics/ResourceSharers.jl b/src/nonstdlib/dynamics/ResourceSharers.jl index ed843ec8..4664f368 100644 --- a/src/nonstdlib/dynamics/ResourceSharers.jl +++ b/src/nonstdlib/dynamics/ResourceSharers.jl @@ -1,10 +1,11 @@ module ResourceSharers -export Rhizome, @rhizome, ResourceSharer, Variable +export Rhizome, @rhizome, ResourceSharer, @resource_sharer, Variable using ...Syntax using ...Syntax.Tries using ...Syntax.Tries: flatten, node using ...Syntax.GATs: tcompose +using ...Util using MLStyle using OrderedCollections @@ -77,11 +78,11 @@ The only problem is that I'm not sure then what to call the single field in `Rhizome`. Also, this would require a slight refactor of the rest of the code. """ struct Rhizome + theory::GAT + mcompose::AlgClosure + mzero::AlgClosure boxes::Trie{Trie{PortVariable}} junctions::Trie{Variable} - function Rhizome(boxes::Trie{Trie{PortVariable}}, junctions::Trie{Variable}) - new(boxes, junctions) - end end """ @@ -102,15 +103,15 @@ databases, recursion, and plug-and-play circuits](https://arxiv.org/abs/1305.029 function ocompose(r::Rhizome, rs::Trie{Rhizome}) # paired :: Trie{Tuple{Trie{PortVariable}, Rhizome}} paired = zip(r.boxes, rs) - boxes = flatten(mapwithkey(paired) do k, (interface, r′) + boxes = flatten(mapwithkey(Trie{Trie{PortVariable}}, paired) do k, (interface, r′) # k :: TrieVar # interface :: Trie{PortVariable} # r′ :: Rhizome # We want to create the new collection of boxes - map(r′.boxes) do b + map(Trie{PortVariable}, r′.boxes) do b # b :: Trie{PortVariable} - map(b) do p + map(PortVariable, b) do p # p :: PortVariable # p.junction :: namespace(b.junctions) jvar = p.junction @@ -128,7 +129,7 @@ function ocompose(r::Rhizome, rs::Trie{Rhizome}) end) # Add all unexposed junctions newjunctions = flatten( - map(rs) do r′ + map(Trie{Variable}, rs) do r′ internal_junctions = filter(j -> !j.exposed, r′.junctions) if isnothing(internal_junctions) Tries.node(OrderedDict{Symbol, Trie{Variable}}()) @@ -140,7 +141,7 @@ function ocompose(r::Rhizome, rs::Trie{Rhizome}) junctions = merge(r.junctions, newjunctions) - Rhizome(boxes, junctions) + Rhizome(r.theory, r.mcompose, r.mzero, boxes, junctions) end # TODO: this should just use a `toexpr` method @@ -210,9 +211,9 @@ will be assumed to be of that type. 3. The namespace for the external ports of the rhizome is `[a, b]`. As noted in 1., each of these ports is typed with `default`. """ -macro rhizome(theory, head, body) +macro rhizome(theorymod, head, body) # macroexpand `theory` to get the actual theory - theory = macroexpand(__module__, :($theory.Meta.@theory)) + theory = macroexpand(__module__, :($theorymod.Meta.@theory)) # parse the name and junctions out of `head` junctions = OrderedDict{TrieVar, Variable}() (name, args) = @match head begin @@ -254,8 +255,14 @@ macro rhizome(theory, head, body) boxes[box] = Trie(interface) end :( - $(esc(name)) = $(Rhizome(Trie(boxes), junctions)) - ) + $name = $Rhizome( + $theory, + $theorymod.Meta.Constructors.:(+), + $theorymod.Meta.Constructors.zero, + $(Trie(boxes)), + $(junctions), + ) + ) |> esc end """ @@ -275,6 +282,82 @@ struct ResourceSharer # observe::AlgClosure end +""" +A DSL for writing down resource sharers + +Example: +``` +@resource_sharer ThRing Spring begin + variables = x, v + params = k + update = (state, params) -> (x = state.v, v = -params.k * state.x) +end +``` +""" +macro resource_sharer(theory, name, body) + args = Expr[] + + for line in body.args + @match line begin + _ :: LineNumberNode => nothing + Expr(:(=), arg, val) => + push!(args, Expr(:kw, arg, Expr(:quote, val))) + end + end + + esc(:($name = $ResourceSharer($theory.Meta.theory; $(args...)))) +end + +function parse_namespace(theory::GAT, expr::Expr0) + vs = OrderedDict{TrieVar, AlgType}() + argexprs = @match expr begin + Expr(:tuple, args...) => args + _ => [expr] + end + for arg in argexprs + (vname, typeexpr) = @match arg begin + vname::Symbol => (vname, :default) + Expr(:(.), _, _) => (arg, :default) + Expr(:(::), vname, type) => (vname, type) + end + v = parse_var(vname) + type = fromexpr(theory, typeexpr, AlgType) + vs[v] = type + end + Trie(vs) +end + +function ResourceSharer(theory::GAT; variables::Expr0, params::Expr0, update::Expr0) + variable_trie = parse_namespace(theory, variables) + variables = map(Variable, variable_trie) do type + Variable(true, type) + end + param_type = tcompose(parse_namespace(theory, params)) + state_type = tcompose(variable_trie) + + update = begin + (argexpr, bodyexpr) = @match update begin + Expr(:(->), args, body) => (args, last(body.args)) + end + statename, paramname = @match argexpr begin + Expr(:tuple, s, p) => (s, p) + end + args = TypeScope(statename => state_type, paramname => param_type) + body = fromexpr(GATContext(theory, args), bodyexpr, AlgTerm) + AlgMethod(args, body, "", LID.([1,2]), state_type) + end + + ResourceSharer(variables, param_type, update) +end + +function Base.show(io::IO, r::ResourceSharer; theory) + println(io, "ResourceSharer:") + print(io, "variables = ", map(v -> string(toexpr(theory, v.type)), String, r.variables)) + println(io, "params = ", toexpr(theory, r.params)) + println(io, "update = ") + show(io, r.update; theory) +end + """ If C is a cartesian category, and t1 and t2 are families of objects in C with a function of finite sets dom(t2) -> dom(t1), then we can use "copy and delete" to form a morphism in C @@ -294,7 +377,7 @@ function pullback(t1::Trie{AlgType}, t2::Trie{Tuple{AlgType, TrieVar}}; argname= ctx = TypeScope(argname => ty1) x = AlgTerm(ident(ctx; name=argname)) body = tcompose( - map(t2) do (_, k) + map(AlgTerm, t2) do (_, k) x[k] end ) @@ -318,8 +401,8 @@ Produces an AlgMethod going from tcompose(first.(t2)) to tcompose(t1) function pushforward( t1::Trie{AlgType}, t2::Trie{Tuple{AlgType, TrieVar}}, - mcompose::Tuple{Ident, Ident}, - mzero::Tuple{Ident, Ident}; + mcompose::AlgClosure, + mzero::AlgClosure; argname=:x ) preimages = Dict{TrieVar, Vector{TrieVar}}() @@ -335,18 +418,18 @@ function pushforward( ctx = TypeScope(argname => ty2) x = AlgTerm(ident(ctx; name=argname)) body = tcompose( - mapwithkey(t1) do k, _ + mapwithkey(AlgTerm, t1) do k, _ foldl( - (term, v) -> AlgTerm(mcompose..., [term, x[v]]), + (term, v) -> first(values(mcompose.methods))(term, x[v]), preimages[k]; - init=AlgTerm(mzero..., AlgTerm[]) + init=mzero() ) end ) AlgMethod(ctx, body, "", [LID(1)], ty1) end -function oapply(r::Rhizome, sharers::Trie{ResourceSharer}, mcompose, mzero) +function oapply(r::Rhizome, sharers::Trie{ResourceSharer}) new_variables = filter(v -> !v.exposed, flatten( map(sharers) do sharer sharer.variables @@ -365,8 +448,8 @@ function oapply(r::Rhizome, sharers::Trie{ResourceSharer}, mcompose, mzero) # to their type, and to the variable in the reduced system that they # map to full_state = flatten( - mapwithkey(zip(r.boxes, sharers)) do b, (interface, sharer) - mapwithkey(sharer.variables) do k, v + mapwithkey(Trie{Tuple{AlgType, TrieVar}}, zip(r.boxes, sharers)) do b, (interface, sharer) + mapwithkey(Tuple{AlgType, TrieVar}, sharer.variables) do k, v if v.exposed (v.type, interface[k].junction) else @@ -385,7 +468,7 @@ function oapply(r::Rhizome, sharers::Trie{ResourceSharer}, mcompose, mzero) copy = pullback(state, full_state; argname=:state) # add :: full_state -> state - add = pushforward(state, full_state, mcompose, mzero) + add = pushforward(state, full_state, r.mcompose, r.mzero) update_ctx = TypeScope(:state => state_type, :params => params) statevar, paramsvar = AlgTerm.(idents(update_ctx; name=[:state, :params])) diff --git a/src/syntax/Tries.jl b/src/syntax/Tries.jl index c9238462..e154ebd4 100644 --- a/src/syntax/Tries.jl +++ b/src/syntax/Tries.jl @@ -121,6 +121,9 @@ function content(p::Trie) end end +""" +Construct a new Trie node. +""" function node(d::OrderedDict{Symbol, <:AbstractTrie{A}}) where {A} nonempties = OrderedDict{Symbol, NonEmptyTrie{A}}() for (k, t) in pairs(d) @@ -134,7 +137,7 @@ function node(d::OrderedDict{Symbol, <:AbstractTrie{A}}) where {A} if length(nonempties) > 0 Trie{A}(NonEmptyTrie{A}(Node_{NonEmptyTrie{A}}(nonempties))) else - Trie{A}(nothing) + Trie{A}() end end @@ -267,7 +270,12 @@ function Base.map(f, return_type::Type, t::AbstractTrie) end end -function flatten(t::Trie{Trie{A}})::Trie{A} where {A} +function Base.map(f, t::AbstractTrie{A}) where {A} + B = Core.Compiler.return_type(f, Tuple{A}) + map(f, B, t) +end + +function flatten(t::AbstractTrie{Trie{A}}) where {A} @match t begin Leaf(v) => v Node(bs) => node(n => flatten(v) for (n, v) in bs) @@ -315,16 +323,16 @@ function mapwithkey(f, return_type::Type, t::AbstractTrie; prefix=PACKAGE_ROOT) @match t begin Leaf(v) => leaf(f(prefix, v)) Node(bs) => - node([k => mapwithkey(f, v; prefix=getproperty(prefix, k)) for (k, v) in bs]...) + node([k => mapwithkey(f, return_type, v; prefix=getproperty(prefix, k)) for (k, v) in bs]...) Empty() => Trie{return_type}() end end -function traversewithkey(f, t::Trie; prefix=PACKAGE_ROOT) +function traversewithkey(f, t::AbstractTrie; prefix=PACKAGE_ROOT) @match t begin Leaf(v) => (f(prefix, v); nothing) Node(bs) => begin - for (k, v) in branches(t) + for (k, v) in bs traversewithkey(f, v; prefix=getproperty(prefix, k)) end end @@ -349,8 +357,8 @@ function Base.merge(t1::AbstractTrie{A}, t2::AbstractTrie{A}) where {A} @match (t1, t2) begin (Leaf(_), _) || (_, Leaf(_)) => error("cannot merge tries with overlapping keys") - (Empty, _) => t2 - (_, Empty) => t1 + (Empty(), _) => t2 + (_, Empty()) => t1 (Node(b1), Node(b2)) => begin b = OrderedDict{Symbol, NonEmptyTrie{A}}() for (n, t) in b1 @@ -378,19 +386,19 @@ Fails if the keys in the dict are not prefix-free. function Trie(d::OrderedDict{TrieVar, A}) where {A} branches = OrderedDict{Symbol, OrderedDict{TrieVar, A}}() for (v, x) in d - if isroot(v) - if length(d) == 1 - return leaf(x) - else - error("attempted trie conversion failed because keys were not prefix-free") - end - else - (n, v′) = content(v) - if haskey(branches, n) - branches[n][v′] = x - else - branches[n] = OrderedDict(v′ => x) - end + @match v begin + Root() => + if length(d) == 1 + return leaf(x) + else + error("attempted trie conversion failed because keys were not prefix-free") + end + Nested((n, v′)) => + if haskey(branches, n) + branches[n][v′] = x + else + branches[n] = OrderedDict(v′ => x) + end end end node(n => Trie(d′) for (n, d′) in branches) diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl index c370a5e6..df0c5a4f 100644 --- a/src/syntax/gats/ast.jl +++ b/src/syntax/gats/ast.jl @@ -138,13 +138,15 @@ rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::AlgTerm) = retag(reps::Dict{ScopeTag, ScopeTag}, t::AlgTerm) = AlgTerm(retag(reps, t.body)) -function tcompose(t::Trie{AlgTerm}) - if Tries.isleaf(t) - t[] - else - AlgTerm(AlgNamedTuple{AlgTerm}(OrderedDict{Symbol, AlgTerm}( - (n, tcompose(v)) for (n, v) in Tries.branches(t) - ))) +function tcompose(t::AbstractTrie{AlgTerm}) + @match t begin + Tries.Leaf(v) => v + Tries.Node(bs) => + AlgTerm(AlgNamedTuple{AlgTerm}(OrderedDict{Symbol, AlgTerm}( + (n, tcompose(v)) for (n, v) in bs + ))) + Tries.Empty() => + AlgTerm(AlgNamedTuple{AlgTerm}(OrderedDict{Symbol, AlgTerm}())) end end @@ -237,11 +239,12 @@ function AlgSort(t::AlgType) end end -function tcompose(t::Trie{AlgType}) - if Tries.isnode(t) - AlgType(AlgNamedTuple(OrderedDict(k => tcompose(v) for (k,v) in AbstractTrees.children(t)))) - else - t[] +function tcompose(t::AbstractTrie{AlgType}) + @match t begin + Tries.Node(bs) => + AlgType(AlgNamedTuple(OrderedDict(k => tcompose(v) for (k,v) in AbstractTrees.children(t)))) + Tries.Leaf(v) => v + Tries.Empty() => AlgType(AlgNamedTuple(OrderedDict{Symbol, AlgType}())) end end @@ -293,11 +296,9 @@ headof(a::AlgDot) = a.head bodyof(a::AlgDot) = a.body function Base.getindex(a::AlgTerm, v::TrieVar) - if Tries.isroot(v) - a - else - (n, v′) = Tries.content(v) - getindex(AlgTerm(AlgDot(n, a)), v′) + @match v begin + Tries.Root() => a + Tries.Nested((n, v′)) => getindex(AlgTerm(AlgDot(n, a)), v′) end end diff --git a/src/syntax/gats/closures.jl b/src/syntax/gats/closures.jl index 60b9a255..59cf595a 100644 --- a/src/syntax/gats/closures.jl +++ b/src/syntax/gats/closures.jl @@ -45,20 +45,21 @@ function tcompose(ms::Trie{AlgMethod}, argnames::Vector{Symbol}) # Then create a new typescope with the same variable names, but with types # given by tcompose of the argument types of the ms - contexts = map(m -> m.context, ms) + contexts = map(m -> m.context, TypeScope, ms) context = TypeScope( - Scope([x => tcompose(map(ctx -> getvalue(ctx, LID(i)), contexts)) for (i,x) in enumerate(argnames)]...) + Scope([x => tcompose(map(ctx -> getvalue(ctx, LID(i)), AlgType, contexts)) for (i,x) in enumerate(argnames)]...) ) # Then for each method, create a new body by applying it to the variables # in the new scope with the appropriate AlgDots added - bodies = mapwithkey(ms) do k, m + bodies = mapwithkey(AlgTerm, ms) do k, m m([AlgTerm(x)[k] for x in getidents(context)]...) end # Finally, compose all of the bodies into an expression creating an # AlgNamedTuple body = Tries.fold( + AlgTerm(AlgNamedTuple(OrderedDict{Symbol, AlgTerm}())), x -> x, d -> AlgTerm(AlgNamedTuple{AlgTerm}(d)), bodies @@ -131,6 +132,11 @@ function Base.show(io::IO, f::AlgClosure) print(io, fndef) end +function Base.show(io::IO, m::AlgMethod; theory) + fndef = Expr(:(->), Expr(:tuple, toexpr(theory, m.context).args...), toexpr(GATContext(theory, m.context), m.body)) + print(io, fndef) +end + function strip_annot(t::AlgTerm) if isannot(t) strip_annot(t.body.term) diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl index d84d869e..cdb26c00 100644 --- a/src/syntax/gats/exprinterop.jl +++ b/src/syntax/gats/exprinterop.jl @@ -37,9 +37,21 @@ function fromexpr(c::GATContext, e, ::Type{AlgTerm}) Expr(:., body, QuoteNode(head)) => begin t = fromexpr(c, body, AlgTerm) AlgTerm(AlgDot(head, t)) - end + end Expr(:call, head::Symbol, argexprs...) => AlgTerm(parse_methodapp(c, head, argexprs)) Expr(:(::), val, type) => AlgTerm(Constant(val, fromexpr(c, type, AlgType))) + Expr(:tuple, kvs...) => AlgTerm( + AlgNamedTuple{AlgTerm}( + OrderedDict{Symbol, AlgTerm}( + map(kvs) do kv + @match kv begin + Expr(:(=), k, v) => (k => fromexpr(c, v, AlgTerm)) + _ => error("expected key-value pairs inside tuple") + end + end + ) + ) + ) e::Expr => error("could not parse AlgTerm from $e") constant::Constant => AlgTerm(constant) end diff --git a/test/Project.toml b/test/Project.toml index 41e39c56..d58dae29 100644 --- a/test/Project.toml +++ b/test/Project.toml @@ -1,7 +1,10 @@ [deps] AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c" +ComponentArrays = "b0b7db55-cfe3-40fc-9ded-d10e2dbeff66" +DataFrames = "a93c6f00-e57d-5684-b7b6-d8193f3e46c0" DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2" MLStyle = "d8e11817-5142-5d16-987a-aa16d5891078" +Plots = "91a5bcdd-55d7-5caf-9e0b-520d859cae80" StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c" Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" diff --git a/test/nonstdlib/ResourceSharers.jl b/test/nonstdlib/ResourceSharers.jl index 7f8bc155..b71ceb3f 100644 --- a/test/nonstdlib/ResourceSharers.jl +++ b/test/nonstdlib/ResourceSharers.jl @@ -7,21 +7,7 @@ using GATlab.NonStdlib.ResourceSharers: ocompose, oapply using GATlab using GATlab.Syntax.GATs: tcompose -@rhizome ThMonoid rtop(a, b) begin - X(a) - Y(a, c.x = b) -end - -@rhizome ThMonoid rX(a) begin - A(x = a, y = a) -end - -@rhizome ThMonoid rY(a, c.x) begin - A(x = a, y = a) - B(t = c.x) -end - -r = ocompose(rtop, node(:X => leaf(rX), :Y => leaf(rY))) +import Base: +, *, - @theory ThRing begin default::TYPE @@ -32,27 +18,67 @@ r = ocompose(rtop, node(:X => leaf(rX), :Y => leaf(rY))) (-(x::default))::default end -deftype = fromexpr(ThRing.Meta.theory, :default, AlgType) -spring_variables = node(:x => leaf(Variable(true, deftype)), :v => leaf(Variable(true, deftype))) -spring_params = tcompose(node(:k => leaf(deftype))) -@algebraic ThRing spring_update(s::(x,v), p::(k,)) = (x = s.v, v = - p.k * s.x) +@rhizome ThRing rtop(a, b) begin + X(a) + Y(a, c.x = b) +end + +@rhizome ThRing rX(a) begin + A(x = a, y = a) +end + +@rhizome ThRing rY(a, c.x) begin + A(x = a, y = a) + B(t = c.x) +end -Spring = ResourceSharer(spring_variables, spring_params, first(values(spring_update.methods))) +r = ocompose(rtop, Trie(■.X => rX, ■.Y => rY)) -gravity_variables = node(:v => leaf(Variable(true, deftype))) -gravity_params = tcompose(node(:g => leaf(deftype))) -@algebraic ThRing gravity_update(s::(v,), p::(g,)) = (v = - p.g,) +@resource_sharer ThRing Spring begin + variables = x, v + params = k + update = (state, params) -> (x = state.v, v = -params.k * state.x) +end; +show(stdout, Spring; theory=ThRing.Meta.theory) -Gravity = ResourceSharer(gravity_variables, gravity_params, first(values(gravity_update.methods))) +@resource_sharer ThRing Gravity begin + variables = v + params = g + update = (state, params) -> (v = - params.g,) +end; +show(stdout, Gravity; theory=ThRing.Meta.theory) @rhizome ThRing SpringGravity(x, v) begin spring(x, v) gravity(v) end -z = fromexpr(ThRing.Meta.theory, :(zero()), AlgTerm) -p = fromexpr(ThRing.Meta.theory, :(zero() + zero()), AlgTerm) +s = oapply(SpringGravity, Trie(■.spring => Spring, ■.gravity => Gravity)); +show(stdout, s; theory=ThRing.Meta.theory) + +body = toexpr(GATContext(ThRing.Meta.theory, s.update.context), s.update.body) + +zero() = 0.0 + +eval( + :(update(state, params) = ComponentArray(;$(body.args...))) +) + +update((x = 0.0, v = 1.0), (spring = (k = 1.0,), gravity = (g = 9.8,))) + +init = ComponentArray(x = 0.0, v = 1.0) +params = ComponentArray(spring = (k = 1.0,), gravity = (g = 9.8,)) + +function euler(init, params, v, dt, steps) + values = Vector{typeof(init)}(undef, steps+1) + values[1] = init + for i in 1:steps + values[i+1] = values[i] .+ (dt .* v(values[i], params)) + end + values +end -oapply( SpringGravity, node(:spring => leaf(Spring), :gravity => leaf(Gravity)), (p.body.head, p.body.method), (z.body.head, z.body.method)) +traj = euler(init, params, update, 0.1, 100); +DataFrame(x = getproperty.(traj, Ref(:x)), v = getproperty.(traj, Ref(:v))) end