REPL - Interactive Development

The Coq REPL (Read-Eval-Print Loop) is your primary interface for developing Ursus contracts. It provides immediate feedback, interactive exploration, and powerful debugging capabilities.

What is the REPL?

The REPL is an interactive environment where you can:

Load contract files - Import and compile Ursus code
Execute commands - Run Coq commands interactively
Inspect definitions - Examine types, values, and proofs
Test functions - Evaluate expressions
Develop incrementally - Build code step by step

Starting the REPL

CoqIDE

Launch CoqIDE:

coqide MyContract.v &

Features:

Graphical interface
Step-by-step execution
Goal visualization
Syntax highlighting

Proof General (Emacs)

Launch Emacs with Proof General:

emacs MyContract.v

Key bindings:

C-c C-n - Execute next command
C-c C-u - Undo last command
C-c C-RET - Execute to cursor
C-c C-b - Execute buffer

VSCode with VSCoq

Install VSCoq extension:

code --install-extension maximedenes.vscoq

Features:

Modern IDE experience
Inline goal display
Error highlighting
Auto-completion

Command Line (coqtop)

Start interactive session:

coqtop -Q . MyProject

Basic commands:

Coq < Load MyContract.
Coq < Check transfer.
Coq < Print Contract.
Coq < Quit.

Loading Contracts

Load Single File

Load "MyContract.v".

Load with Dependencies

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.
Require Import MyContract.

Set Load Path

Add LoadPath "/path/to/ursus" as Ursus.
Require Import Ursus.MyContract.

Interactive Commands

Inspection Commands

Check type:

Check transfer.
(* transfer : address -> uint256 -> UExpression boolean false *)

Print definition:

Print transfer.
(* Shows full definition *)

Print contract:

Print Contract.
(* Shows contract record structure *)

Search for definitions:

Search uint256.
Search "balance".
SearchAbout mapping.

Evaluation Commands

Compute expression:

Compute {42} + {58}.
(* = {100} : URValue uint256 false *)

Evaluate function:

Eval compute in (add_numbers {10} {20}).

Simplify term:

Eval simpl in (balances[[addr]]).

Developing Functions Interactively

Step-by-Step Development

1. Start function definition:

Ursus Definition myFunction (x: uint256): UExpression uint256 false.

REPL shows:

1 subgoal
______________________________________(1/1)
UExpression uint256 false

2. Add first statement:

{
    refine // var 'y : uint256 := x + {1} ; _ //.

REPL shows:

1 subgoal
y : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

3. Complete function:

    refine // y //.
}
return.
Defined.

REPL confirms:

myFunction is defined

Using Show Command

Inspect current goal at any point:

{
    ::// var 'x : uint256 := {42} .
    Show.  (* Display current goal *)
    ::// var 'y : uint256 := x * {2} .
    Show.  (* Display updated goal *)
    ::// _result := y |.
}

Using Proof Mode

Enter proof mode for complex logic:

Ursus Definition complexFunction (x: uint256): UExpression uint256 false.
Proof.
    (* Use tactics *)
    unfold UExpression.
    intro s.
    (* Build term step by step *)
    ...
Defined.

Debugging in the REPL

Inspect Context

Show all variables:

Show.

Output:

1 subgoal
x : ULValue uint256
y : ULValue uint256
balance : ULValue uint256
______________________________________(1/1)
UExpression boolean false

Type Checking

Check expression type:

Check (x + y).
(* URValue uint256 false *)

Check (balances[[addr]]).
(* ULValue uint256 *)

Simplification

Simplify complex expressions:

Eval simpl in (balances[[addr]] + {100}).

Error Messages

When you make a mistake, the REPL shows detailed errors:

::// balance := "hello" .

Error:

Error: The term "hello" has type "string"
while it is expected to have type "uint256".

Common REPL Workflows

Workflow 1: Exploratory Development

(* Load contract *)
Load "MyContract.v".

(* Check existing functions *)
Check transfer.
Print transfer.

(* Test ideas *)
Check (balances[[addr]] + {100}).

(* Develop new function *)
Ursus Definition newFunction ...

Workflow 2: Test-Driven Development

(* Define property *)
Theorem transfer_correct:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    balance s' to = balance s to + amount.
Proof.
  (* Develop proof interactively *)
  intros.
  unfold exec_transfer.
  simpl.
  ...
Qed.

(* Implement function to satisfy property *)
Ursus Definition transfer ...

(* Start with stub *)
Ursus Definition myFunction (x: uint256): UExpression uint256 false.
{
    ::// skip_ |.
}
return {0}.
Defined.

(* Test compilation *)
Sync.

(* Refine implementation *)
(* ... edit and reload ... *)

REPL Tips and Tricks

Tip 1: Use Undo

Made a mistake? Undo last command:

CoqIDE: Click "Backward" or Ctrl+U Proof General: C-c C-u coqtop: Undo. or Restart.

Tip 2: Save State

Save your progress:

(* In file MyContract.v *)
Ursus Definition myFunction ...
Defined.
Sync.

(* Save file, reload in REPL *)
Load "MyContract.v".

Tip 3: Quick Testing

Test expressions without defining functions:

Check ({42} + {58}).
Compute ({42} + {58}).

Tip 4: Use Locate

Find where something is defined:

Locate "->".
Locate uint256.
Locate UExpression.

Tip 5: Set Options

Configure REPL behavior:

Set Printing All.        (* Show implicit arguments *)
Unset Printing Notations. (* Show raw terms *)
Set Printing Depth 100.  (* Control output depth *)

URSUS language Documentation