Other languages/tools

Twelf

%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).

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

Beluga

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

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

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

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

Package management

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

Commands:

yosys

Prompt

In interactive mode:

Commands

xpath

Resources:

xmlstarlet is a tool that can handle xpath.

. 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

fstar

Theorem prover.

General

Emacs mode: fstar-mode.el

Interactive mode:

HOL4

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

File extension: .sml

Curry

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

Curry lang

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

Functions

Examples:

HTML

Tags:

SystemC

#include <systemc.h>

—

—

Links:

Javascript

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

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

Fortran

https://en.wikibooks.org/wiki/Fortran/Hello_world

General

—

File extension:

Compier: gfortran

F77

Cobol

Dbts: