The CaPriCon Scripting Language Reference
All the basic words are described below.
Stack manipulation
The environment of the interpreter consists mostly of a stack of values, that can be manipulated with the following words.
dup
/dupn
Duplicates the top element, or the nth top element of the stack.
dup
:
dupn
:
swap
/swapn
Swaps the top element of the stack with the second, or the nth element.
swap
:
swapn
:
shift
/shaft
Shifts the nth element towards the top, or shaft the top to the nth place.
shift
:
shaft
:
pop
/popn
Pops the top element, or the nth top element, off the stack.
pop
:
popn
:
clear
Clears the stack.
clear
:
stack
/setstack
Pushes the current stack, as a list, on top of the current stack. In the second case, sets the top element of the stack as the new stack.
stack
:setstack
:
pick
Picks the ibetweennth element of the stack, and discards all others. Can be useful for implementing arbitrary switchlike controlflow.
pick
:
Names and variables
def
Sets the value of a variable.
def
: in an environment where is associated with the variable named .
Examples :
(x + y) * y = 70; y = 7 ; x = 3$
The inverse of
def
. Given the name of a variable at the top of the stack, this function produces the value of the corresponding variable in the current environment.$
:
vocabulary
/setvocabulary
Pushes the active dictionary, that contains all defined variables, on top of the stack. In the second case, make the top of the stack the current dictionary, redefining all variables at once.
lookup
A more flexible version of
$
, where the environment is specified explicitly as a second argument (for example, from callingvocabulary
).
Firstclass functions
exec
Executes the value at the top of the stack, as if it were the meaning of a word. To illustrate, given a function,
'f $ exec
is equivalent tof
itself. That is, evaluating a symbol is no different than looking it up in the current dictionary, andexec
uting its value.
Lists
[
Puts a â€ślist beginningâ€ť (LB) marker on the stack
[
:
]
Creates a list of the elements on the stack until the next â€ślist beginningâ€ť marker, and pushes it on the remaining stack.
]
:
each
Iterates over each element of its second argument, pushing it on the stack and running its second argument afterward.
Examples :
Values: 1 2 3
range
Create a list of numbers from 0 to , being the top element of the stack.
range
:
Simple integer arithmetic
+
,
,*
,div
,mod
Performs the usual binary arithmetic operation on the top two elements of the stack, and replaces them with the result.
sign
Computes the sign of the top stack element. If the sign is negative, produces , if positive produces , otherwise produces .
Strings
format
Much like the
sprintf()
function in C, produces a string which may contain textual representations of various other values.Examples :
"1: Some text
"
toint
Tries to convert the top stack element to an integer, if possible.
Interacting with the environment
exit
Exits the interpreter, immediately and unconditionally.
print
Print the string at the top of the stack into the current document.
source
Opens an external source file, and pushes a quote on the stack with its contents.
cache
Given a resource name and a quote, does one of two things :
 if the resource already exists, try to open it as a CaPriCon object, ignoring the quote
 otherwise, run the quote and store its result in the resource for future use
After the builtin has run, the contents of the requested object can be found at the top of the stack.
redirect
Given a resource name and a quote, executes the quote, redirecting its output to the resource.
StringIndexed Dictionaries
empty
Pushes the empty dictionary onto the stack.
insert
Given a dictionary
d
, a keyk
and a valuev
, inserts the valuev
atk
ind
, then pushes the result on the stack.delete
The reverse of
insert
. Given a dictionaryd
and a keyk
, produce a dictionaryd'
that is identical tod
, without any association fork
.keys
Given a dictionary
d
, pushes a list of all ofd
â€™s keys onto the stack.
Constructing typed terms
universe
Produces a universe.
universe
:
variable
Given a variable name, that exists in the current type context, produces that variable.
variable
:
apply
Given a function
f
, and a termx
, produces the termf x
.apply
:
lambda
/forall
Abstracts the last hypothesis in context for the term at the top of the stack. That hypothesis is abstracted repectively as a lambdaabstraction, or a product.
lambda
:
forall
:
mu
Produces an inductive projection to a higher universe for the term at the top of the stack, if that term is of an inductive type.
mu
:
axiom
Given a combinatorial type (a type without free variables) and an associated tag, produce an axiom with that tag, that can serve as a proof of the given type.
axiom
:
Analysing typed terms
type
Computes the type of the term at the top of the stack.
match
Given a quote for each possible shape, and a term, executes the corresponding quote :

match
:







extract
Extract the term at the top of the stack into an abstract algebraic representation, suitable for the production of foreign functional code, such as OCaml or Haskell.
Managing the type context
intro
Given a type and a name , adds a new hypothesis of type to the context. Alternately, you can give a second hypothesis name , in which case the new hypothesis will be introduced before .
intro
:

extrolambda
/extroforall
Clears the last hypothesis from the context. Every term that references that hypothesis is abstracted either as a lambdaexpression, or as a product, depending on the variant that was called.
rename
Renames a hypothesis. This function takes two parameters : a hypothesis name, and the new name to give it.
substitute
Given a hypothesis name, and a term of the same type as that hypothesis, remove that hypothesis from the context by substituting all its occurences by the given term.
hypotheses
Pushes a list of all the hypothesesâ€™ names in context, from most recent to the oldest.