-
Notifications
You must be signed in to change notification settings - Fork 0
REPL
Viper provides a REPL very similar to Python's. To access it, run ./viper.py
from the repository's root directory:
$ ./viper.py
>>>
The prompt >>>
indicates that Viper is ready to process your input. (You can quit at any time by pressing CTRL+d.)
From here, you can pass code to be evaluated. For example:
>>> 1 + 1
2
>>> print("Hello, world!")
Hello, world!
To process multi-line input, you must enter multi-line mode using :{
and :}
(similar to Haskell's GHCi):
>>> :{
... def say_hi() -> None:
... print("Hi!")
... :}
>>> say_hi()
Hi!
>>>
At some point in the future it is likely the REPL will support multi-line input, but I haven't gotten there yet.
The Viper REPL supports certain configuration operations during runtime, accessed via the :set
command.
The REPL supports multiple modes of execution:
- Lex mode, which outputs the raw lexemes
- Parse mode, which outputs the shared packed parse forest
- Eval mode, which evaluates the result of terms and prints that result to the console
- Exec mode, which commits the execution to the current environment and store (preserving evaluations)
By default, the REPL runs in mode 1100
, which corresponds to having both the Exec and Eval modes enabled.
To see the current mode, do:
>>> :set mode
:set mode: 1100
The mode can be set either numerically:
>>> :set mode 0001
>>>
or by using a system of flags. A flag can be prepended by either a +
or -
and are evaluated from left to right. The flags are:
Flag | Mode |
---|---|
a | all |
l | lex |
p | parse |
e | eval |
x | exec |
So to remove all existing flags and set the parse and exec flags:
>>> :set mode -a +px
>>> :set mode
:set mode: 1010
Lexing and parsing both have short-form single-line switches that can be used so that you don't have to change the mode of interpretation for the remainder of your session.
To lex a line, simply use :lex
or :l
at the front:
>>> :lex 4 + 3
[Int(4), Operator(+), Int(3)]
>>>
Parsing can be done with either :parse
or :p
:
>>> :parse 4 + 3
SingleLine
└─TestExprList
└─[]
└─TestExpr
└─OrTestExpr
└─[]
└─AndTestExpr
└─[]
└─NotNegatedTestExpr
└─OpExpr
├─None
├─AtomExpr
│ ├─IntAtom
│ │ └─Int(4)
│ └─[]
├─[]
│ └─SubOpExpr
│ ├─Operator(+)
│ └─AtomExpr
│ ├─IntAtom
│ │ └─Int(3)
│ └─[]
└─None
>>>
These are equivalent to temporarily switching modes to 0001
(for lexing) or 0010
(for parsing).
If an error is raised internally during evaluation, by default it will be handled and the short message will be output to the console for you. Consider the following example where the variable x
is used though it has never been defined:
>>> x
KeyError: 'No such name in environment: x'
>>>
This behavior can be disabled by inputting the following command:
>>> :set exceptions off
>>> x
Traceback (most recent call last):
...
KeyError: 'No such name in environment: x'
$
Notice that the full traceback is printed (I truncated it here because it's very long) and you are returned to the shell — not the REPL. This can be useful for debugging while development is ongoing.
Viper's memory is managed as a pair of an environment and a store. The environment maps names (variables) to addresses, and the store maps addresses to values.
Both the environment and store are transparently visible to the user.
To read the entire environment, input either :env
or :e
:
>>> x = 3
>>> :env
[{'print': 0, '+': 1, '-': 2, '*': 3, '/': 4, '==': 5, 'x': 6}]
>>>
Specific elements can be searched for by providing a name as argument:
>>> :env x
env[x]: 6
>>>
The store can be accessed similarly to the environment, except that either a name or an address can be provided to do lookups:
...
>>> :store
Store(7, {0: ForeignCloVal((s), {}), 1: ForeignCloVal((a, b), {}), 2: ForeignCloVal((a, b), {}), 3: ForeignCloVal((a, b), {}), 4: ForeignCloVal((a, b), {}), 5: ForeignCloVal((a, b), {}), 6: IntVal(3)})
>>> :store x
store[env[x]]: IntVal(3)
>>> :store 6
store[6]: IntVal(3)
As of this writing, types are not supported in Viper. However, types will be supported, and they will be queryable just like in Haskell using either :type
or :t
:
>>> :type 5
Error: Type checking not supported at this time.
>>>