Abstract syntax for core L4 concepts.

Files:

• Syntax.hs Declaration of data types (types, classes and instances, modules, expressions, timed automata)
• Exec.hs Execution / evaluation of expresssions
• TaToUppaal.hs Conversion of Timed Automata to the Uppaal XTA format, see https://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Introduction.shtml
• TransL.hs Translation from L4 BNFC to the core abstract syntax. Very incomplete.
• Typing.hs Type checking of abstract syntax.

The file Test.hs is for testing only and can be discarded.

with lexicon

Business -> business_2

wordnet annotations in classes

e.g. class Business (132) {

classes

e.g. class Business...

future version! will have support for More Things!

wordnet annotations deleted from classes

class Business {

We should have a test suite that creates this dashboard. See issue #4.

l4: typ2kind: not yet supported: FunT (ClassT (ClsNm "LegalPractitioner")) (FunT (ClassT (ClsNm "Appointment")) BoolT)
CallStack (from HasCallStack):
  error, called at src/ToGF.hs:43:8 in baby-l4-0.1.0.0-7MSFL28Gv2uEWQACncPSnj:ToGF

Start Uppaal with java -jar uppaal.jar &, then File / Open system. Load a model (*xml) file. The view typically opens on the Editor tab (system definition with several automata). On the Simulator tab, one can execute the system by stepping through a scenario. On the Verifier tab, one finds several “queries” (corresponding to proof obligations). These are contained in the *q file associated with the model file. Select one of the formulas and verify it by clicking on the Check button. In order to obtain a counter-example, select “Options / Diagnostic Trace” and then one of Some / Shortest / Fastest. On the next Check, the counterexample will be loaded into the Simulator.

In Haskell, running writeFile "test_haskell_uppaal.xta" (ta_sys_to_uppaal (TmdAutSys [autA, autB])) produces a textual Uppaal XTA file. The file can in principle be read in by the GUI. As there is no graphical layout information information associated with the file, the elements of the automata are first arranged in an arbitrary fashion. After manually rearranging and storing the model, a .ugi file stores graphic information.

The XTA file can be run (together with a query in a .q file) with shell command verifyta contained in the download bundle, as in bin-Linux/verifyta -t0 test_haskell_uppaal.xta test_haskell_uppaal.q, where test_haskell_uppaal.q is, for example:

E<> AutA.l3 and AutB.l2

A textual trace is then written to standard output.

The goal is for this to work:

stack run l4 l4/mini.l4

and you should (eventually) get this output:

Program [Mapping "is_legal" "legal_1_A",Mapping "Business" "business_1_N"] [] [VarDecl "myNumber" IntT,VarDecl "myBusiness" (ClassT (ClsNm "Business")),VarDecl "is_legal" (FunT (ClassT (ClsNm "Business")) BoolT)] [] []

PAtom (AKind Nat (IVar (VString "myNumber")))
myNumber is a number
myNumber är ett tal
PAtom (AKind (KInd (IVarN Business)) (IVar (VString "myBusiness")))
myBusiness has type business
myBusiness är av typen affär
PAtom (AKind (KFun (KInd (IVarN Business)) Boolean) (IVar (VString "is_legal")))
is_legal is a function from the type business to a Boolean value
is_legal är en funktion från typen affär till en boolesk variabel

So try running the command above; it does a stack build along the way, and you can expect the first run to take a little while.

If you get an error involving Syntax.gf, then you need to get your RGL and WordNet installed correctly. To get RGL installed, you need gf.

Where is gf? From inside the baby-l4 directory (which is where you should already be, if you are reading this):

Inside baby-l4, run

stack exec which gf

You should see something like:

/Users/mengwong/.stack/snapshots/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/bin/gf

Why? Baby-l4’s stack build installs a working gf as a dependency, so we will use that instead of installing gf-core from source.

Because it’s huge, save it to a variable in the shell:

mygf=`stack exec which gf`

In your ~/.zshenv or in your ~/.profile, depending on whether you belong to the zsh or bash persuasion, create a line

export GF_LIB_PATH=$HOME/gf_lib_path

For that environment variable to take effect, you can restart your shell or just paste it at your shell prompt. Now when you run:

echo $GF_LIB_PATH

You should see:

/Users/<you>/gf_lib_path

This is where gf will install the RGL, and where baby-l4’s codebase will look for it.

You need to create it.

mkdir $GF_LIB_PATH

TODO: raise a PR against gf-rgl to mkdir -p $GF_LIB_PATH if it doesn’t already exist. Note that this mkdir PR will be complicated by the fact that a GF_LIB_PATH may be a colon-separated list.

Now we are ready to install to it.

Download gf-rgl from Github:

mkdir ~/src
cd ~/src
git clone https://github.com/GrammaticalFramework/gf-rgl
cd gf-rgl

You should now be in a directory called ~/src/gf-rgl

In the gf-rgl directory, run:

./Setup.sh --gf=$mygf

You should see:

Building [prelude]
Building [present]
Building [alltenses]
Copying to /Users/mengwong/gf_lib_path

First, clone gf-wordnet:

cd ~/src
git clone https://github.com/GrammaticalFramework/gf-wordnet
cd gf-wordnet

Then run mygf on some of the WordNet*.gf files; this command will install the compiled gfo files to GF_LIB_PATH.

$mygf --gfo-dir=$GF_LIB_PATH WordNetEng.gf WordNetSwe.gf

stack run l4 l4/mini.l4

should produce a whole bunch of errors you can ignore:

Warning: Unable to find a known candidate for the Cabal entry Prop, but did find:
         * PropEng.gf
         * PropI.gf
         * PropLexiconEng.gf
         * PropLexicon.gf
         * PropTopEng.gf
         * PropLatex.gf
         * Prop.gf
         * PropTopSwe.gf
         * PropLexiconPor.gf
         * Prop.gfo
         * PropPor.gf
         * PropSwe.gf
         * PropTop.gf
         * PropTopPor.gf
         * PropLexiconSwe.gf If you are using a custom preprocessor for this module with its own file extension, consider adding the file(s)
         to your .cabal under extra-source-files.
baby-l4-0.1.0.0: unregistering (local file changes: README.org)
baby-l4> configure (lib + exe)
Configuring baby-l4-0.1.0.0...
baby-l4> build (lib + exe)
Preprocessing library for baby-l4-0.1.0.0..
Building library for baby-l4-0.1.0.0..
Preprocessing executable 'l4' for baby-l4-0.1.0.0..
Building executable 'l4' for baby-l4-0.1.0.0..

Warning: Unable to find a known candidate for the Cabal entry Prop, but did find:
         * PropEng.gf
         * PropI.gf
         * PropLexiconEng.gf
         * PropLexicon.gf
         * PropTopEng.gf
         * PropLatex.gf
         * Prop.gf
         * PropTopSwe.gf
         * PropLexiconPor.gf
         * Prop.gfo
         * PropPor.gf
         * PropSwe.gf
         * PropTop.gf
         * PropTopPor.gf
         * PropLexiconSwe.gf If you are using a custom preprocessor for this module with its own file extension, consider adding the file(s)
         to your .cabal under extra-source-files.
baby-l4> copy/register
Installing library in /Users/mengwong/src/smucclaw/baby-l4/.stack-work/install/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/lib/x86_64-osx-ghc-8.8.4/baby-l4-0.1.0.0-2uuTWxtfYE14aM49x0XA7O
Installing executable lsp-server-bl4 in /Users/mengwong/src/smucclaw/baby-l4/.stack-work/install/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/bin
Installing executable l4 in /Users/mengwong/src/smucclaw/baby-l4/.stack-work/install/x86_64-osx/0d89070f643fd180a58cfc42b9ba6fbece00cfd59cde65a81136970789de7eb9/8.8.4/bin
Registering library for baby-l4-0.1.0.0..

… and eventually produce the desired output:

Program [Mapping "is_legal" "legal_1_A",Mapping "Business" "business_1_N"] [] [VarDecl "myNumber" IntT,VarDecl "myBusiness" (ClassT (ClsNm "Business")),VarDecl "is_legal" (FunT (ClassT (ClsNm "Business")) BoolT)] [] []

PAtom (AKind Nat (IVar (VString "myNumber")))
myNumber is a number
myNumber är ett tal
PAtom (AKind (KInd (IVarN Business)) (IVar (VString "myBusiness")))
myBusiness has type business
myBusiness är av typen affär
PAtom (AKind (KFun (KInd (IVarN Business)) Boolean) (IVar (VString "is_legal")))
is_legal is a function from the type business to a Boolean value
is_legal är en funktion från typen affär till en boolesk variabel

If this install procedure did not go as planned, ask for help on Slack.

Yes, use colons to separate, as is the convention with $PATH variables.

If you are using Nix, obviously you are competent enough to figure it out on your own.

There is also something to do with flake.

Yes, patches welcome!