Other languages/tools

%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

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'.

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

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):

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

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

Commands:

• add <pkgname>: installation

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
• read_json, read_verilog, write_json, write_verilog: read, write netlist in different formats

Examples

• Get all hrefs from an html file: //@href
  • xmlstarlet sel -t -v "//@href" ../build/html/blog/index.html
• Extract only the contents of body tag:
  • xmllint --xpath '/html/body/node()' input.html
  • xmlstarlet sel -t -v '/html/body/node()' make4ht-vPSgKS.html (xmlstarlet removed comments, xmllint didn't)

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

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

Variables are global by default

var val = 1;
console.log("Outer val: " + val);
{
    console.log("Inner val: " + val);
    va1 = 2;
    console.log("Inner va1: " + va1);
}
console.log("Outer va1: " + va1);

// Outer val: 1
// Inner val: 1
// Inner va1: 2
// Outer va1: 2

In the above snippet, va1 was not limited to the inner scope but became a new global variable.

Concatenation vs addition

• + is string concatenation when one of the operands is a string
• + is addition when both operands are numbers

var n1 = 3;
var n2 = 5;
var n1n2 = n1+n2

var s1 = "Hi";
var s2 = "Hello";
var n1s1 = n1+s1;
var s1n1 = s1+n1;
var s1s2 = s1+s2;

console.log("n1+n2 = " + (n1 + n2));
console.log("n1+s1 = " + (n1 + s1));
console.log("s1+n1 = " + (s1 + n1));
console.log("s1+s2 = " + (s1 + s2));

// n1+n2 = 8
// n1+s1 = 3Hi
// s1+n1 = Hi3
// s1+s2 = HiHello

General

• Case insensitive keywords
• Single line comments start with !

—

File extension:

• .f90: modern fortran
• .f95: another
• .f77: old fortran
  • Needs -ffixed-form in gfortran
• .for

Compier: gfortran

F77

• First 6 columns of each line are 'reserved for special formatting purposes like statement numbers and continuation markers'
• ie, most lines needs to prefixed by 6 spaces
  • http://hpcf-files.umbc.edu/hpcf/hpc-archived/Fortran%2077%20Hello%20World%20Program.php
• Relic of punchcard era where lines had to be of a fixed length??
• Max length of line = 72
  • Continuation character in column 6 means next line/punchcard can be used
  • https://en.wikibooks.org/wiki/Fortran/Beginning_Fortran