Grundlagen

Datei: HelloWorld.hih

module Example.HelloWorld is
    """
    No contract: the exit code of the programme, the result of what it did.
    """
    function main(): ExitCode;
end module.

Datei: HelloWorld.hiq

module body Example.HelloWorld is
    function main(): ExitCode is
        printLn("Hello, world!");
        return ExitSuccess();
    end;
end module body.

Ausgabe von ./main (Exit-Status 0):

Hello, world!

Datei: LearnMatch.hiq

module body Example.LearnMatch is
    -- A key of a keyboard: a character by its code, or one of two keys
    -- that are not characters.
    union Key: Free is
        case Char is
            code: Nat8;
        case Enter;
        case Escape;
    end;

    -- What a programme is told: a key was pressed, with or without shift,
    -- or some time has passed.
    union Event: Free is
        case Press is
            key: Key;
            shift: Bool;
        case Tick is
            millis: Nat32;
    end;

    -- The patterns look two levels deep: into the event and into its key.
    -- A range such as 97 .. 122 takes every value from 97 to 122, the
    -- small letters a to z.  A bar joins patterns that have the same
    -- answer, and an underscore takes any value without a name.  The first
    -- pattern that fits is taken, and the compiler refuses a case that
    -- leaves out a value.
    function describe(event: Event): Unit is
        case event of
            when Press(Char(97 .. 122), false) do
                printLn("a small letter");
            when Press(Char(97 .. 122), true) | Press(Char(65 .. 90), _) do
                printLn("a capital letter");
            when Press(Char(48 .. 57), _) do
                printLn("a digit");
            when Press(Char(_), _) do
                printLn("another character");
            when Press(Enter, _) | Press(Escape, _) do
                printLn("a key that is not a character");
            when Tick(0) do
                printLn("no time at all");
            when Tick(millis) do
                print("a tick of ");
                print(millis);
                printLn(" ms");
        end case;
        return nil;
    end;

    function press(code: Nat8, shift: Bool): Event is
        return Press(key => Char(code => code), shift => shift);
    end;

    function main(): ExitCode is
        describe(press('q', false));
        describe(press('q', true));
        describe(press('Q', false));
        describe(press('7', false));
        describe(press('!', true));
        describe(Press(key => Enter(), shift => false));
        let none: Nat32 := 0;
        let quarter: Nat32 := 250;
        describe(Tick(millis => none));
        describe(Tick(millis => quarter));
        return ExitSuccess();
    end;
end module body.

Ausgabe von ./main (Exit-Status 0):

a small letter
a capital letter
a capital letter
a digit
another character
a key that is not a character
no time at all
a tick of 250 ms

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Parse Error
  Error code: H0009
  Module:
    [unknown]
  Location:
    Filename: 'Example.hiq'
    From: line 3, column 34
    To: line 3, column 35
  Description:
    Hilde has no operator precedence: an operator takes two operands, and only `+`, `*`, `and` and `or` can be chained with themselves. Put the operation before `*` in parentheses, as in `(a + b) * c`.
    
    Suggested fix: `(1 + 2)`
  Code:
    1 | module body Example is
    2 |     function main(): ExitCode is
    3 |         let total: Int32 := 1 + 2 * 3;
    4 |         printLn(total);
    5 |         return ExitSuccess();

Datei: LearnBorrow.hiq

module body Example.LearnBorrow is
    record Counter: Linear is
        count: Nat32;
    end;

    -- A write reference, &!, lets the callee change the caller's value.
    generic [R: Region]
    function bump(counter: &![Counter, R]): Unit is
        counter->count := counter->count + 1;
        return nil;
    end;

    -- A write reference passed on is used up.  &~ passes on a new one
    -- and keeps the old one usable; the last use may pass it on itself.
    generic [R: Region]
    function bumpTwice(counter: &![Counter, R]): Unit is
        bump(&~counter);
        bump(counter);
        return nil;
    end;

    function main(): ExitCode is
        -- var, because a write reference is taken from it.
        var counter: Counter := Counter(count => 0);
        bumpTwice(&!counter);
        bump(&!counter);
        let { count: Nat32 } := counter;
        printLn(count);
        return ExitSuccess();
    end;
end module body.

Ausgabe von ./main (Exit-Status 0):

3

Datei: Example.hiq

module body Example is
    record Ticket: Linear is
        number: Int32;
    end;

    function redeem(ticket: Ticket): Int32 is
        let { number: Int32 } := ticket;
        return number;
    end;

    function main(): ExitCode is
        let ticket: Ticket := Ticket(number => 7);
        borrow view: &[Ticket, R] := &ticket do
            printLn(redeem(ticket));
        end borrow;
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Linearity Error
  Error code: H4006
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 14, column 12
    To: line 14, column 36
  Description:
    The variable `ticket` cannot be consumed while it is borrowed (immutably).
  Code:
    12 |         let ticket: Ticket := Ticket(number => 7);
    13 |         borrow view: &[Ticket, R] := &ticket do
    14 |             printLn(redeem(ticket));
    15 |         end borrow;
    16 |         return ExitSuccess();

Datei: Example.hiq

module body Example is
    generic [R: Region]
    function same(x: &[Int32, R]): &[Int32, R] is
        return x;
    end;

    function main(): ExitCode is
        let n: Int32 := 5;
        let value: Int32 := !same(&n);
        printLn(value);
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 0):

hilde check: 1 modules given, 1 checked, no error

Ausgabe von ./main (Exit-Status 0):

5

Datei: Example.hiq

module body Example is
    generic [R: Region]
    function local(n: Int32): &[Int32, R] is
        let x: Int32 := n;
        return &x;
    end;

    function main(): ExitCode is
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Type Error
  Error code: H3094
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 5, column 8
    To: line 5, column 18
  Description:
    A reference made inside this function cannot be handed out as `R`.
    
    `R` is a region parameter of the function: the caller chooses it, and it outlives the call.  The reference here has the region `Region<55>`, which ends inside the function.
  Code:
    3 |     function local(n: Int32): &[Int32, R] is
    4 |         let x: Int32 := n;
    5 |         return &x;
    6 |     end;
    7 | 

Datei: Example.hiq

module body Example is
    record Ticket: Linear is
        number: Int32;
    end;

    function main(): ExitCode is
        let ticket: Ticket := Ticket(number => 7);
        let { number: Int32 } := ticket;
        printLn(number);
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 0):

hilde check: 1 modules given, 1 checked, no error

Ausgabe von ./main (Exit-Status 0):

7

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Linearity Error
  Error code: H4012
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 8, column 8
    To: line 8, column 29
  Description:
    The variable `ticket` is not consumed by the time of the return statement. Did you forget to call a destructor, or destructure the contents?
  Code:
     6 |     function main(): ExitCode is
     7 |         let ticket: Ticket := Ticket(number => 7);
     8 |         return ExitSuccess();
     9 |     end;
    10 | end module body.

Datei: Example.hiq

module body Example is
    record Ticket: Linear is
        number: Int32;
    end;

    function redeem(ticket: Ticket): Int32 is
        let { number: Int32 } := ticket;
        return number;
    end;

    function main(): ExitCode is
        let ticket: Ticket := Ticket(number => 7);
        printLn(redeem(ticket));
        printLn(redeem(ticket));
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Linearity Error
  Error code: H4008
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 14, column 8
    To: line 14, column 32
  Description:
    The variable `ticket` has already been consumed.
  Code:
    12 |         let ticket: Ticket := Ticket(number => 7);
    13 |         printLn(redeem(ticket));
    14 |         printLn(redeem(ticket));
    15 |         return ExitSuccess();
    16 |     end;

Datei: LearnContracts.hih

module Example.LearnContracts is
    -- An account holds a balance.  It is linear: it is opened once and
    -- closed once, and nothing else can make one disappear.
    record Account: Linear is
        balance: Nat64;
    end;

    """
    No contract: a value of its own type built from its arguments; no property cheaper than its type holds.
    """
    function open(amount: Nat64): Account;

    """
    No contract: a number read from its argument; its type gives its range, and nothing cheaper holds.
    """
    generic [R: Region]
    function balance(account: &[Account, R]): Nat64;

    -- A deposit adds a positive amount, and the balance afterwards is the
    -- old balance plus the amount.
    generic [R: Region]
    function deposit(account: &![Account, R], amount: Nat64): Unit
        requires amount > 0
        ensures balance(&account) = (old(balance(&account)) + amount);

    -- A withdrawal takes a positive amount the account holds.  The caller
    -- has to make sure of that: a call that does not is stopped before the
    -- function runs, and the message names this line and the call.
    generic [R: Region]
    function withdraw(account: &![Account, R], amount: Nat64): Unit
        requires (amount > 0) and (amount <= balance(&account))
        ensures balance(&account) = (old(balance(&account)) - amount);

    """
    Closes the handle it is given.
    No contract: it only frees or closes what it is given.
    """
    function close(account: Account): Nat64;

    """
    No contract: the exit code of the programme, the result of what it did.
    """
    function main(): ExitCode;
end module.

Datei: LearnContractsBroken.hiq

import Example.LearnContracts (
    Account,
    open,
    balance,
    withdraw,
    close
);

module body Example.LearnContractsBroken is
    -- The second withdrawal asks for more than the account holds.  The
    -- requires of withdraw does not hold, so the programme stops before
    -- withdraw runs, and the message names the contract in
    -- LearnContracts.hih and this call.  The last two lines never run.
    function main(): ExitCode is
        var account: Account := open(100);
        withdraw(&!account, 30);
        printLn(balance(&account));
        withdraw(&!account, 71);
        printLn(balance(&account));
        printLn(close(account));
        return ExitSuccess();
    end;
end module body.

Ausgabe von ./main (Exit-Status 0):

150
30
30

Ausgabe von ./broken (Exit-Status 255):

70
Hilde: contract violated: the requires (amount > 0) and (amount <= balance(&account)) of Example.LearnContracts.withdraw (LearnContracts.hih:38) does not hold for the call at LearnContractsBroken.hiq:25; the caller is at fault

Ausgabe von hilde check Example.hih,Example.hiq (Exit-Status 255):

Error:
  Title: Declaration Error
  Error code: H2051
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 3, column 8
    To: line 3, column 22
  Description:
    The body of the public function `half` holds a contract.
    
    The contract of a public function stands in its interface only: it is written at `Example.hih:3`.  Remove the requires, ensures and raises clauses from the body.
  Code:
    1 | module body Example is
    2 |     function half(n: Nat32): Nat32
    3 |         requires n > 0
    4 |     is
    5 |         return n / 2;

Datei: LearnErrors.hiq

module body Example.LearnErrors is
    -- Half of an even number, and nothing for an odd one.
    function halve(n: Int32): Option[Int32] is
        if (n - ((n / 2) * 2)) = 0 then
            let half: Int32 := n / 2;
            let some: Option[Int32] := Some(value => half);
            return some;
        else
            let none: Option[Int32] := None();
            return none;
        end if;
    end;

    -- ? after a call, as the whole right side of a let: a None makes
    -- this function return None at once, a Some gives its value.
    function eighth(n: Int32): Option[Int32] is
        let a: Int32 := halve(n)?;
        let b: Int32 := halve(a)?;
        let c: Int32 := halve(b)?;
        let some: Option[Int32] := Some(value => c);
        return some;
    end;

    function show(result: Option[Int32]): Unit is
        case result of
            when Some(value as v: Int32) do
                printLn(v);
            when None do
                printLn("odd on the way");
        end case;
        return nil;
    end;

    function main(): ExitCode is
        show(eighth(40));
        show(eighth(12));
        -- An Option or Either nobody looks at is a compile error; a
        -- result that really does not matter is thrown away by name.
        ignore(halve(7));
        return ExitSuccess();
    end;
end module body.

Ausgabe von ./main (Exit-Status 0):

5
odd on the way

Datei: Example.hiq

module body Example is
    function half(n: Int32): Option[Int32] is
        let r: Option[Int32] := Some(value => n / 2);
        return r;
    end;

    function main(): ExitCode is
        half(4);
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Type Error
  Error code: H3037
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 8, column 8
    To: line 8, column 16
  Description:
    The value of this expression has type `Option[Int32]`, which carries a failure the caller is meant to look at, so it may not be thrown away. Handle it with a case statement, hand it to your own caller with the ? operator, or, if the failure really is to be ignored here, say so in the program with ignore(...).
  Code:
     6 | 
     7 |     function main(): ExitCode is
     8 |         half(4);
     9 |         return ExitSuccess();
    10 |     end;

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Declaration Error
  Error code: H2028
  Module:
    Example
  Location:
    [no span available]
  Description:
    Cannot import from the `Hilde.Memory` module in a safe module.
    
    Consider using a safe wrapper or adding `pragma Unsafe_Module;`
  Code:
    [no span available]

Datei: Example.hiq

import Bindings.Time (wallNanos);

module body Example is
    function main(): ExitCode is
        printLn(wallNanos() > 0);
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Declaration Error
  Error code: H2045
  Module:
    Example
  Location:
    [no span available]
  Description:
    `Example` imports from `Bindings.Time`, a module that binds C.
    
    Only the standard library imports a module whose name begins with `Bindings.`; a program imports the safe module built on it, whose name begins with `Standard.`.
  Code:
    [no span available]

Datei: Example.hiq

import Standard.Task (Scope, openScope, closeScope, Task, spawn, join);

module body Example is
    function double(n: Index): Index is
        return n * 2;
    end;

    function main(): ExitCode is
        let n: Index := 5;
        case openScope() of
            when Some(value as opened: Scope) do
                var scope: Scope := opened;
                let work: Fn[Index, Index] := double;
                case spawn(&!scope, work, n) of
                    when Right(right as task: Task[Index]) do
                        printLn(join(task));
                    when Left(left as back: Index) do
                        printLn(back);
                end case;
                closeScope(scope);
            when None do
                skip;
        end case;
        return ExitSuccess();
    end;
end module body.

Ausgabe von hilde check Example.hiq (Exit-Status 0):

hilde check: 1 modules given, 8 checked, no error

Ausgabe von ./main (Exit-Status 0):

10

Ausgabe von hilde check Example.hiq (Exit-Status 0):

hilde check: 1 modules given, 8 checked, no error

Ausgabe von hilde compile Example.hiq --entrypoint=Example:main --output=main (Exit-Status 255):

Error:
  Title: Type Error
  Error code: H3002
  Module:
    Example
  Location:
    [no span available]
  Description:
    The argument of a task holds a reference or a span.
    
    A task can outlive the borrow the reference comes from, so what is handed to `Standard.Task.spawn` must own everything it points at.  Move the value in, or copy what the task needs.
  Code:
    [no span available]

Ausgabe von hilde check Example.hiq (Exit-Status 255):

Error:
  Title: Type Error
  Error code: H3066
  Module:
    Example
  Location:
    Filename: 'Example.hiq'
    From: line 18, column 24
    To: line 23, column 33
  Description:
    The argument of a task in a lending scope holds a reference of another region.
    
    A task started with `Standard.Task.spawnLending` may be lent only what the scope's own borrow lends -- the region the scope was opened for -- because only that borrow is sure to outlive the task.
  Code:
    16 |                     borrow i: &[Index, sigma] := &inner do
    17 |                         let work: Fn[&[Index, sigma], Index] := read;
    18 |                         case spawnLending(&!scope, work, i) of
    19 |                             when Right(right as task: Task[Index]) do
    20 |                                 printLn(join(task));
    21 |                             when Left(left as back: &[Index, sigma]) do
    22 |                                 printLn(0);
    23 |                         end case;
    24 |                     end borrow;
    25 |                     closeLending(scope);