Other languages/tools

Twelf
Beluga
awk
smtlib2
C++
Julia
Perl
yosys
xpath
fstar
HOL4
Nix (language)

Twelf

File extension: .elf
Comment (single line): Starts with %
Comment (multi-line): between %{ and %}
Coverage check
Totality check
Adequacy

`%name` ʳ

Not mandatory, but makes twelf output messages more readable.

If %name is given for a type, names of variables of that type which twelf generates will have the prefix indicated by %name.

Name starts with an uppercase letter. Usually a single letter would do, though multi-character prefixes are fine too.

For example, with the following definitions,

nat: type.
z: nat.
s: nat -> nat.

plus: nat -> nat -> nat -> type.
plus/z: plus z N N.
plus/s: plus (S N1) N2 (S N3) <- plus N1 N2 N3.
% plus/s: plus N1 N2 N3 -> plus (S N1) N2 (S N3).

Twelf gives:

_ = plus/s (plus/s plus/z).

% _ : {X1:nat -> nat} {X2:nat -> nat} {X3:nat} plus (X1 (X2 z)) X3 (X1 (X2 X3))
%    = [X1:nat -> nat] [X2:nat -> nat] [X3:nat] plus/s (plus/s plus/z).

But if we add a %name for ~nat, like

%name nat N.

It would have been:

_ = plus/s (plus/s plus/z).

% _ : {N1:nat -> nat} {N2:nat -> nat} {N3:nat} plus (N1 (N2 z)) N3 (N1 (N2 N3))
%    = [N1:nat -> nat] [N2:nat -> nat] [N3:nat] plus/s (plus/s plus/z).

List of keywords

`%.`	`%abbrev`	`%assert`	`%block`	`%clause`
`%covers`	`%define`	`%deterministic`	`%establish`	`%freeze`
`%infix`	`%prefix`	`%postfix`	`%mode`	`%name`
`%prove`	`%query`	`%querytabled`	`%reduces`	`%solve`
`%subord`	`%tabled`	`%terminates`	`%thaw`	`%theorem`
`%total`	`%trustme`	`%unique`	`%use`	`%worlds`

Emacs mode

As of January 2024, twelf.el file for emacs mode needs some brackets removed. Other than that, it should work right out of the box.

(Got to set twelf-root variable first.)

First, twelf-server needs to be started: M-x twelf-server (will display a 'Server OK' message).

C-c C-c: Load a configuration file
- Runs all files in the cfg file
C-c C-s: Load an elf file
C-c C-d: Type check a specific declaration

First run the cfg file. Afterwards individual elf files can be run as needed.

Configuration file

All files in a twelf project should be listed in a sources.cfg files. Those files are compiled in the order in which they are listed.

Misc

Wiki Twelf: like twelf literate programming.
Elf: Predecessor of twelf
Delphin: a research project which built on twelf
To have unproven assertions (for experimentation purposes), twelf needs to be put to 'unsafe mode'.

Beluga

https://github.com/Beluga-lang/Beluga

File extension: .bel
Comment (single line): Starts with %
Pure language
- no IO, exception, reference
There are no:
- built-in tuples, nat, bool
- polymorphism (theory of beluga is inconsistent with it)
Based on LF, like twelf.
- Feels very similar to twelf, but has major differences.
Boxing: Data is embedded into computations with [ |- stuff ].
Data and values live at different levels. So 'boxing' and 'unboxing' needed.
- 'Boxing is necessary to ensure we are working with pure data; unboxing is necessary for inspecting what the data looks like' ʳ

Variables:

Data variables will always be within a box
Program variables will never be within a box
Convention:
- Upper-case letters: data variables
- Lower-case letters: computation/program variables

Emacs mode

Key	Description	elisp function
C-c C-c	Compile	`'compile`
C-c C-l	Highlight holes	`'beluga-highlight-holes`
C-c C-x	Run command	`'beluga-run-command`
C-c C-t	Get type	`'beluga-get-type`
C-c C-s	Split hole	`'beluga-split-hole`
C-c C-i	Intro hole	`'beluga-intro-hole`
C-c C-j	Jump hole	`'beluga-hole-jump`
C-c C-p	Get hole info	`'beluga-hole-info`
C-c C-e	Erase holes	`'beluga-erase-holes`

harpoon

For interactive theorem proving with commands.
Bundled with beluga.
https://beluga-lang.readthedocs.io/en/latest/getting-started.html

Example:

$ harpoon --sig hello.bel
## Type Reconstruction begin: hello.bel ##
## Type Reconstruction done:  hello.bel ##
Configuring theorem #1
  Name of theorem (:quit or empty to finish):

awk

Reference:

The AWK programming language - Alfred Aho, Brian Kernighan, Peter J. Weinberger
https://www.gnu.org/software/gawk/manual/gawk.html

Line number starts from 0.

Predefined variables

https://www.gnu.org/software/gawk/manual/gawk.html#Built_002din-Variables

NR: line/record number (from all files)
FNR: line number (from current file)
RS: record separator. ie, separates lines
- Default \n.
END:
$0: current line text

BEGIN and END

Special patterns.

BEGIN: run before file is processed
END: run after file is processed

Positional specifier

Follwing two statements have the same effect:

printf "%s %s\n", "hello", "world"
printf "%2$s %1$s\n", "world", "hello"

and prints 'hello world'.

Appending to a string variable

$ echo 'a' | awk 'BEGIN {a="1"} /.+/ {a=a$0} END{print a}'
1a

awk function

function <name> {

}

https://faculty.cs.niu.edu/~berezin/330/N/awk-fun.html

Arithmetic

Integer division: int()
Can treat strings as if they are numbers

String substitution

sub
gsub

https://www.gnu.org/software/gawk/manual/html_node/String-Functions.html

Matching non-empty lines

A trick:

length { <code> }

This works because length of empty line gives 0, which is considered as false value.

Thanks to tirnanog from #awk.

Tips

print "": outputs a blank line (with \n?)
Indexing starts from 1
Formatting functions: sprintf, printf

Jargon

awk	Meaning
record	line

smtlib2

smtlib2 is a format for SAT/SMT solvers like z3.

(declare-const a Bool)

is short for

(define-fun b () Bool)

Julia

https://computationalthinking.mit.edu/Fall24/installation/

General

Import package: using pkgname
Packages for drawing plots:
- plots.jl: https://docs.juliaplots.org/stable/
  - PGFPlots backend can be used for plots to be used in latex
  - Unicodeplots: plots as text
  - plotly: plots for webpages
- https://discourse.julialang.org/t/comparison-of-plotting-packages/99860/2
- LatexStrings can be used to write labels in latex syntax

Package management

Drop to julia repl and type ]
Prompt will change to pkg>

Commands:

add <pkgname>: installation

yosys

Prompt

In interactive mode:

yosys>: Entire design selected
yosys*>: Only a part of design selected
yosys [modname]>: Entire module named modname selected
yosys [modname]*>: Only a part of module named modname selected

Commands

shell: enter shell
show: make diagram (graphviz) for selected design
proc: translate process blocks to netlists
fsm:
memory:
hierarchy:
cd: alias for ~select -module <modname>
- Can do cd .. to back to topmost level ??
sta: perform static timing analysis
clean
difflibmap
check
flattern
future
opt
techmap
printattrs

xpath

Resources:

xmlstarlet is a tool that can handle xpath.

html can be used as input but it (probably) needs to be xml-like. ie, all tags needs to be closed.

`.`	Current node
`..`	Parent node
`@`	Specify attribute
`/`	Directly under current node
`//`	Anywhere under current node
`last`
`starts-with`

/* 2nd node under root */
/root/node[2]

Examples

Get all hrefs from an html file: //@href

xmlstarlet sel -t -v "//@href" ../build/html/blog/index.html

fstar

Theorem prover.

Proof-oriented programming in F*/

General

Low*: A subset of F* that can be compiled down to C (using KaRaMeL)
- Low* is a DSL (shallow) within F*
Dependent types possible
F* is turing complete, but in a way that doesn't break consistency.
- ie, infinite recursion possible somehow.
Proofs often involve using SMT solvers like Z3.
F* programs are extractable to:
- C
- OCaml
- WASM
- F#
Comments:
- Multiline: (* comment *)
- Single-line: // comment
File extension: .fst
Each file must be a module, apparently

Emacs mode: fstar-mode.el

C-c v: Load entire buffer for type checking

Interactive mode:

C-c C-n: Next line
C-c C-u: Previous line

HOL4

HOL4 theorem prover: https://hol-theorem-prover.org/cheatsheet.html

File extension: .sml

>> ?
rw: rewrite ?
tac1 >> tac2: apply tac1, then use tac2 on all generated goals
- Like tac1; tac2 in coq
f $ g: f (g x)
- Right associative function application
- Same as in Haskell

Curry

A functional-logic programming language.
Kind of like some aspects of Prolog and Haskell mixed together

lst :: Data a => [a] -> [a]
lst l | _:xs =:= l
      = xs
  where xs free

The where clause tells that xs does not appear in l (is free in l) so that the compiler can see that it came out of the blue.

=:= is an equation invoking unification.

Used KICS2 v3.1 for the above snippet. https://www-ps.informatik.uni-kiel.de/kics2/Manual.pdf

lst [1,2,3] gave this:

-------------------------------------
Executing with KiCS2 3.1 /all-values:
-------------------------------------

[2,3]
KiCS2 compilation time: 1.21s / elapsed: 0:01.54
KiCS2 compilation time: 1.19s / elapsed: 0:01.48
GHC compilation time: 1.64s / elapsed: 0:02.46
Execution time: 0.00s / elapsed: 0:00.01

Looks like lst [] simply doesn't result in any value instead of giving error as in Haskell:

-------------------------------------
Executing with KiCS2 3.1 /all-values:
-------------------------------------

KiCS2 compilation time: 1.22s / elapsed: 0:02.13
KiCS2 compilation time: 1.16s / elapsed: 0:01.50
GHC compilation time: 1.68s / elapsed: 0:06.56
Execution time: 0.00s / elapsed: 0:00.01

Default rules

Curry lang

KICS2: Haskell target
PAKCS: Prolog target

https://curry.pages.ps.informatik.uni-kiel.de/curry-lang.org/

endAsStart :: Data a => [a] -> Bool
endAsStart l | x:(xs ++ [x]) =:= l 
      = True
 where x,xs free
endAsStart'default _ = False

Links:

Nix (language)

Language associated with NixOS.

References:

General

Nix is like json with functions.
List elements are separated by a space.
Attribute names needn't be within quotes. Can be though.
Derivation: A build task in nix
a.b.c=1 means a = {b = {c = 1}} ??
Comments: starts with #
nix-repl: A repl to try out nix expressions
- Useful for just getting familiar with nix
- For ease of use, assignment statements are allowed in nix-repl.
- But proper nix only has expressions.
nix-instantiate: evaluate a nix file
- nix-instantiate --eval file.nix

Functions

Functions take only one argument.
All functions are anonymous. But they can be assigned to a variable though.

Examples:

x: x+1: Increment
x: y: x+y: Addition
{x, y}: x+y: Addition

HTML

Tags:

object
embed

SystemC

#include <systemc.h>

sc_in: input port
sc_out: output port
sc_bit: bit type
sc_signal
SC_CTOR: constructor
SC_METHOD: a block with its sensitivity list
- Sensitivity list specified with sensitive keyword
SC_MODULE
SC_CTHREAD
sc_time_stamp()
wait()
sc_trace
sc_start: starts simulation
- First call: starts scheduler ˡ
- Subsequent calls: resume scheduler
sc_main: like main() in C

—

Convert synthesizable systemc to systemverilog: https://github.com/intel/systemc-compiler

—

Links:

Twelf

%name ʳ

List of keywords

Emacs mode

Configuration file

Misc

Beluga

Variables:

Emacs mode

harpoon

awk

Predefined variables

BEGIN and END

Positional specifier

Appending to a string variable

awk function

Arithmetic

String substitution

Matching non-empty lines

Tips

Jargon

smtlib2

Julia

General

Package management

yosys

Prompt

Commands

xpath

Examples

fstar

General

Emacs mode: fstar-mode.el

HOL4

Curry

Nix (language)

General

Functions

HTML

SystemC

`%name` ʳ