directories and symbolic resource sharers

Author: olynch

.editorconfig

@@ -0,0 +1,2 @@
+[*.jl]
+indent_size = 2

.gitignore

@@ -26,3 +26,4 @@ docs/site/
 # committed for packages, but should be committed for applications that require a static
 # environment.
 Manifest.toml
+/coverage/

Project.toml

@@ -4,13 +4,15 @@ authors = ["AlgebraicJulia Developers"]
 version = "0.1.3"
 
 [deps]
+AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"
 AlgebraicInterfaces = "23cfdc9f-0504-424a-be1f-4892b28e2f0c"
 Colors = "5ae59095-9a9b-59fe-a467-6f913c188581"
 Crayons = "a8cc5b0e-0ffa-5ad4-8c14-923d3ee1735f"
 DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
 MLStyle = "d8e11817-5142-5d16-987a-aa16d5891078"
 Markdown = "d6f4376e-aef5-505a-96c1-9c027394607a"
+OrderedCollections = "bac558e1-5e72-5ebc-8fee-abe8a469f55d"
 Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
 Reexport = "189a3867-3050-52da-a836-e630ba90ab69"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"

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
+```

docs/src/examples/springs.md

@@ -0,0 +1,5 @@
+# Composition of resource sharers
+
+```julia
+
+```

docs/src/nonstdlib/resource_sharers.md

@@ -0,0 +1,9 @@
+# Resource Sharers
+
+```@docs
+GATlab.NonStdlib.ResourceSharers.Rhizome
+GATlab.NonStdlib.ResourceSharers.ResourceSharer
+GATlab.NonStdlib.ResourceSharers.Variable
+GATlab.NonStdlib.ResourceSharers.PortVariable
+GATlab.NonStdlib.ResourceSharers.ocompose
+```

dynamics.md

@@ -0,0 +1,111 @@
+# The Road to Dynamical Systems
+
+## Basic steps
+
+- [x] Tuple types
+- [-] Symbolic functions
+    Data type:
+
+    ```julia
+    struct AlgebraicFunction
+        theory::GAT
+        args::TypeScope
+        ret::AlgType
+        body::AlgTerm
+    end
+    ```
+
+    Affordances:
+    - [x] DSL for writing down functions, composing, etc.
+    - [ ] A function `tcompose(t::Dtry{AlgebraicFunction})::AlgebraicFunction`, implementing the Dtry-algebra structure on morphisms
+    - [ ] Interpret/compile a symbolic function into a real function
+    - [ ] Serialize symbolic functions
+- [ ] Compilation
+- [ ] Serialization
+
+## Lens-based dynamical systems
+
+- [ ] Arenas
+    Sketch:
+    ```julia
+    struct Arena
+        in::AlgType
+        out::AlgType
+    end
+    ```
+
+    Affordances:
+    - A function `tcompose(arena::Dtry{Arena})::Arena`, implementing the Dtry-algebra structure on objects
+- [ ] Multilenses
+    Sketch:
+    ```julia
+    struct MultiLens
+        inner_boxes::Dtry{Arena}
+        outer_box::Arena
+        # used for namespacing `params` in composition, must not overlap with `inner_boxes`
+        name::Symbol 
+        params::AlgType
+        # (params, tcompose(inner_boxes[...].out)) -> outer_box.out
+        output::AlgebraicFunction
+        # (params, tcompose(inner_boxes[...].out), outer_box.in) -> tcompose(inner_boxes[...].in)
+        update::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - A function `ocompose(l::MultiLens, args::Dtry{MultiLens})::MultiLens` implementing the Dtry-multicategory structure
+- [ ] Systems
+    Sketch:
+    ```julia
+    struct System
+        interface::Arena
+        state::AlgType
+        params::AlgType
+        # (params, state) -> interface.out
+        output::AlgebraicFunction
+        # (params, state, interface.in) -> state
+        input::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - A function `oapply(l::MultiLens, args::Dtry{System})::System` implementing the action of the Dtry-multicategory of multilenses on systems.
+
+## Resource sharers
+
+- [ ] Interfaces
+- [ ] Rhizomes (epi-mono uwds)
+    ```julia
+    struct VariableType
+        type::AlgType
+        exposed::Bool
+    end
+
+    struct Rhizome
+        boxes::Dtry{Interface}
+        junctions::Dtry{VariableType}
+        mapping::Dict{DtryVar, DtryVar}
+    end
+    ```
+
+    Affordances:
+    - `ocompose(r::Rhizome, rs::Dtry{Rhizome})::Rhizome`
+
+    In `ocompose`, the names of the junctions in the top-level rhizome dominate.
+- [ ] Systems
+    ```julia
+    struct ResourceSharer
+        variables::Dtry{VariableType}
+        params::AlgType
+        output::AlgType
+        # (params, state) -> state
+        update::AlgebraicFunction
+        # (params, state) -> output
+        readout::AlgebraicFunction
+    end
+    ```
+
+    Affordances:
+    - `oapply(r::Rhizome, sharers::Dtry{ResourceSharer})::ResourceSharer`
+
+    In `oapply`, variables get renamed to the junctions that they are attached to.

src/models/ModelInterface.jl

@@ -644,12 +644,12 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
   _x = gensym("val")
 
   # Map CODOM sorts to whereparam symbols
-  whereparamdict = OrderedDict(s=>gensym(s.head.name) for s in sorts(codom_theory))
+  whereparamdict = OrderedDict(s=>gensym(headof(s).name) for s in sorts(codom_theory))
   # New model is parameterized by these types
   whereparams = collect(values(whereparamdict))
   # Julia types of domain sorts determined by theorymap 
   jltype_by_sort = Dict(map(sorts(dom_theory)) do v
-    v => whereparamdict[AlgSort(tmap(v.method).val)]
+    v => whereparamdict[AlgSort(tmap(methodof(v)).val)]
   end)
 
   # Create input for instance_code
@@ -758,13 +758,9 @@ function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, migrat
   b = bodyof(t)
   if GATs.isvariable(t)
     nameof(b)
-  elseif  GATs.isdot(t)
+  elseif GATs.isdot(t)
     impl = to_call_impl(b.body, theory, mod, migrate)
-    if isnamed(b.head)
-      Expr(:., impl, QuoteNode(nameof(b.head)))
-    else 
-      Expr(:ref, impl, getlid(b.head).val)
-    end
+    Expr(:., impl, QuoteNode(b.head))
   else
     args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
     name = nameof(headof(b))

src/models/SymbolicModels.jl

@@ -328,13 +328,13 @@ end
 
 function internal_accessors(theory::GAT)
   map(theory.sorts) do sort
-    typecon = getvalue(theory[sort.method])
-    map(collect(pairs(theory.accessors[sort.method]))) do (i, acc)
+    typecon = getvalue(theory[methodof(sort)])
+    map(collect(pairs(theory.accessors[methodof(sort)]))) do (i, acc)
       accessor = getvalue(theory[acc])
       return_type = getvalue(typecon[typecon.args[i]])
       JuliaFunction(
         name=esc(nameof(getdecl(accessor))),
-        args=[:(x::$(esc(nameof(sort.head))))],
+        args=[:(x::$(esc(nameof(sort))))],
         return_type = typename(theory, return_type),
         impl=:(x.type_args[$i])
       )
@@ -415,11 +415,11 @@ function symbolic_instance_methods(
   type_con_funs = []
   accessors_funs = []
   for sort in sorts(theory)
-    type_con = getvalue(theory[sort.method])
-    symgen = symbolic_generator(theorymodule, syntaxname, sort.method, type_con, theory)
+    type_con = getvalue(theory[methodof(sort)])
+    symgen = symbolic_generator(theorymodule, syntaxname, methodof(sort), type_con, theory)
     push!(type_con_funs, symgen)
     for binding in argsof(type_con)
-      push!(accessors_funs, symbolic_accessor(theorymodule, theory, syntaxname, sort.method, binding))
+      push!(accessors_funs, symbolic_accessor(theorymodule, theory, syntaxname, methodof(sort), binding))
     end
   end
 
@@ -614,7 +614,7 @@ function parse_json_sexpr(syntax_module::Module, sexpr;
   theory = theory_module.Meta.theory
   type_lens = Dict(
     nameof(getdecl(getvalue(binding))) => length(getvalue(binding).args)
-    for binding in [theory[sort.method] for sort in sorts(theory)]
+    for binding in [theory[methodof(sort)] for sort in sorts(theory)]
   )
 
   function parse_impl(sexpr::Vector, ::Type{Val{:expr}})