#+TITLE: The home of the L4 DSL
#+STARTUP: content

Hi! If you /aren't/ a L4 internal developer, or if you aren't already familiar with L4, you might want to look at [[https://docs.google.com/spreadsheets/d/1leBCZhgDsn-Abg2H_OINGGv-8Gpf9mzuX1RR56v0Sss/edit?usp=sharing][LegalSS]] first. This documentation is primarily intended for core devs -- programmers working on the compiler toolchain and IDE for L4 itself.

* L4 Language Family

The L4 language family currently comprises:

** a compiler for the developer-friendly /Natural L4/ syntax, in the directory ~lib/dsl/haskell/natural4~

The syntax uses a plethora of English keywords arranged in a sentence-like structure, similar to languages like SQL.

The current IDE is a spreadsheet environment. In the future, we may add support for text-mode IDEs if there is demand.

The compiler consists of a parser, interpreter, and transpiler to a variety of downstream targets.

** a semantically rigorous /Core L4/ syntax which lives in the repo ~smucclaw/baby-l4~

Please see https://github.com/smucclaw/baby-l4 and the [[https://github.com/smucclaw/complaw/blob/generated-pdf/Publications/Documentation/L4Language/main.pdf][L4 Language Report]].

* Transpilation Targets

L4 transpiles to the following targets. An L4 "program" can be exported to these formats:

| Target                       | Purpose                    | Status (Dec 2022) |
|------------------------------+----------------------------+-------------------|
| Purescript                   | decision logic             | stable            |
| Haskell                      | expose AST & IR internals  | stable            |
| Org-Mode                     | expose AST & IR internals  | stable            |
| Epilog                       | decision logic             | early release     |
| ASP (Answer Set Programming) | abduction                  | early release     |
| Markdown                     | human readability          | early release     |
| Petri Nets                   | workflows and verification | early release     |
| Typescript                   | data schema as class types | early release     |
| JSON                         | instance data values       | early release     |
| Prolog                       | decision logic             | in progress       |
| Pro B                        | formal verification        | in progress       |
| DMN                          | decision logic             | in progress       |
| mCRL2                        | formal verification        | evaluation        |
| Uppaal                       | formal verification        | evaluation        |
| Tapaal                       | formal verification        | evaluation        |
| BPMN                         | workflows for execution    | on roadmap        |
| DocAssemble                  | document assembly          | on roadmap        |
| Catala                       | decision logic             | on roadmap        |
| Blawx                        | decision logic, ontology   | on roadmap        |
| MorphIR                      | decision logic, ontology   | on roadmap        |
| Word                         | human readability          | on roadmap        |
| PDF                          | human readability, signing | on roadmap        |
| LegalDocumentML              | standards-based interop    | on roadmap        |
| Alloy                        | formal verification        | on roadmap        |

After a successful run of the ~natural4~ interpreter you will find exports udner the ~workdir~ directory.

* Natural L4

** Spreadsheet Interface

[[https://docs.google.com/spreadsheets/d/1leBCZhgDsn-Abg2H_OINGGv-8Gpf9mzuX1RR56v0Sss/edit?usp=sharing][LegalSS]] contains examples of L4 "source code".

*L4 developers* -- the /legal engineers/ working with L4 source code to build legal infrastructure and applications -- are supported by a sidebar in the spreadsheet that displays warnings, errors, and exported files.

That sidebar is generated by the L4 toolchain, which makes sense of L4 source code from the spreadsheet.

That L4 toolchain is, in turn, supported by the L4 *internal developer* community. We also refer to internal developers as *core developers*.

Operating instructions for the parts of the toolchain that bring up a web-based development environment (Google Sheets) and web application (end-user-facing Vue app) are available at https://docs.google.com/document/d/1EvyiQhSgapumBRt9UloRpwiRcgVhF-m65FVdAz3chfs/edit

The rest of this documentation introduces the logic and semantics of natural4, its internal data structures, and its surface syntax.

Along the way it discusses the internal structure of our compiler codebase.

** Compiler Toolchain

*** Prerequisites

1. Clone this repository.
2. (/For Nix users only:/) You will have your own setup universe which we won't go into here, but if you use Nix you already probably have Haskell well in hand. You are using Nix if your ~$PATH~ contains ~$HOME/.nix-profile/bin/~
3. If you're not a Nix user, install [[https://www.haskell.org/ghcup/install/][GHCup]].
4. After installing GHCup, your ~$PATH~ should contain ~$HOME/.ghcup/bin/~ 
5. Use GHCup to install [[https://docs.haskellstack.org/en/stable/README/][Stack]] by running ~ghcup tui~.
6. After installing Stack, your ~$PATH~ should contain ~$HOME/.local/bin/~ 
7. /For [[https://betterprogramming.pub/haskell-vs-code-setup-in-2021-6267cc991551][VS Code]] and [[https://github.com/emacs-lsp/lsp-haskell][emacs]] users:/ use GHCup to install HLS by manually running

   #+begin_src shell
     ghcup compile hls --git-ref master --ghc 9.2.5 --cabal-update
   #+end_src
   
8. /For Emacs users:/ proceed to the instructions at [[https://github.com/emacs-lsp/lsp-haskell][lsp-haskell]].

9. /For VS Code users:/ proceed to the instructions at [[https://github.com/haskell/vscode-haskell][vscode-haskell]].

*** Installation

After your Haskell setup is working well enough to run ~stack~,

#+begin_example
  src/smucclaw/dsl$ cd lib/haskell/natural4
  natural4$ stack test
#+end_example

It may take some time to compile ~ghc~, plus a whole raft of dependencies.

**** Confirming the install

A number of sample CSV inputs can be found in the ~test/examples~ directory.
(The following should be run from the ~lib/haskell/natural4~ subdirectory.)

#+begin_src
  natural4$ stack run -- --workdir=workdir --toasp --tomd test/examples/mustsing-latest.csv
#+end_src

This should compile the ~l4~ parser, and produce a bunch of output under the ~workdir/~ directory.

You can browse that output using any text editor or filesystem explorer.

**** Install the binary

If you're happy with the above output,

#+begin_src bash
  natural4$ stack install
#+end_src

will put a ~natural4-exe~ somewhere in your ~$HOME/.local/bin~ directory. After the above installation procedure, that directory should appear in your ~$PATH~.

**** Generate Haddock documentation

#+begin_src shell
natural4$ stack haddock
#+end_src

will generate Haddock documentation from the Haskell source. The output takes the form of ~.html~ files; pay attention to the last dozen lines or so of the ~stack haddock~ run output to get the actual pathnames.

*** Downloading the Spreadsheet

The typical user drafts an L4 program in a spreadsheet.

That program can be downloaded as a CSV, which this toolchain consumes.

Example: Go to the "Case Study: PDPA DBNO" tab in [[https://docs.google.com/spreadsheets/d/1leBCZhgDsn-Abg2H_OINGGv-8Gpf9mzuX1RR56v0Sss/edit?usp=sharing][LegalSS]], and click ~File/ Download / as CSV~.

The downloaded filename will probably be quite long. For the sake of concision, we will call it ~pdpadbno.csv~

Is there some other way to obtain the same CSV using only the command line? Yes. If you just want to use the stock CSV, you can do

#+begin_example
  wget -O pdpadbno.csv 'https://docs.google.com/spreadsheets/d/e/2PACX-1vSbknuGFkvvk_Pv9e97iDW9BInxd-Cj27-xC8d_SwveP1PxERV7ZmiAIU7PWXas2CEMH2bl8PyyD6X3/pub?gid=0&single=true&output=csv'
#+end_example

Otherwise, if you want to make your own changes and get the resulting spreadsheet in CSV form, you should make a copy (File > Make a Copy in Google Sheets), if you haven't already, and make your changes in that copy. Then, to get the URL for ~wget~, click on ~File / Share / Publish to web~, choose the appropriate tab under 'Link' and select ~CSV~ as the output format under 'Embed', and finally click on Publish. You will then be presented with a URL; this URL is what should replace that in the ~wget~ eaxmple block above.

Is this more or less the same file as what's already present in ~test/casestudypdpadbno-latest.csv~? Yes, it is. But now you know how to get a copy fresh from any edits you make.

*** Generating the Transpilation Targets in the Workdir

The job of a compiler / transpiler / parser / interpreter toolchain is to transform user code to some useful target representation.

We'll first want to output all the target representations to disk. To do that, navigate to ~dsl/lib/haskell/natural4~ and run

#+begin_example
$ stack run -- --workdir=workdir --toasp --tomd pdpadbno.csv
#+end_example

The result will be something like:

#+begin_example
$ tree workdir     
workdir
└── no-uuid
    ├── aasvg
    │   ├── 2022-12-01T08:56:17.579Z
    │   │   ├── Assessment-anyall.hs
    │   │   ├── Assessment-anyall.json
    │   │   ├── Assessment-full.svg
    │   │   ├── Assessment-qjson.json
    │   │   ├── Assessment-qtree.hs
    │   │   ├── Assessment-tiny.svg
    │   │   ├── Notify_Individuals-N-anyall.hs
    │   │   ├── Notify_Individuals-N-anyall.json
    │   │   ├── Notify_Individuals-N-full.svg
    │   │   ├── Notify_Individuals-N-qjson.json
    │   │   ├── Notify_Individuals-N-qtree.hs
    │   │   ├── Notify_Individuals-N-tiny.svg
    │   │   └── index.html
    │   ├── 2022-12-07T10:01:07.764Z
    │   │   ├── Assessment-anyall.hs
    │   │   ├── Assessment-anyall.json
    │   │   ├── Assessment-full.svg
    │   │   ├── Assessment-qjson.json
    │   │   ├── Assessment-qtree.hs
    │   │   ├── Assessment-tiny.svg
    │   │   ├── Notify_Individuals-N-anyall.hs
    │   │   ├── Notify_Individuals-N-anyall.json
    │   │   ├── Notify_Individuals-N-full.svg
    │   │   ├── Notify_Individuals-N-qjson.json
    │   │   ├── Notify_Individuals-N-qtree.hs
    │   │   ├── Notify_Individuals-N-tiny.svg
    │   │   └── index.html
    │   └── LATEST -> 2022-12-07T10:01:07.764Z
    ├── asp
    │   ├── 2022-12-01T08:55:44.907Z.lp
    │   └── 2022-12-07T09:35:17.752Z.lp
    ├── babyl4
    │   ├── 2022-12-07T10:01:07.764Z.l4
    │   └── LATEST.l4 -> 2022-12-07T10:01:07.764Z.l4
    ├── corel4
    │   ├── 2022-12-07T10:01:07.764Z.l4
    │   └── LATEST.l4 -> 2022-12-07T10:01:07.764Z.l4
    ├── grounds
    │   ├── 2022-12-07T10:01:07.764Z.txt
    │   └── LATEST.txt -> 2022-12-07T10:01:07.764Z.txt
    ├── json
    │   ├── 2022-12-07T10:01:07.764Z.json
    │   └── LATEST.json -> 2022-12-07T10:01:07.764Z.json
    ├── native
    │   ├── 2022-12-07T10:01:07.764Z.hs
    │   └── LATEST.hs -> 2022-12-07T10:01:07.764Z.hs
    ├── natlang
    │   ├── 2022-12-07T10:01:07.764Z.txt
    │   └── LATEST.txt -> 2022-12-07T10:01:07.764Z.txt
    ├── org
    │   ├── 2022-12-07T10:01:07.764Z.org
    │   └── LATEST.org -> 2022-12-07T10:01:07.764Z.org
    ├── petri
    │   ├── 2022-12-07T10:01:07.764Z.dot
    │   └── LATEST.dot -> 2022-12-07T10:01:07.764Z.dot
    ├── prolog
    │   ├── 2022-12-07T10:01:07.764Z.pl
    │   └── LATEST.pl -> 2022-12-07T10:01:07.764Z.pl
    ├── purs
    │   ├── 2022-12-07T10:01:07.764Z.purs
    │   └── LATEST.purs -> 2022-12-07T10:01:07.764Z.purs
    └── ts
        ├── 2022-12-07T10:01:07.764Z.ts
        └── LATEST.ts -> 2022-12-07T10:01:07.764Z.ts
#+end_example

These outputs correspond to the transpilation targets enumerated above, and can be further transformed if necessary before being put in front of the end-user's eyeballs.

The above run disabled two of the output targets because they are still works in progress: ~--toasp --tomd~

You can remove those options from the command line to enable those output channels, but they may not work.

*** The AST and Intermediate Representations

The initial AST produced by the ~natural4~ parser is found in the ~native/~ output directory as ~LATEST.hs~.

Subsequently, that AST is transformed by the Interpreter module to a data structure output to the ~org/~ output directory as ~LATEST.org~.

From there, it is further transformed to an intermediate representation called CoreL4, also known as Baby L4. That transformation is currently under renovation: there is a plaintext code generator which is slightly older, and a slightly newer initiative to perform direct in-memory conversion from one set of types to another. In our defense, this high-level/low-level dichotomy is also present in GHC; and the old/new pair of transformation pathways [[https://youtube.com/clip/UgkxZsC3tlHNvw3wZWEMizZYu9HXnAWWeMgS][also appears in GHC's history]].

**** native: a Haskell data structure

This is the simplest output mode. It confirms the parse happened as intended.

You should see a ~LATEST.hs~ file under the ~workdir/*/native/~ output directory. You can get just that output by running

#+begin_src
  natural4$ stack run -- --only native test/casestudypdpadbno-latest.csv
#+end_src

This should produce a screenful of output. If all went well, the output will be in the format of a Haskell data structure, containing the rules that have been parsed. It will look something like this:

#+begin_src haskell
    [ Regulative
        { every = "Person"
        , who = Just
            ( All
                ( Pre "Who" )
                [ Leaf "walks"
                , Any
                    ( Pre "any of:" )
                    [ Leaf "eats"
                    , Leaf "drinks"
                    ]
                ]
            )
        , cond = Nothing
        , deontic = DMust
        , action =
            ( "sing"
            , []
            )
        , temporal = Nothing
        , hence = Nothing
        , lest = Nothing
        , rlabel = Nothing
        , lsource = Nothing
        , srcref = Nothing
        , upon = Nothing
        , given = Nothing
        }
    ]
    [ Regulative
        { every = "Person"
        , who = Just
            ( All
                ( Pre "Who" )
                [ Leaf "walks"
                , Any
                    ( Pre "any of:" )
                    [ Leaf "eats"
                    , Leaf "drinks"
                    ]
                ]
            )
        , cond = Nothing
        , deontic = DMust
        , action =
            ( "sing"
            , []
            )
        , temporal = Nothing
        , hence = Nothing
        , lest = Nothing
        , rlabel = Nothing
        , lsource = Nothing
        , srcref = Nothing
        , upon = Nothing
        , given = Nothing
        }
    ]
    [ Constitutive
        { term = "The rule-level checkbox is checked"
        , cond = Just
            ( Any
                ( Pre "any of:" )
                [ Leaf "the conditions do not hold"
                , All
                    ( Pre "all of:" )
                    [ Leaf "the conditions do hold"
                    , Leaf "the action is satisfied"
                    ]
                ]
            )
        , rlabel = Nothing
        , lsource = Nothing
        , srcref = Nothing
        }
    ]
    [ Regulative
        { every = "Person"
        , who = Just
            ( Leaf "Qualifies" )
        , cond = Nothing
        , deontic = DMust
        , action =
            ( "sing"
            , []
            )
        , temporal = Nothing
        , hence = Nothing
        , lest = Nothing
        , rlabel = Nothing
        , lsource = Nothing
        , srcref = Nothing
        , upon = Nothing
        , given = Nothing
        }
    , Constitutive
        { term = "Qualifies"
        , cond = Just
            ( All
                ( Pre "all of:" )
                [ Leaf "walks"
                , Any
                    ( Pre "any of:" )
                    [ Leaf "eats"
                    , Leaf "drinks"
                    ]
                ]
            )
        , rlabel = Nothing
        , lsource = Nothing
        , srcref = Nothing
        }
    ]
#+end_src

The semantics of this data structure will be outlined below. This outline complements other documentation:
- Haddock documentation for the LS.* modules (produced by the [[*Generate Haddock documentation]] procedure above
- the [[https://docs.google.com/spreadsheets/d/1leBCZhgDsn-Abg2H_OINGGv-8Gpf9mzuX1RR56v0Sss/edit?pli=1#gid=1732775477][L4 Manual tab of the LegalSS]]
- the [[https://docs.google.com/document/d/1EvyiQhSgapumBRt9UloRpwiRcgVhF-m65FVdAz3chfs/edit#][operating instructions Google Doc]]

The following documentation focuses on the parsing and interpretation aspects of the toolchain and the data structures in particular.

**** org: an Org-Mode file showing Interpreter output

The interpreter performs a number of transformations. For your convenience it writes each stage of those transformations out to the ~org/LATEST.org~ output file, in a format compatible with org-mode.

If you are an Emacs user, you have native support for org-mode built in; opening the ~LATEST.org~ output file should automatically load ~org-mode~.

If you are a VS Code user you will need to install the relevant extensions.

**** baby-l4 / core-l4

This is a formally rigorous language representing decision logic, ontology, and workflow rules.

This is where some of the type-checking and type inference occurs.

Some of the downstream targets are produced by transpilers which proceed from CoreL4.

For details, please see https://github.com/smucclaw/baby-l4 and the [[https://github.com/smucclaw/complaw/blob/generated-pdf/Publications/Documentation/L4Language/main.pdf][L4 Language Report]].

*** Transpilation Targets In Detail

This section is still under construction. It will give a short explanation of each transpilation target and its intended use.

**** prolog

Those elements of L4 which correspond to first-order logic can be transpiled to a Prolog-like syntax.

The inspiration is [[https://www.doc.ic.ac.uk/~rak/papers/British%20Nationality%20Act.pdf][The British Nationality Act as a Logic Program]]. In principle it should be possible to express the British Nationality Act as an L4 program, from which we can extract a Prolog program.

We usually see decision-related reasoning in the context of constitutive rules: an X counts as a Y if Z holds. In the trivial case, an X counts as true if Z holds:

#+begin_src prolog
  constitutiveRule(X) :- Z.

  bna(isBritishCitizen,X) :- bna(isBritishCitizen,Y), parent(Y, X).
#+end_src



The reasoning used is backward-chaining deduction. Given a goal statement, the task is to decide if that goal is true or false. "It depends." What does it depend on? We work through all the dependencies, backtracking, until the goal can be proven true -- or false.

Prolog's other great strength -- abductive reasoning through unification -- does not arise in our current swipl implementation. We do want to use this feature for planning problems, in the future.

Our current transpilation pathway to Prolog actually runs through the CoreL4 language. It is possible that in future we will go direct from Natural4.

Within the Prolog family of targets we differentiate:

***** SWIPL

***** Clingo

***** s(CASP)

**** petri: a Petri Net showing the state diagram

One of the ~workdir~ outputs is a ~Petri~ (workflow) net in GraphViz ~dot~ format. This is like a state diagram.

To convert it to an SVG which can be opened in a web browser, you will need GraphViz installed. Then run

#+begin_src 
  dot -Tsvg workdir/no-uuid/petri/LATEST.dot > workdir/no-uuid/petri/LATEST.svg
#+end_src

It is not exactly a state diagram because things can be in multiple sub-states at once. Petri Nets are good at showing that.

**** aasvg: AnyAll SVG showing the decision logic

**** json: for consumption by other tools such as a web app

**** Purescript

This is consumed by the Vue web application documented in the [[https://docs.google.com/document/d/1EvyiQhSgapumBRt9UloRpwiRcgVhF-m65FVdAz3chfs/edit][Operating Instructions Google Doc]].

If you know Haskell, you will be able to read Purescript.

*** Debugging

Sometimes, a downloaded CSV may not agree with the parser.

If a parse error occurs, you can enable debugging by adding ~--dbug~ to the command line. An alternative way to enable debugging is to set the environment variable ~MP_DEBUG=True~.

Debugging output is super verbose. We process it with the following idiom:

#+begin_src
  filename=casestudypdpadbno-latest; MP_DEBUG=True stack run test/$filename.csv |& bin/debug2org > out/$filename.org
#+end_src

The ~debug2org~ script rewrites the raw debugging output into a format which is more easily viewed in Emacs [[https://orgmode.org/][org-mode]]. Mostly, it's about folding: the parser's output is organized to reflect its attempts to parse various expressions. Most of those parse attempts are "desired failures" and are not of interest; org-mode lets you hide them by pressing ~TAB~.

Making sense of the parser debug output requires some familiarity with programming language theory, with compiler theory, and with the specifics of our L4 parser toolchain.

*** Development Conveniences

This little script (on Mac at least) watches your Downloads folder so every time you Save As CSV it moves the new download over to the ~test/~ directory. Run from home directory. You may need to edit to taste.

#+begin_example
  fswatch -x ~/Downloads/ | perl -nle 'if (my ($fn, $target) = /(Legal(?:SSv| Spreadsheets - )(.*).csv) Created.*Renamed/) { for ($target) { $_ = lc $_; s/[^a-z]//g }; rename (qq(Downloads/$fn), qq(src/smucclaw/dsl/lib/haskell/natural4/test/$target-latest.csv)) && print(qq($fn -> $target)) && system(qq(cd src/smucclaw/dsl/lib/haskell/natural4; teedate=`date +%Y%m%d-%H%M%S`.txt; stack run -- --workdir=workdir test/$target-latest.csv > workdir/no-uuid/\$teedate; ln -sf \$teedate workdir/no-uuid/LATEST.txt; head \$teedate; echo done ))} BEGIN { $|++ }'
#+end_example

We should probably turn this into an actual shell script, not a command-line "one-liner".

** Parser Internals

The parser consumes CSV and produces a list of rules largely corresponding to the input.

Along the way, some "inline" rules are promoted to top-level.

*** Promotion of inline rules to top level

**** TYPICALLY

In some positions, a term can be assigned a default value using the ~TYPICALLY~ keyword.

Such uses result in a top-level rule: ~DefTypically~.

**** MEANS

Suppose we have

#+begin_example
  EVERY Person
    WHO Qualifies
        MEANS walks
          AND    eats
              OR drinks
   MUST sing
#+end_example

(This is from the [[https://docs.google.com/spreadsheets/d/1leBCZhgDsn-Abg2H_OINGGv-8Gpf9mzuX1RR56v0Sss/edit?pli=1#gid=1505307398][Waddington example]].)

This parses to two top-level rules:
1. a regulative rule ~EVERY person WHO Qualifies MUST sing~.
2. a constitutive rule ~Qualifies MEANS walks AND eats OR drinks~.

*** Internal Mechanics

This promotion is accomplished thanks to the Monad Writer context of the Natural L4 Parser.

https://github.com/smucclaw/dsl/blob/main/lib/haskell/natural4/src/LS/Types.hs#L151-L152

** Interpreter Internals

The Interpreter conducts multiple passes over the Parser's AST.

The following passes are on the roadmap for the Interpreter.

*** Entity Model                                                   :stable:

Let's declare as a ~Class~ anything that has attributes and instances.

How do we deal with subclasses, inheritance, and diamonds?

Subclasses are constructed using the ~EXTENDS~ keyword.

~HAS-A~ relationships are dealt with using nesting of the ~HAS~ keyword.

Diamond inheritance is excluded.

*** Statics: rephrase as First-Order Logic                         :stable:

Construct trees of ANDs and ORs. How do we deal with a particular defined term appearing in multiple locations?

E.g. given a shopping cart with both alcohol and cigarettes, a ~LegalCheckout~ may refer to the "subroutine" for ~AgeOfMajority~ twice; do we need to "cache" to result of evaluation, or is that a problem for the runtimes? Perhaps we can assist by at least giving identifiers so the runtime can do the right thing.

The ~AnyAll~ library is responsible for most of this work.

The result of this transformation stage is visible in the ~qaHornsR~ and ~qaHornsT~ functions.

*** Macros                                                         :future:

If the language has support for user-defined macros or other forms of syntactic sugar, evaluate those macros and desugar to canonical form.

*** Type annotations                                           :inProgress:

Filter all instances of ~TypedMulti~ in our AST where the ~snd~ is ~Just~; collect the explicit type annotations.

*** Type inference                                                 :future:

Filter all instances of ~TypedMulti~ in our AST where the ~snd~ is ~Nothing~; attempt type inference based on observations of how the ~fst~ element is used elsewhere. For top marks, Implement Hindley-Milner inference.

This work may be delegated to the Core L4.

Alternatively, we may be able to call GHC as a library.

** Interpretation Requirements for Downstream Transpilation

After the parser succeeds, we have in our hands a list of ~Rules~.

It is now the interpreter's job to think about the Rules, get organized, and prepare for the next step -- transpilation.

The transpilers will be wanting answers to questions like:

*** What is the ontology? What are the entities and relationships?

The DECLARE and DEFINE keywords together construct class and instance definitions.

*** Roadmap for the Interpreter: Some Open Questions

**** Entity Relations

We need to find a way to relate different entities with one another -- an ~Employee~ may have an ~Employer~. In a database, they may be connected explicitly by ~id~ fields or they may be connected implicitly.

In our system, we allow ~DECLARE / HAS~ to nest, so that multiple levels of nesting can be created. This is analogous to records containing other records, and to ~HAS-A~ relationships between classes.

**** Which types were explicit and which were inferred?

The TypedMulti alias looks like this:

#+begin_src haskell
  type KVsPair = (NonEmpty Text.Text, Maybe TypeSig)    --- so really there are multiple Values
  type TypedMulti = KVsPair                             --- | apple | orange | banana | :: | Fruit   |
#+end_src

The ~Maybe TypeSig~ part can be used for both explicitly annotated types and inferred types.

**** What warnings and errors do we produce?

In particular, the interpreter might be able to perform tree-shaking, dead code identification, and identify null pointer references.

It might also be able to identify race conditions. Maybe one transpiler can request to view the output of another transpiler backend, so the formal verification module ends up running first and then the other transpilers read output from that.

**** Can we get a representation of the original program text?

The Parser produces decent source locations, but the transformations performed by the Interpreter may muddy the trail.

**** If not, then for each node in the AST, can we at least get a link back to a source reference in the original program text?

And even beyond -- because in the left column of L4 we have the ~(Act 1.2)~ cells which provide links even farther back to the source legislation.

**** What are the "statics" -- the inference rules?

The interpreter needs to get its head around how all the BoolStructs go together.

Our NLG component, for instance, needs to convert text like ~X gives birth to live young.~ to ~Does X give birth to live young?~

So it will want to know every single "ground term" which we need to ask the user about.

The Shannon/Allen visualizer and the JSON outputters will want to know how those terms fit together: the BoolStructs with their Labels.

The web app interface builder may expect the interpreter to do some kind of reduction/optimization of the questions -- see ROBDD.

**** What are the "dynamics" -- the state transitions?

This is of particular interest to the visualizer that produces a Petri net.

The interpreter needs to get its head around how all the HENCE and LEST blocks connect.

**** Are there any defined terms that weren't actually defined?

We are literally looking at capitalization to determine what's a Defined Term.


** Contract with Transpilers

Each transpiler under ~XPile~ can expect an ~Interpretation~ containing the interpreter's analysis of the rules.

That analysis consists of
- classtable :: of type ~ClsTab~, a table of all the top-level classes declared
- scopetable :: of type ~ScopeTabs~, a table of all the rule scopes defined

That Interpretation also contains
- origrules :: a list of rules (~[Rule]~) as returned by the Parser

*** ClsTab

See Haddock reference.

Classes contain ontological semantics according to the conventional OOP paradigm, excluding diamond inheritance.

Classes can contain other classes, in a ~HAS-A~ relationship, using nested ~HAS~ keywords.

Classes can extend other classes, in an ~IS-A~ relationship, using the ~EXTENDS~ keyword.

*** ScopeTabs

Scopes in L4 are intended to constrain certain definitions, reflecting source text such as

#+begin_quote
  For the purposes of Sections 1 and 2, "work-week" is defined to include half a day on Saturdays, in addition to Mondays through Fridays, but excludes Sundays.

  For the purposes of Sections 3 and 4, "work-week" is defined to exclude Saturdays and Sundays.
#+end_quote

Scopes allow us to represent these kinds of statements.

See Haddock reference.

** Language Reference

See the LegalSS L4 Manual.