User-Defined Types and Structures

Ursus supports custom data structures through records (structs) and enumerations. This section explains how to define and use them.

Records (Structs)

Records are the primary way to define custom data structures in Ursus.

Defining Records

Recommended way (using Contract):

Types
  Record Person := {
      name: string;
      surname: string;
      age: uint256
  };

This is the recommended approach as it integrates with the Contract system.

Manual way (using GlobalGeneratePruvendoRecord):

Inductive PersonFields :=
| Person_ι_name
| Person_ι_surname
| Person_ι_age.

Definition PersonL := [string : Type ; string : Type ; uint256 : Type]%glist.
GlobalGeneratePruvendoRecord PersonL PersonFields.

This creates a type called PersonLRecord. This approach is not recommended for normal use.

Record Literals

Syntax:

[$ value1 ⇒ field1 ;
   value2 ⇒ field2 ;
   ...
   valueN ⇒ fieldN $]

Example:

::// var person: Person := [$ {"John"} ⇒ name ;
                               {"Smith"} ⇒ surname ;
                               {42} ⇒ age $] .

Accessing Fields

Read field:

::// var person_name: string := person->name .
::// var person_age: uint256 := person->age .

Write field:

::// person->age := {43} .
::// person->name := {"Jane"} .

Nested Records

Records can contain other records:

Types
  Record Address := {
      street: string;
      city: string;
      zipcode: uint32
  }
  Record Person := {
      name: string;
      home_address: (_ResolveName "Address");
      age: uint256
  };

Usage:

::// var addr: Address := [$ {"Main St"} ⇒ street ;
                             {"NYC"} ⇒ city ;
                             {10001} ⇒ zipcode $] .

::// var person: Person := [$ {"John"} ⇒ name ;
                              addr ⇒ home_address ;
                              {42} ⇒ age $] .

::// var city: string := person->home_address->city .

Enumerations

Enumerations define a type with a fixed set of values.

Defining Enums

Types
  Inductive Status := Pending | Active | Completed | Cancelled;

Using Enums

Assignment:

::// var status: Status := Active .

Pattern matching:

::// match status with
     | Pending => { ->> }
     | Active => { ->> }
     | Completed => { ->> }
     | Cancelled => { ->> }
     end | .
{
    ::// (* Pending case *) |.
}
{
    ::// (* Active case *) |.
}
{
    ::// (* Completed case *) |.
}
{
    ::// (* Cancelled case *) |.
}

Using Records in Contracts

As Contract State

Types
  Record User := {
      user_id: uint256;
      balance: uint256;
      active: boolean
  };

Record Contract := {
    owner: address;
    current_user: (_ResolveName "User");
    users: mapping address (_ResolveName "User")
}.

In Function Parameters

Ursus Definition registerUser (user: User): UExpression PhantomType false.
{
    ::// users[[msg->sender]] := user |.
}
return.
Defined.

In Function Returns

#[pure, returns=_result]
Ursus Definition getUser (addr: address): UExpression User false.
{
    ::// _result := users[[addr]] |.
}
return.
Defined.

Complex Examples

Record with Mappings

Types
  Record TokenInfo := {
      total_supply: uint256;
      balances: mapping address uint256;
      allowances: mapping address (mapping address uint256)
  };

Record with Arrays

Types
  Record Proposal := {
      proposal_id: uint256;
      description: string;
      votes_for: array address;
      votes_against: array address;
      executed: boolean
  };

Record with Optionals

Types
  Record Config := {
      max_supply: optional uint256;
      owner: optional address;
      paused: boolean
  };

Type Resolution

When referencing user-defined types in contract state, use _ResolveName:

Record Contract := {
    user: (_ResolveName "User");
    users: mapping address (_ResolveName "User");
    status: (_ResolveName "Status")
}.

This ensures proper type resolution during code generation.

Best Practices

1. Use Contract Types Section

Good:

Types
  Record User := { ... };

Avoid:

GlobalGeneratePruvendoRecord ...

2. Meaningful Field Names

Good:

Record User := {
    user_id: uint256;
    balance: uint256;
    is_active: boolean
}.

Avoid:

Record User := {
    x: uint256;
    y: uint256;
    z: boolean
}.

3. Group Related Data

Good:

Record Transaction := {
    from: address;
    to: address;
    amount: uint256;
    timestamp: uint256
}.

Avoid:

(* Scattered fields in contract state *)
Record Contract := {
    tx_from: address;
    some_other_field: uint256;
    tx_to: address;
    tx_amount: uint256
}.

See Also

• Types and Primitives - Built-in types
• Contract Structure - Using types in contracts
• Simple Contract Example - Complete example