-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Documenter.jl
committed
Sep 21, 2023
1 parent
b4d58e9
commit 1c6d8e2
Showing
8 changed files
with
12 additions
and
12 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
{"documenter":{"julia_version":"1.9.3","generation_timestamp":"2023-09-20T23:59:28","documenter_version":"1.0.1"}} | ||
{"documenter":{"julia_version":"1.9.3","generation_timestamp":"2023-09-21T00:14:10","documenter_version":"1.0.1"}} |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
<!DOCTYPE html> | ||
<html lang="en"><head><meta charset="UTF-8"/><meta name="viewport" content="width=device-width, initial-scale=1.0"/><title>Model families · GATlab.jl</title><meta name="title" content="Model families · GATlab.jl"/><meta property="og:title" content="Model families · GATlab.jl"/><meta property="twitter:title" content="Model families · GATlab.jl"/><meta name="description" content="Documentation for GATlab.jl."/><meta property="og:description" content="Documentation for GATlab.jl."/><meta property="twitter:description" content="Documentation for GATlab.jl."/><script data-outdated-warner src="../../assets/warner.js"></script><link href="https://cdnjs.cloudflare.com/ajax/libs/lato-font/3.0.0/css/lato-font.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/juliamono/0.050/juliamono.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.2/css/fontawesome.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.2/css/solid.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.2/css/brands.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.16.8/katex.min.css" rel="stylesheet" type="text/css"/><script>documenterBaseURL="../.."</script><script src="https://cdnjs.cloudflare.com/ajax/libs/require.js/2.3.6/require.min.js" data-main="../../assets/documenter.js"></script><script src="../../search_index.js"></script><script src="../../siteinfo.js"></script><script src="../../../versions.js"></script><link class="docs-theme-link" rel="stylesheet" type="text/css" href="../../assets/themes/documenter-dark.css" data-theme-name="documenter-dark" data-theme-primary-dark/><link class="docs-theme-link" rel="stylesheet" type="text/css" href="../../assets/themes/documenter-light.css" data-theme-name="documenter-light" data-theme-primary/><script src="../../assets/themeswap.js"></script></head><body><div id="documenter"><nav class="docs-sidebar"><div class="docs-package-name"><span class="docs-autofit"><a href="../../">GATlab.jl</a></span></div><button class="docs-search-query input is-rounded is-small is-clickable my-2 mx-auto py-1 px-2" id="documenter-search-query">Search docs (Ctrl + /)</button><ul class="docs-menu"><li><a class="tocitem" href="../../">GATlab.jl</a></li><li><span class="tocitem">Concepts</span><ul><li><a class="tocitem" href="../overview/">For Catlab users</a></li><li><a class="tocitem" href="../theories/">Theories</a></li><li class="is-active"><a class="tocitem" href>Model families</a></li></ul></li><li><a class="tocitem" href="../../api/">Library Reference</a></li><li><a class="tocitem" href="../../stdlib/">Standard Library</a></li></ul><div class="docs-version-selector field has-addons"><div class="control"><span class="docs-label button is-static is-size-7">Version</span></div><div class="docs-selector control is-expanded"><div class="select is-fullwidth is-size-7"><select id="documenter-version-selector"></select></div></div></div></nav><div class="docs-main"><header class="docs-navbar"><a class="docs-sidebar-button docs-navbar-link fa-solid fa-bars is-hidden-desktop" id="documenter-sidebar-button" href="#"></a><nav class="breadcrumb"><ul class="is-hidden-mobile"><li><a class="is-disabled">Concepts</a></li><li class="is-active"><a href>Model families</a></li></ul><ul class="is-hidden-tablet"><li class="is-active"><a href>Model families</a></li></ul></nav><div class="docs-right"><a class="docs-navbar-link" href="https://github.com/AlgebraicJulia/GATlab.jl" title="View the repository on GitHub"><span class="docs-icon fa-brands"></span><span class="docs-label is-hidden-touch">GitHub</span></a><a class="docs-navbar-link" href="https://github.com/AlgebraicJulia/GATlab.jl/blob/main/docs/src/concepts/models.md" title="Edit source on GitHub"><span class="docs-icon fa-solid"></span></a><a class="docs-settings-button docs-navbar-link fa-solid fa-gear" id="documenter-settings-button" href="#" title="Settings"></a><a class="docs-article-toggle-button fa-solid fa-chevron-up" id="documenter-article-toggle-button" href="javascript:;" title="Collapse all docstrings"></a></div></header><article class="content" id="documenter-page"><h1 id="Model-families"><a class="docs-heading-anchor" href="#Model-families">Model families</a><a id="Model-families-1"></a><a class="docs-heading-anchor-permalink" href="#Model-families" title="Permalink"></a></h1><p>The semantics part of GATlab is the <em>model family</em> infrastructure.</p><p>Given a theory, one can declare a model family for that theory. This consists of the following.</p><ol><li><p>A struct <code>T</code>. Each value of the struct is a <em>model</em> of the theory. The struct subtypes <code>Model{Th, Tuple{Ts...}}</code>. <code>Th</code> is the theory that the struct is a model family for, and <code>Ts</code> specifies types for each of the type constructors in <code>Theory</code>.</p></li><li><p>For each type constructor <code>i</code> in <code>Theory</code>, an overload of <code>checkvalidity</code> of the form</p><pre><code class="language-julia hljs">checkvalidity(m::T, ::TypCon{i}, args..., val) = ...</code></pre><p>This checks that <code>val</code> is a valid instance of <code>i</code> applied to <code>args...</code>, assuming that <code>args...</code> have been previously checked to be valid.</p><p>This can then be applied using, for instance</p><pre><code class="language-julia hljs">checkvalidity(m, Category.Hom, x, y, f)</code></pre><p>using the singleton structs defined in <a href="../theories/#Theories">Theories</a></p></li><li><p>For each term constructor <code>i</code> in <code>Theory</code>, an overload of <code>ap</code> of the form</p><pre><code class="language-julia hljs">ap(m::T, ::TrmCon{i}, args...) = ...</code></pre><p>Here <code>args...</code> is to be interpreted as elements of the full context of the term constructor, not just the direct arguments of the term constructor itself. The reason for this is that the implementation of <code>ap</code> might need the data of, say, the domain and codomain of morphisms in order to compose them, and because we have an indexed form of dependent types, this information is not available from the morphism data itself.</p></li></ol></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../theories/">« Theories</a><a class="docs-footer-nextpage" href="../../api/">Library Reference »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="auto">Automatic (OS)</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.0.1 on <span class="colophon-date" title="Wednesday 20 September 2023 23:59">Wednesday 20 September 2023</span>. Using Julia version 1.9.3.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html> | ||
<html lang="en"><head><meta charset="UTF-8"/><meta name="viewport" content="width=device-width, initial-scale=1.0"/><title>Model families · GATlab.jl</title><meta name="title" content="Model families · GATlab.jl"/><meta property="og:title" content="Model families · GATlab.jl"/><meta property="twitter:title" content="Model families · GATlab.jl"/><meta name="description" content="Documentation for GATlab.jl."/><meta property="og:description" content="Documentation for GATlab.jl."/><meta property="twitter:description" content="Documentation for GATlab.jl."/><script data-outdated-warner src="../../assets/warner.js"></script><link href="https://cdnjs.cloudflare.com/ajax/libs/lato-font/3.0.0/css/lato-font.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/juliamono/0.050/juliamono.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.2/css/fontawesome.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.2/css/solid.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.2/css/brands.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.16.8/katex.min.css" rel="stylesheet" type="text/css"/><script>documenterBaseURL="../.."</script><script src="https://cdnjs.cloudflare.com/ajax/libs/require.js/2.3.6/require.min.js" data-main="../../assets/documenter.js"></script><script src="../../search_index.js"></script><script src="../../siteinfo.js"></script><script src="../../../versions.js"></script><link class="docs-theme-link" rel="stylesheet" type="text/css" href="../../assets/themes/documenter-dark.css" data-theme-name="documenter-dark" data-theme-primary-dark/><link class="docs-theme-link" rel="stylesheet" type="text/css" href="../../assets/themes/documenter-light.css" data-theme-name="documenter-light" data-theme-primary/><script src="../../assets/themeswap.js"></script></head><body><div id="documenter"><nav class="docs-sidebar"><div class="docs-package-name"><span class="docs-autofit"><a href="../../">GATlab.jl</a></span></div><button class="docs-search-query input is-rounded is-small is-clickable my-2 mx-auto py-1 px-2" id="documenter-search-query">Search docs (Ctrl + /)</button><ul class="docs-menu"><li><a class="tocitem" href="../../">GATlab.jl</a></li><li><span class="tocitem">Concepts</span><ul><li><a class="tocitem" href="../overview/">For Catlab users</a></li><li><a class="tocitem" href="../theories/">Theories</a></li><li class="is-active"><a class="tocitem" href>Model families</a></li></ul></li><li><a class="tocitem" href="../../api/">Library Reference</a></li><li><a class="tocitem" href="../../stdlib/">Standard Library</a></li></ul><div class="docs-version-selector field has-addons"><div class="control"><span class="docs-label button is-static is-size-7">Version</span></div><div class="docs-selector control is-expanded"><div class="select is-fullwidth is-size-7"><select id="documenter-version-selector"></select></div></div></div></nav><div class="docs-main"><header class="docs-navbar"><a class="docs-sidebar-button docs-navbar-link fa-solid fa-bars is-hidden-desktop" id="documenter-sidebar-button" href="#"></a><nav class="breadcrumb"><ul class="is-hidden-mobile"><li><a class="is-disabled">Concepts</a></li><li class="is-active"><a href>Model families</a></li></ul><ul class="is-hidden-tablet"><li class="is-active"><a href>Model families</a></li></ul></nav><div class="docs-right"><a class="docs-navbar-link" href="https://github.com/AlgebraicJulia/GATlab.jl" title="View the repository on GitHub"><span class="docs-icon fa-brands"></span><span class="docs-label is-hidden-touch">GitHub</span></a><a class="docs-navbar-link" href="https://github.com/AlgebraicJulia/GATlab.jl/blob/main/docs/src/concepts/models.md" title="Edit source on GitHub"><span class="docs-icon fa-solid"></span></a><a class="docs-settings-button docs-navbar-link fa-solid fa-gear" id="documenter-settings-button" href="#" title="Settings"></a><a class="docs-article-toggle-button fa-solid fa-chevron-up" id="documenter-article-toggle-button" href="javascript:;" title="Collapse all docstrings"></a></div></header><article class="content" id="documenter-page"><h1 id="Model-families"><a class="docs-heading-anchor" href="#Model-families">Model families</a><a id="Model-families-1"></a><a class="docs-heading-anchor-permalink" href="#Model-families" title="Permalink"></a></h1><p>The semantics part of GATlab is the <em>model family</em> infrastructure.</p><p>Given a theory, one can declare a model family for that theory. This consists of the following.</p><ol><li><p>A struct <code>T</code>. Each value of the struct is a <em>model</em> of the theory. The struct subtypes <code>Model{Th, Tuple{Ts...}}</code>. <code>Th</code> is the theory that the struct is a model family for, and <code>Ts</code> specifies types for each of the type constructors in <code>Theory</code>.</p></li><li><p>For each type constructor <code>i</code> in <code>Theory</code>, an overload of <code>checkvalidity</code> of the form</p><pre><code class="language-julia hljs">checkvalidity(m::T, ::TypCon{i}, args..., val) = ...</code></pre><p>This checks that <code>val</code> is a valid instance of <code>i</code> applied to <code>args...</code>, assuming that <code>args...</code> have been previously checked to be valid.</p><p>This can then be applied using, for instance</p><pre><code class="language-julia hljs">checkvalidity(m, Category.Hom, x, y, f)</code></pre><p>using the singleton structs defined in <a href="../theories/#Theories">Theories</a></p></li><li><p>For each term constructor <code>i</code> in <code>Theory</code>, an overload of <code>ap</code> of the form</p><pre><code class="language-julia hljs">ap(m::T, ::TrmCon{i}, args...) = ...</code></pre><p>Here <code>args...</code> is to be interpreted as elements of the full context of the term constructor, not just the direct arguments of the term constructor itself. The reason for this is that the implementation of <code>ap</code> might need the data of, say, the domain and codomain of morphisms in order to compose them, and because we have an indexed form of dependent types, this information is not available from the morphism data itself.</p></li></ol></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../theories/">« Theories</a><a class="docs-footer-nextpage" href="../../api/">Library Reference »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="auto">Automatic (OS)</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.0.1 on <span class="colophon-date" title="Thursday 21 September 2023 00:14">Thursday 21 September 2023</span>. Using Julia version 1.9.3.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html> |
Oops, something went wrong.