Syntax Reference

※ utils;

/* User record: stores a name and an age,
   used across the file read and greeting logic below */
⊞ User { 𝕊 name, ℤ age };

⊎ Outcome { Success(𝕊), Failure(FileNotFound) };

equals User(a, b) -> 𝔹 {
    ↵ a.name = b.name;
}

:: greet(§ User u) -> 𝕊 {
    § 𝕊 greeting <- join("Hello, ", u.name);
    ↵ greeting;
}

:: readUserFile(§ User u, ⊙ FileReadCapability cap) -> 𝕊 {
    ⚑ ↯ readFile(u.name, cap) {
        success(contents) → ↵ contents;
        failure(err) → ↵ "could not read file";
    }
}

:: isAdult(§ User u) -> 𝔹 {
    ? (u.age >= 18) : {
        ↵ ⊤;
    } ⋮ {
        ↵ ⊥;
    }
}

:: printVoid() -> ▢ {
    ↯ logMessage("done");
}

:: firstAdultName(§ ⟦τ User, σ 5⟧ users) -> 𝕊 {
    § ℤ i <- 0;

    ⥁ (i < 5) {
        ? (↯ isAdult(users @ i)) : {
            ↵ (users @ i).name;
        } ⋮ {
            i <- i + 1;
        }
    }

    ↵ "no adult found";
}

:: countVowels(§ 𝕊 word) -> ℤ {
    § ℤ count <- 0;
    § ℤ i <- 0;

    ↻ i 0..10 {
        ? ((word @ i) = 'a') : {
            count <- count + 1;
        } ⋮ {
            count <- count;
        }

        ? (i = 9) : {
            ⏹;
        } ⋮ {
            ▶;
        }
    }

    ↵ count;
}

:: oldestUser(§ ⟦τ User, σ 3⟧ users) -> User {
    § ℤ oldestIndex <- 0;
    § ℤ i <- 0;

    ↻ i 0..3 {
        ? ((users @ i).age > (users @ oldestIndex).age) : {
            oldestIndex <- i;
        } ⋮ {
            oldestIndex <- oldestIndex;
        }
    }

    ↵ users @ oldestIndex;
}

:: main(⊙ FileReadCapability cap) -> ℤ {
    § User sam <- ↳ User { name: "Sam", age: 25 };
    § User alex <- ↳ User { name: "Alex", age: 31 };
    § User priya <- ↳ User { name: "Priya", age: 42 };

    § ⟦τ User, σ 3⟧ users <- [sam, alex, priya];
    § ⟦τ ⟦τ ℤ, σ 3⟧, σ 3⟧ grid <- [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

    § ℂ initial <- 'S';
    § ℤ hexValue <- 0x1F;
    § ℝ bigNumber <- 1e10;

    § 𝕊 greeting <- ↯ greet(sam);
    § 𝔹 samIsAdult <- ↯ isAdult(sam);
    § User oldest <- ↯ oldestUser(users);
    § ℤ max <- ? (sam.age > alex.age) : { ↵ sam.age; } ⋮ { ↵ alex.age; };

    ⋈ oldest.name {
        "Priya" → ↵ 1;
        _ → ↵ 0;
    }
}

import utils;

/* User record: stores a name and an age,
   used across the file read and greeting logic below */
rec User { str name, int age };

union Outcome { Success(str), Failure(FileNotFound) };

equals User(a, b) -> bool {
    ret a.name = b.name;
}

fn greet(var: User u) -> str {
    var: str greeting <- join("Hello, ", u.name);
    ret greeting;
}

fn readUserFile(var: User u, cap: FileReadCapability cap) -> str {
    verify call readFile(u.name, cap) {
        success(contents) -> ret contents;
        failure(err) -> ret "could not read file";
    }
}

fn isAdult(var: User u) -> bool {
    if (u.age >= 18) then {
        ret true;
    } else {
        ret false;
    }
}

fn printVoid() -> void {
    call logMessage("done");
}

fn firstAdultName(var: arr[type: User, size: 5] users) -> str {
    var: int i <- 0;

    while (i < 5) {
        if (call isAdult(users at i)) then {
            ret (users at i).name;
        } else {
            i <- i + 1;
        }
    }

    ret "no adult found";
}

fn countVowels(var: str word) -> int {
    var: int count <- 0;
    var: int i <- 0;

    for i 0..10 {
        if ((word at i) = 'a') then {
            count <- count + 1;
        } else {
            count <- count;
        }

        if (i = 9) then {
            break;
        } else {
            continue;
        }
    }

    ret count;
}

fn oldestUser(var: arr[type: User, size: 3] users) -> User {
    var: int oldestIndex <- 0;
    var: int i <- 0;

    for i 0..3 {
        if ((users at i).age > (users at oldestIndex).age) then {
            oldestIndex <- i;
        } else {
            oldestIndex <- oldestIndex;
        }
    }

    ret users at oldestIndex;
}

fn main(cap: FileReadCapability cap) -> int {
    var: User sam <- new User { name: "Sam", age: 25 };
    var: User alex <- new User { name: "Alex", age: 31 };
    var: User priya <- new User { name: "Priya", age: 42 };

    var: arr[type: User, size: 3] users <- [sam, alex, priya];
    var: arr[type: arr[type: int, size: 3], size: 3] grid <- [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

    var: char initial <- 'S';
    var: int hexValue <- 0x1F;
    var: float bigNumber <- 1e10;

    var: str greeting <- call greet(sam);
    var: bool samIsAdult <- call isAdult(sam);
    var: User oldest <- call oldestUser(users);
    var: int max <- if (sam.age > alex.age) then { ret sam.age; } else { ret alex.age; };

    match oldest.name {
        "Priya" -> ret 1;
        _ -> ret 0;
    }
}

import utils;

/* User record: stores a name and an age,
   used across the file read and greeting logic below */
record User { string name, integer age };

either Outcome { Success(string), Failure(FileNotFound) };

equals User(a, b) returnType boolean {
    return a.name = b.name;
}

function greet(container: User u) returnType string {
    container: string greeting <- join("Hello, ", u.name);
    return greeting;
}

function readUserFile(container: User u, capability: FileReadCapability cap) returnType string {
    verify runFunction readFile(u.name, cap) {
        success(contents) means return contents;
        failure(err) means return "could not read file";
    }
}

function isAdult(container: User u) returnType boolean {
    if (u.age >= 18) then {
        return true;
    } else {
        return false;
    }
}

function printVoid() returnType void {
    runFunction logMessage("done");
}

function firstAdultName(container: list[type: User, size: 5] users) returnType string {
    container: integer i <- 0;

    whileLoop (i < 5) {
        if (runFunction isAdult(users at i)) then {
            return (users at i).name;
        } else {
            i <- i + 1;
        }
    }

    return "no adult found";
}

function countVowels(container: string word) returnType integer {
    container: integer count <- 0;
    container: integer i <- 0;

    loop i 0..10 {
        if ((word at i) = 'a') then {
            count <- count + 1;
        } else {
            count <- count;
        }

        if (i = 9) then {
            break;
        } else {
            continue;
        }
    }

    return count;
}

function oldestUser(container: list[type: User, size: 3] users) returnType User {
    container: integer oldestIndex <- 0;
    container: integer i <- 0;

    loop i 0..3 {
        if ((users at i).age > (users at oldestIndex).age) then {
            oldestIndex <- i;
        } else {
            oldestIndex <- oldestIndex;
        }
    }

    return users at oldestIndex;
}

function main(capability: FileReadCapability cap) returnType integer {
    container: User sam <- new User { name: "Sam", age: 25 };
    container: User alex <- new User { name: "Alex", age: 31 };
    container: User priya <- new User { name: "Priya", age: 42 };

    container: list[type: User, size: 3] users <- [sam, alex, priya];
    container: list[type: list[type: integer, size: 3], size: 3] grid <- [[1, 2, 3], [4, 5, 6], [7, 8, 9]];

    container: character initial <- 'S';
    container: integer hexValue <- 0x1F;
    container: float bigNumber <- 1e10;

    container: string greeting <- runFunction greet(sam);
    container: boolean samIsAdult <- runFunction isAdult(sam);
    container: User oldest <- runFunction oldestUser(users);
    container: integer max <- if (sam.age > alex.age) then { return sam.age; } else { return alex.age; };

    check oldest.name {
        "Priya" means return 1;
        anything means return 0;
    }
}