This small tutorial will explain you how to play with MPgram, by creating a small example: the dependent type family So .
The type constructor So has kind " ∀ b : Bool => * ", and this type family has unique null-ary data constructor oh : So true . In Epigram, you will define it like following:
(Screenshot from Durham Epigram)
Step 1. Creating a node
To write a declaration, you should first create a root node, as shown in the following screenshot. Right-click on the model and choose Create Root Node -> Epigram -> DeclarationContainer.
Step 2. Choosing a declaration
MPgram creates new DeclarationContainer with three-coloured icon and makes an empty cell in the editor pane. You can type anything you like in that cell, but you'd better type either data, let or inspect . We'll choose to type data here.
Then, just press space. Something has happened: MPgram has understood what you meant, and created new empty data-where declaration.
Step 3. Writing a signature for the type constructor
Then, set cursor to the words "no signatures" inside the brackets and press Ctrl-Enter. Ctrl-Enter is used in MPS to create new nodes in a collection. Now you can see that the editor has created a new placeholder for a signature.
Choose a kind of the signature by pressing Ctrl-Space. We'll choose simple one now.
The editor responds with an empty signature which looks like colon between a placeholder for identifier and a placeholder for type expression.
Type any name you like for an identifier (we choose "b"). Then choose a known expression for type by pressing Ctrl-Space. Unfortunately, we haven't defined Bool yet. So we'll introduce this name (choose (introduce) ).
MPgram creates a cell for a new identifier. MPgram doesn't know its arity, hence it makes an empty collection for identifiers' parameters.
Type Bool as a name for newly created identifier.
Now it's time for naming our type constructor. Type So in the appropriate cell.
Then create a new parameter placeholder (Ctrl-Enter on (no parameters) ). Finish with choosing a parameter (Ctrl-Space). It's only one parameter available here, and it is "b".
Look at the tab. Its name has changed from DeclarationContainer to So.
Step 4. Defining data constructors
Let's create a signature for a data constructor. Press Ctrl-Enter on (no signatures). You've learnt the purpose of Ctrl-Enter, haven't you?
Press Ctrl-Space on the placeholder which has just appeared and choose deduction now.
New deduction rule has appeared just now.
And you can see the type expression already written in it, which is So applied to an empty placeholder.
Now name new data constructor as "oh" and let's type a parameter, yet remained undefined, of So . We want it to be "true", but we haven't defined what is "true". Hence we'll introduce that name, just like Bool before.
And this is what we'll get:
Step 5. Defining unknown identifiers introduced before
Now we have a data-where declaration for the So type family. But the names Bool and true, though visible, still remain unknown. We have to define these names. Let's declare the Bool type family.
Create new DeclarationContainer and make it a data-where declaration, just like we did it before to create the declaration for So. Fill in the cells in the data clause by yourself and continue with creating a new signature in the where clause.
Create a simple signature for true data constructor. Press Ctrl-Enter on this signature to create one more signature.
Press Ctrl-Enter on the placeholder just appeared, choose simple and finish our declaration with writing a simple signature for false data constructor.
Step 6. Replacing unknown identifiers with newly defined ones
Well, we've just defined the Bool type family. But MPgram still doesn't know that our Bool and that unknown "Bool" in the declaration for So are the same. It's not difficult to make MPgram know about that.
Just set cursor after the word "Bool" in the definition for Bool type constructor and press space. By doing that, you tell MPgram that you want to replace all usages of an unknown identifier with the name "Bool" with this legally defined identifier Bool. If there's any identifier with the name "Bool" such that Bool type constructor is visible from every usage of that identifier, MPgram will perform such replacement.
Ditto with true.
Now look at the declaration for So. There's no cell now where empty collection of parameters for identifiers Bool and true used to be (the (parameters...) cells). The replacement was a success. Well, if the arity of Bool or true was more than 0, the appropriate number of parameters' placeholders would appear after Bool or true, respectively.
Now these "Bool" and "true" are that very Bool and true we have just defined. To be sure, you can press now Ctrl-B on "Bool" or on "true" - and MPgram should go to the definition of this name.
Step 7. Sending declaration to Epigram elaborator
We have succesfully written a full definition of So type family. Let's send it to Epigram, to be sure that we have written a well-typed piece of program. If we have not, we'll receive an error message after sending the declaration to the Epigram elaborator.
Select the whole DeclarationContainer for So, either by pressing Ctrl-UpArrow several times or double-clicking the "So" node in the tree view which is situated in the north-west corner. You'll see that a button have appeared in the inspector pane. Press it to send our declaration to Epigram. (Red spot in the following screenshot marks this button).
You see some output in the tools pane. What does it mean? First, there are no error messages - that means our declaration is well-typed. Then, you see that several nodes were sent to Epigram. Though you have pressed only one button hence asked to send only declaration of So, MPgram have sent all required declarations to Epigram in the right order. In our case, MPgram have sent Bool before sending So.
Congratulations! You've written the full definition of So type family and have successfully sent it to the Epigram elaborator.