Disco files and the disco REPL¶
For anything beyond simple one-off calculations that can be entered at the disco prompt, disco definitions may be stored in a file which can be loaded into the REPL.
Disco files typically end in
Here is a simple example:
approx_pi : Rational approx_pi = 22/7 increment : N -> N increment(n) = n + 1
This file contains definitions for
Each definition consists of a type signature of the form
<type>, followed by an equality of the form
<expression>. Both parts of a definition are required; in
particular, if you omit a type signature, disco will complain that the
name is not defined. The example file shown above contains two
approx_pi is defined to be the
increment is defined to be the function which
outputs one more than its natural number input. (Functions and the
syntax for defining them will be covered in much more detail in an
upcoming section of the tutorial.)
The order of definitions in a
.disco file does not matter;
each definition may refer to any other definition in the whole file.
To load the definitions in a file into the disco REPL, you can use the
:load command. After successfully loading a file, all the names
defined in the file are available for use; the
:names command can
be used to list all the available names. For example:
Disco> :load example/basics.disco Loading example/basics.disco... Loaded. Disco> :names approx_pi : ℚ increment : ℕ → ℕ Disco> approx_pi 22/7 Disco> increment(3) 4 Disco> :type increment increment : ℕ → ℕ Disco> approx_pi + increment(17) 148/7
(If you want to follow along, note that the above interaction assumes that the disco REPL was run from the docs/tutorial subdirectory.)
Other REPL commands¶
The disco REPL has a few other commands which are useful for disco developers.
:parseshows the fully parsed form of an expression.
Disco> :parse 2 + [3,4 : Int] TBin_ () Add (TNat_ () 2) (TContainer_ () ListContainer [(TNat_ () 3,Nothing),(TAscr_ () (TNat_ () 4) (Forall (<> TyAtom (ABase Z))),Nothing)] Nothing)
:prettyshows the pretty-printed form of a term (without typechecking it).
Disco> :pretty 2 + [3,4:Int] 2 + [3, (4 : ℤ)]
:desugarshows the desugared term corresponding to an expression.
Disco> :desugar [3,4] 3 :: 4 :: 
:compileshows the compiled core language term corresponding to an expression.
Disco> :compile [3 - 4] CCons 1 [CApp (CConst OAdd) [(Lazy,CCons 0 [CNum Fraction (3 % 1),CApp (CConst ONeg) [(Strict,CNum Fraction (4 % 1))]])],CCons 0 ]
Comments and documentation¶
Comments in disco have a similar syntax to Haskell, with the exception that only single-line comments are supported, and not multi-line comments. In particular, two consecutive hyphens
--will cause disco to ignore everything until the next newline character.
Comments can be placed anywhere and are literally ignored by disco. In many cases, however, the purpose of a comment is to provide documentation for a function. In this case, disco supports special syntax for documentation, which must be placed before the type signature of a definition. Each line of documentation must begin with
|||(three vertical bars).
When this file is loaded into the disco REPL, we can use the
:doccommand to see the documentation associated with each name.
fizzdoes not have any associated documentation, the
:doccommand simply shows its type.