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 : x period period period right-arrow x x period period period
  • dupn : n x 0 period period x Subscript n Baseline period period period right-arrow x Subscript n Baseline x 0 period period x Subscript n Baseline period period period
swap / swapn

Swaps the top element of the stack with the second, or the nth element.

  • swap : x y period period period right-arrow y x period period period
  • swapn : n x y 0 period period y Subscript n Baseline period period period right-arrow y Subscript n Baseline y 0 period period y Subscript n minus 1 Baseline x period period period
shift / shaft

Shifts the nth element towards the top, or shaft the top to the nth place.

  • shift : n x 1 period period x Subscript n Baseline period period period right-arrow x Subscript n Baseline x 1 period period x Subscript n minus 1 Baseline period period period
  • shaft : n x 1 period period x Subscript n Baseline period period period right-arrow x 2 period period x Subscript n Baseline x 1 period period period
pop / popn

Pops the top element, or the nth top element, off the stack.

  • pop : x period period period right-arrow period period period
  • popn : n x 0 period period x Subscript n Baseline period period period right-arrow x 0 period period x Subscript n minus 1 Baseline period period period
clear

Clears the stack.

  • clear : period period period right-arrow
stack / set-stack

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 : upper S t a c k right-arrow left-bracket upper S t a c k right-bracket upper S t a c k
  • set-stack : left-bracket upper S t a c k right-bracket period period period right-arrow upper S t a c k
pick

Picks the i-between-nth element of the stack, and discards all others. Can be useful for implementing arbitrary switch-like control-flow.

  • pick : i n x 0 period period x Subscript i Baseline period period x Subscript n minus 1 Baseline period period period right-arrow x Subscript i Baseline period period period

Names and variables

def

Sets the value of a variable.

  • def : v a l u e n a m e period period period right-arrow period period period in an environment where v a l u e is associated with the variable named n a m e .

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.

  • $ : n a m e period period period right-arrow normal dollar-sign n a m e period period period
vocabulary / set-vocabulary

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 calling vocabulary).

First-class 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 to f itself. That is, evaluating a symbol is no different than looking it up in the current dictionary, and executing its value.

Lists

[

Puts a “list beginning” (LB) marker on the stack

  • [ : period period period right-arrow upper L upper B period period period
]

Creates a list of the elements on the stack until the next “list beginning” marker, and pushes it on the remaining stack.

  • ] : x 0 period period x Subscript n Baseline upper L upper B period period period right-arrow left-bracket x Subscript n Baseline period period x 0 right-bracket period period period
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 n minus 1 , n being the top element of the stack.

  • range : n period period period right-arrow left-bracket 0 period period n minus 1 right-bracket period period period

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 negative 1 , if positive produces 1 , otherwise produces 0 .

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

"

to-int

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.

String-Indexed Dictionaries

empty

Pushes the empty dictionary onto the stack.

insert

Given a dictionary d, a key k and a value v, inserts the value v at k in d, then pushes the result on the stack.

delete

The reverse of insert. Given a dictionary d and a key k, produce a dictionary d' that is identical to d, without any association for k.

keys

Given a dictionary d, pushes a list of all of d’s keys onto the stack.

Constructing typed terms

universe

Produces a universe.

  • universe : i period period period right-arrow upper S e t Subscript i Baseline period period period
variable

Given a variable name, that exists in the current type context, produces that variable.

  • variable : n a m e period period period right-arrow v a r left-parenthesis n a m e right-parenthesis period period period
apply

Given a function f, and a term x, produces the term f x.

  • apply : x f period period period right-arrow left-parenthesis f x right-parenthesis period period period
lambda / forall

Abstracts the last hypothesis in context for the term at the top of the stack. That hypothesis is abstracted repectively as a lambda-abstraction, or a product.

  • lambda : left-parenthesis normal upper Gamma comma h colon upper T Subscript h Baseline right-tack x right-parenthesis period period period right-arrow left-parenthesis normal upper Gamma right-tack left-parenthesis lamda left-parenthesis h colon upper T Subscript h Baseline right-parenthesis period x right-parenthesis right-parenthesis period period period
  • forall : left-parenthesis normal upper Gamma comma h colon upper T Subscript h Baseline right-tack x right-parenthesis period period period right-arrow left-parenthesis normal upper Gamma right-tack left-parenthesis for-all left-parenthesis h colon upper T Subscript h Baseline right-parenthesis comma x right-parenthesis right-parenthesis period period period
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 : x period period period right-arrow mu left-parenthesis x right-parenthesis period period period
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 : t a g upper T period period period right-arrow upper A x i o m Subscript upper T comma t a g Baseline period period period

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 :

  • k Subscript upper S e t Baseline k Subscript lamda Baseline k Subscript for-all Baseline k Subscript a p p l y Baseline k Subscript mu Baseline k Subscript v a r Baseline k Subscript a x i o m Baseline match :
  • vertical-bar normal upper Gamma right-tack left-parenthesis lamda left-parenthesis x colon upper T Subscript x Baseline right-parenthesis period y right-parenthesis period period period right-arrow k Subscript lamda Baseline left-parenthesis normal upper Gamma comma x colon upper T Subscript x Baseline right-tack x y period period period right-parenthesis
  • vertical-bar normal upper Gamma right-tack left-parenthesis for-all left-parenthesis x colon upper T Subscript x Baseline right-parenthesis period y right-parenthesis period period period right-arrow k Subscript for-all Baseline left-parenthesis normal upper Gamma comma x colon upper T Subscript x Baseline right-tack x y period period period right-parenthesis
  • vertical-bar left-parenthesis f x 1 period period x Subscript n Baseline right-parenthesis period period period right-arrow k Subscript a p p l y Baseline left-parenthesis left-bracket x 1 period period x Subscript n Baseline right-bracket f period period period right-parenthesis
  • vertical-bar mu left-parenthesis x right-parenthesis period period period right-arrow k Subscript mu Baseline left-parenthesis x period period period right-parenthesis
  • vertical-bar x period period period right-arrow k Subscript v a r Baseline left-parenthesis n a m e left-parenthesis x right-parenthesis period period period right-parenthesis
  • vertical-bar upper A x i o m Subscript upper T comma t a g Baseline period period period right-arrow k Subscript a x i o m Baseline left-parenthesis t a g upper T period period period right-parenthesis
  • vertical-bar upper S e t Subscript n Baseline period period period right-arrow k Subscript upper S e t Baseline left-parenthesis n period period period right-parenthesis
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 upper T and a name upper H , adds a new hypothesis upper H of type upper T to the context. Alternately, you can give a second hypothesis name upper H prime , in which case the new hypothesis will be introduced before upper H prime .

intro :
- vertical-bar normal upper Gamma right-tack n a m e left-parenthesis upper H right-parenthesis upper T period period period right-arrow normal upper Gamma comma upper H colon upper T right-tack period period period
- vertical-bar normal upper Gamma comma upper H prime colon upper T Subscript upper H Sub Superscript prime Subscript Baseline comma normal upper Delta right-tack n a m e left-parenthesis upper H Superscript prime Baseline right-parenthesis n a m e left-parenthesis upper H right-parenthesis upper T period period period right-arrow normal upper Gamma comma upper H colon upper T comma upper H prime colon upper T Subscript upper H Sub Superscript prime Subscript Baseline comma normal upper Delta right-tack period period period

extro-lambda / extro-forall

Clears the last hypothesis from the context. Every term that references that hypothesis is abstracted either as a lambda-expression, 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.