k5 (kframework) installation with vim goodies
docker run -u dev --entrypoint="" -v $(pwd):/home/dev/playground jakegillberg/kframework /bin/bash --login -c 'cd /home/dev/playground; echo "hello world"'
If it works, you should see a printed hello world. Replace echo "hello world" with a different command you would like to run, like kompile.
Create a file called lambda.k and write the below lines to it:
module LAMBDA
imports DOMAINS
syntax Val ::= Id
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [left]
| "(" Exp ")" [bracket]
endmodule
Congratulations! you just wrote a K definition!
Replace echo "hello world" with kompile lambda.k in the command above for:
docker run -u dev --entrypoint="" -v $(pwd):/home/dev/playground jakegillberg/kframework /bin/bash --login -c 'cd /home/dev/playground; kompile lambda.k'
Contratulations! You just compiled a K definition! You should see the below output:
40 states, 1247 transitions, table size 5228 bytes
[Warning] Compiler: Could not find main syntax module with name LAMBDA-SYNTAX
in definition. Use --syntax-module to specify one. Using LAMBDA as default.
Create a file called identity.lambda and write the below line to it:
lambda x . x
Congratulations! You just wrote a progam in your newly-defined language!
Execute krun identity.lambda in your docker environment, like we did with kompile lambda.k:
docker run -u dev --entrypoint="" -v $(pwd):/home/dev/playground jakegillberg/kframework /bin/bash --login -c 'cd /home/dev/playground; krun identity.lambda'
Congratulations! You just parsed a program using kframework! You should see the elow output:
<k>
lambda x . x
</k>