forked from codesandbox/codesandbox-client
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathmonarch.html
More file actions
4308 lines (3661 loc) · 166 KB
/
monarch.html
File metadata and controls
4308 lines (3661 loc) · 166 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta charset="utf-8">
<meta name="viewport" content="width=device-width">
<title>Monaco Editor Monarch</title>
<link data-inline="yes-please" href="./lib/bootstrap-cosmo.css" rel="stylesheet">
<link data-inline="yes-please" href="./lib/bootstrap-responsive.min.css" rel="stylesheet">
<link data-inline="yes-please" href="./all.css" rel="stylesheet" type="text/css">
<link data-inline="yes-please" href="./monarch/monarch.css" rel="stylesheet" />
<link data-name="vs/editor/editor.main" rel="stylesheet" href="../release/dev/vs/editor/editor.main.css">
</head>
<body>
<nav class="navbar navbar-inverse navbar-fixed-top">
<div class="navbar-inner">
<div class="container">
<div class="logo">
<a href="index.html">Monaco Editor</a>
</div>
<!-- collapse button for smaller screens -->
<button type="button" class="btn btn-navbar" data-toggle="collapse" data-target=".nav-collapse">
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
</button>
<!-- navbar title -->
<div class="nav-collapse collapse">
<ul class="nav">
<li><a class="nav-item" href="index.html">Home</a></li>
<li><a class="nav-item" href="api/index.html">API Doc</a></li>
<li><a class="nav-item" href="playground.html">Playground</a></li>
<li><a class="nav-item" href="monarch.html">Monarch</a></li>
<li><a class="nav-item" target="_blank" href="https://registry.npmjs.org/monaco-editor/-/monaco-editor-{{version}}.tgz">Download {{version}}</a></li>
</ul>
</div>
</div>
</div>
</nav>
<section id="monarch">
<!--******************************************
Main elements
**********************************************-->
<div id="main">
<div id="header"><img src="monarch/monarch-34px.png" id="logo"></img>Monarch Documentation
</div>
<div id="leftPane">
<div class="paneheader">Language syntax definition
<span class="selectbox">
Sample: <select id="sampleselect">
<option>mylang</option>
<option>java</option>
<option>javascript</option>
<option>python</option>
<option>csharp</option>
<option>xdot</option>
<option>koka</option>
<option disabled=true></option>
<option>boogie</option>
<option>chalice</option>
<option>dafny</option>
<option>formula</option>
<option>smt2</option>
<option>specsharp</option>
<option>z3python</option>
<option disabled=true></option>
<option>html</option>
<option>markdown</option>
<option>ruby</option>
</select>
</span>
</div>
<div id="langPane"></div>
<div id="commandbar">Generate:
</div>
</div>
<div id="rightPane">
<div class="paneheader">Language editor
<span class="arrowdown" style="display:none">▼</span>
<span class="selectbox">
Theme: <select id="themeselect">
<option>vs</option>
<option>vs-dark</option>
</select>
</span>
</div>
<div id="editor"></div>
<div id="monarchConsole"></div>
</div>
<!--******************************************
Documentation
**********************************************-->
<!-- <div id="footer">
Documentation <span class="arrowdown">▼</span>
</div>-->
<div id="documentation">
<h2>Monarch: create declarative syntax highlighters using JSON</h2>
<p>This document describes how to create a syntax highlighter using the
Monarch library. This library allows you to specify an efficient syntax highlighter, using a declarative lexical specification (written as a JSON value). The specification is expressive enough to specify sophisticated highlighters with complex state transitions, dynamic brace matching, auto completion, other language embeddings, etc. as shown in the 'advanced' topic sections of this document. On a first read, it is safe to skip any section or paragraph marked as <span class="adv">(Advanced)</span> since many of the advanced features are rarely used in most language definitions.<br>
– Daan Leijen.
</p>
<h2>Creating a language definition</h2>
<p>A language definition is basically just a JSON value describing various properties of your language. Recognized attributes are:</p>
<dt>ignoreCase</dt><dd>(optional=<code>false</code>, boolean) Is the language case insensitive?. The regular expressions in the tokenizer use this to do case (in)sensitive matching, as well
as tests in the <code>cases</code> construct.</dd>
<dt>defaultToken</dt><dd>(optional=<code>"source"</code>, string) The default token returned if nothing matches in the tokenizer. It can be convenient to set this to <code>"invalid"</code> during development of your colorizer to easily spot what is not matched yet.</dd>
<dt id="brackets">brackets</dt><dd>(optional, array of bracket definitions) This is used by the tokenizer to easily define matching braces. See <a href="#@brackets"><code class="dt">@brackets</code></a> and <a href="#bracket"><code class="dt">bracket</code></a> for more information. Each bracket definition is an array of 3 elements, or object, describing the <code>open</code> brace, the <code>close</code> brace, and the <code>token</code> class. The default definition is:
<pre class="highlight">
[ ['{','}','delimiter.curly'],
['[',']','delimiter.square'],
['(',')','delimiter.parenthesis'],
['<','>','delimiter.angle'] ]</pre>
</dd>
<dt>tokenizer</dt><dd>(required, object with states) This defines the tokenization rules – see the next section for a detailed description.</dd>
</dl>
<p>There are more attributes that can be specified which are described in the <a href="#moreattr">advanced attributes</a> section later in this document.</p>
<h2>Creating a tokenizer</h2>
<p>The <code>tokenizer</code> attribute describes how lexical analysis takes place, and how the input is divided into tokens. Each token is given a CSS class name which is used to render each token in the editor. Standard CSS token classes include:</p>
<pre class="highlight" type="text/plain">
identifier entity constructor
operators tag namespace
keyword info-token type
string warn-token predefined
string.escape error-token invalid
comment debug-token
comment.doc regexp
constant attribute
delimiter .[curly,square,parenthesis,angle,array,bracket]
number .[hex,octal,binary,float]
variable .[name,value]
meta .[content]</pre>
<p>Note: The token classes in the third column are currently only highlighted correctly if you include the <code>monarch.css</code> style file (Aug 2012).</p>
<h3>States</h3>
<p>A tokenizer consists of an object that defines states. The initial state of the tokenizer is the first state defined in the tokenizer. When a tokenizer is in a certain state, only the rules in that state will be applied. All rules are matched in order and when the first one matches its action is used to determine the token class. No further rules are tried. Therefore, it can
be important to order the rules in a way that is most efficient, i.e. whitespace and identifiers first.</p>
<p><span class="adv">(Advanced)</span> A state is interpreted as dot (<code>.</code>) separated sub-states. When looking up the rules for a state, the tokenizer first tries the entire state name, and then looks at its parent until it finds a definition. For example, in our example, the states <code>"comment.block"</code> and <code>"comment.foo"</code> would both be handled by the <code>comment</code> rules. Hierarchical state names can be used to maintain complex lexer states, as shown for example in the section on <a href="#htmlembed">complex embeddings</a>.</p>
<h3>Rules</h3>
<p>Each state is defined as an array of rules which are used to match the input.
Rules can have the following form:</p>
<dl>
<dt>[<em>regex</em>, <em>action</em>]</dt><dd>Shorthand for <code>{ regex: <em>regex</em>, action: <em>action</em> }</code></dd>
<dt>[<em>regex</em>, <em>action</em>, <em>next</em>]</dt><dd>Shorthand for <code>{ regex: <em>regex</em>, action: <em>action</em>{next: <em>next</em>} }</code></dd>
<dt>{regex: <em>regex</em>, action: <em>action</em> }</dt><dd>When <code><em>regex</em></code> matches against the current input, then <code><em>action</em></code> is applied to set the token class. The regular expression <code><em>regex</em></code> can be either a regular expression (using <code>/<em>regex</em>/</code>), or a string representing a regular expression. If it starts with a <code>^</code> character, the expression only
matches at the start of a source line. The <code>$</code> can be used to match against the end of a source line. Note that the tokenizer is not called when the end of the line is already reached, and the empty pattern <code>/$/</code> will therefore never match (but see <a href="#@eos"><code class="dt">'@eos'</code></a> too). Inside a regular expression, you can reference a string attribute named <code><em>attr</em></code> as <code>@<em>attr</em></code>, which is automatically expanded. This is used in the standard example to share the regular expression for escape sequences using <code>'@escapes'</code> inside the regular expression for characters and strings.
<p>Regular expression primer: common regular expression escapes we use are <code>\d</code> for <code>[0-9]</code>, <code>\w</code> for <code>[a-zA-Z0-9_]</code>, and <code>\s</code> for <code>[ \t\r\n]</code>. The notation <code><em>regex</em>{<em>n</em>}</code> stands for <code><em>n</em></code> occurrences of <code><em>regex</em></code>. Also, we use <code>(?=<em>regex</em>)</code> for non-consuming `followed by <code><em>regex</em></code>', <code>(?!<em>regex</em>)</code> for `not followed by', and <code>(?:<em>regex</em>)</code> for a non-capturing group (i.e. cannot use <code>$<em>n</em></code> to refer to it).</p>
</dd>
<dt>{ include: <em>state</em> }</dt><dd> Used for nice organization of your rules and expands to all the rules defined in <code><em>state</em></code>. This is pre-expanded and has no influence on performance. Many samples include the <code>'@whitespace'</code> state for example.</dd>
</dl>
<h3>Actions</h3>
<p>An action determines the resulting token class. An action can have the following forms:</p>
<dl>
<dt><em>string</em></dt><dd>Shorthand for <code>{ token: <em>string</em> }</code>.</dd>
<dt>[<em>action1</em>,...,<em>actionN</em>]</dt><dd>An array of N actions. This is only allowed when the regular expression consists of exactly N groups (ie. parenthesized parts). Due to the way the tokenizer works, you must define the groups in such a way that all groups appear at top-level and encompass the entire input, for example, we could define characters with an ascii code escape sequence as:
<pre class="highlight">/(')(\\(?:[abnfrt]|[xX][0-9]{2}))(')/, ['string','string.escape','string']]</pre>
<p>Note how we used a non-capturing group using <code>(?: )</code> in the inner group</p>
<dt id="token">{ token: <em>tokenclass</em> }</dt><dd>An object that defines the token class used with CSS rendering. Common token classes are for example <code>'keyword'</code>, <code>'comment'</code> or <code>'identifier'</code>. You can use a dot to use hierarchical CSS names, like <code>'type.identifier'</code> or <code>'string.escape'</code>. You can also include <code>$</code> patterns that are substituted with a captured group from the matched input or the tokenizer state. The patterns are described in the <a href="#pattern">guard section</a> of this document.
There are some special token classes:
<dl>
<dt id="@brackets">"@brackets"</dt> or
<dt>"@brackets.<em>tokenclass</em></dt><dd>Signifies that brackets were tokenized. The token class for CSS is determined by the token class defined in the <a href="#brackets"><code>brackets</code></a> attribute (together with <code><em>tokenclass</em></code> if present). Moreover, <a href="#bracket"><code class="dt">bracket</code></a> attribute is set such that the editor is matches the braces (and does auto indentation). For example:
<pre class="highlight">[/[{}()\[\]]/, '@brackets']</pre>
</dd>
<dt id="@rematch">"@rematch"</dt><dd><span class="adv">(Advanced)</span> Backs up the input and re-invokes the tokenizer. This of course only works when a state change happens too (or we go into an infinite recursion), so this is usually used in combination with the <code class="dt">next</code> attribute. This can be used for example when you are in a certain tokenizer state and want to get out when seeing certain end markers but don't want to consume them while being in that state. See also <a href="#nextEmbedded"><code class="dt">nextEmbedded</code></a>.</dd>
</dl>
<p>An action object can contain more fields that influence the state of a lexer. The following attributes are recognized:</p>
<dl>
<dt id="next">next: <em>state</em></dt><dd>(string) If defined it pushes the current state onto the tokenizer stack and makes <code><em>state</em></code> the current state. This can be used for example to start tokenizing a block comment:
<pre class="highlight">['/\\*', 'comment', '@comment' ]</pre>
<p>Note that this is a shorthand for</p>
<pre class="highlight">{ regex: '/\\*', action: { token: 'comment', next: '@comment' } }</pre>
<p>Here the matched <code>/*</code> is given the <code>"comment"</code> token class, and the tokenizer proceeds with matching the input using the rules in state <code>@comment</code>.</p>
<p>There are a few special states that can be used for the <code>next</code> attribute:</p>
<dl>
<dt>"@pop"</dt><dd>Pops the tokenizer stack to return to the previous state. This is used for example to return from block comment tokenizing after seeing the end marker:
<pre class="highlight">['\\*/', 'comment', '@pop']</pre>
</dd>
<dt>"@push"</dt><dd>Pushes the current state and continues in the current state. Nice for doing nested block comments when seeing a comment begin marker, i.e. in the <code>@comment</code> state, we can do:
<pre class="highlight">['/\\*', 'comment', '@push']</pre>
<dt id="popall">"@popall"</dt><dd>Pops everything from tokenizer stack and returns to the top state. This can be used during recovery to 'jump' back to the initial state from a deep nesting level.
</dd>
</dl>
</dd>
<dt id="switchTo">switchTo: <em>state</em></dt><dd><span class="adv">(Advanced)</span> Switch to <code><em>state</em></code> without changing the stack.</dd>
<dt id="goBack">goBack: <em>number</em></dt><dd><span class="adv">(Advanced)</span> Back up the input by <code><em>number</em></code> characters.</dd>
<dt id="bracket">bracket: <em>kind</em></dt><dd><span class="adv">(Advanced)</span> The <code><em>kind</em></code> can be either <code>'@open'</code> or <code>'@close'</code>. This signifies that a token is either an open or close brace. This attribute is set automatically if the token class is <a href="#@brackets"><code class="dt">@brackets</code></a>.
The editor uses the bracket information to show matching braces (where an open bracket matches with a close bracket if their token classes are the same). Moreover, when a user opens a new line the editor will do auto indentation on open braces. Normally, this attribute does not need to be set if you are using the <a href="#brackets"><code class="dt">brackets</code></a> attribute and it is only used for complex brace matching. This is discussed further in the next section on <a href="#complexmatch">advanced brace matching</a>.</dd>
<dt id="nextEmbedded">nextEmbedded: <em>langId</em> <span style="color=black">or</span> '@pop'</dt><dd><span class="adv">(Advanced)</span> Signifies to the editor that this token is followed by code in another language specified by the <code><em>langId</em></code>, i.e. for example <code>javascript</code>. Internally, our syntax highlighter keeps tokenizing the source until it finds an an ending sequence. At that point, you can use <code class="dt">nextEmbedded</code> with a <code class="dt">'@pop'</code> value to pop out of the embedded mode again. Usually, we need to use a <code class="dt">next</code> attribute too to switch to a state where we can tokenize the foreign code. As an example, here is how we could support CSS fragments in our language:
<pre class="highlight">root: [
[/<style\s*>/, { token: 'keyword', bracket: '@open'
, next: '@css_block', nextEmbedded: 'text/css' }],
[/<\/style\s*>/, { token: 'keyword', bracket: '@close' }],
...
],
css_block: [
[/[^"<]+/, ''],
[/<\/style\s*>/, { token: '@rematch', next: '@pop', nextEmbedded: '@pop' }],
[/"/, 'string', '@string' ],
[/</, '']
],</pre>
<p>Note how we switch to the <code>css_block</code> state for tokenizing the CSS source. Also inside the CSS we use the <code>@string</code> state to tokenize CSS strings such that we do not stop the CSS block when we find <code></style></code> inside a string. When we find the closing tag, we also <a href="#@pop"><code class="dt">"@pop"</code></a> the state to get back to normal tokenization. Finally, we need to <a href="#@rematch"><code class="dt">"@rematch"</code></a> the token (in the <code>root</code> state) since the editor ignores our token classes until we actually exit the embedded mode. See also a later section on <a href="#htmlembed">complex dynamic embeddings</a>.
(Bug: you can only start an embedded section if the you consume characters at the start of the embedded block (like consuming the <code><style></code> tag) (Aug 2012))</p>
</dd>
<dt id="log">log: <em>message</em></dt><dd>Used for debugging. Logs <code><em>message</em></code> to the console window in the browser (press F12 to see it). This can be useful to see if a certain action is executing. For example:
<pre class="highlight">[/\d+/, { token: 'number', log: 'found number $0 in state $S0' } ]</pre>
</dd>
<p> </p>
<!--
<dt>bracketType: <em>bracketType</em></dt><dd>If <code>token</code> is <code>"@brackets"</code>, this attribute can specify for an arbitrary matched input (like <code>"end"</code>), which is not present in the <code>brackets</code> attribute, what kind of bracket this is: <code>"@open"</code>, <code>"@close"</code>, or <code>"@none"</code>.</dd>
-->
</dl>
</dd>
<dt id="cases">{ cases: { <em>guard1</em>: <em>action1</em>, ..., <em>guardN</em>: <em>actionN</em> } }</dt><dd>The final kind of action object is a cases statement. A cases object contains an object where each field functions as a guard. Each guard is applied to the matched input and as soon as one of them matches, the corresponding action is applied. Note that since these are actions themselves, cases can be nested.
Cases are used for efficiency: for example, we match for identifiers and then test whether the identifier is possibly a keyword or builtin function:
<pre class="highlight">[/[a-z_\$][a-zA-Z0-9_\$]*/,
{ cases: { '@typeKeywords': 'keyword.type'
, '@keywords': 'keyword'
, '@default': 'identifier' }
}
]</pre>
<p>The guards can consist of:</p>
<dl>
<dt>"@<em>keywords</em>"</dt><dd>The attribute <code><em>keywords</em></code> must be defined in the language object and consist of an array of strings. The guard succeeds if the matched input matches any of the strings. (Note: all cases are pre-compiled and the list is tested using efficient hash maps). <span class="adv">Advanced</span>: if the attribute refers to a single string (instead of an array) it is compiled to a regular expression which is tested against the matched input.</dd>
<dt>"@default"</dt><dd>(or <code>"@"</code> or <code>""</code>) The default guard that always succeeds.</dd>
<dt id="@eos">"@eos"</dt><dd>Succeeds if the matched input has reached the end of the line.</dd>
<dt>"<em>regex</em>"</dt><dd>If the guard does not start with a <code>@</code> (or <code>$</code>) character it is interpreted as a regular expression that is tested against the matched input. Note: the <code><em>regex</em></code> is prefixed with <code>^</code> and postfixed with <code>$</code> so it must match the matched input entirely. This can be used for example to test for specific inputs, here is an example from the Koka language which uses this to enter various tokenizer states based on the declaration:
<pre class="highlight">
[/[a-z](\w|\-[a-zA-Z])*/,
{ cases:{ '@keywords': {
cases: { 'alias' : { token: 'keyword', next: '@alias-type' }
, 'struct' : { token: 'keyword', next: '@struct-type' }
, 'type|cotype|rectype': { token: 'keyword', next: '@type' }
, 'module|as|import' : { token: 'keyword', next: '@module' }
, '@default' : 'keyword' }
}
, '@builtins': 'predefined'
, '@default' : 'identifier' }
}
]
</pre>
<p>Note the use of nested cases to improve efficiency. Also, the library recognizes simple regular expressions like the ones above and compiles them efficiently. For example, the list of words <code>type|cotype|rectype</code> is tested using a Javascript hashmap/object.</p>
</dd>
</dl>
<p id="pattern"><span class="adv">(Advanced)</span> In general, a guard has the form <code class="dt">[<em>pat</em>][<em>op</em>]<em>match</em></code>, with an optional pattern, and operator (which are <code>$#</code> and <code>~</code> by default). The pattern can be any of:</p>
<dl>
<dt>$#</dt><dd>(default) The matched input (or the group that matched when the action is an array).</dd>
<dt>$<em>n</em></dt><dd>The <em>n</em>th group of the matched input, or the entire matched input for <code>$0</code>.</dd>
<dt>$S<em>n</em></dt><dd>The <em>n</em>th part of the state, i.e. <code>$S2</code> returns <code>foo</code> in a state <code>@tag.foo</code>. Use <code>$S0</code> for the full state name.</dd>
</dl>
<p>The above patterns can actually occur in many attributes and are automatically expanded. Attributes where these patterns expand are <a href="#token"><code class="dt">token</code></a>, <a href="#next"><code class="dt">next</code></a>, <a href="#nextEmbedded"><code class="dt">nextEmbedded</code></a>, <a href="#switchTo"><code class="dt">switchTo</code></a>, and <a href="#log"><code class="dt">log</code></a>. Also, these patterns are expanded in the <code class="dt"><em>match</em></code> part of a guard.</p>
<p>The guard operator <code><em>op</em></code> and <code><em>match</em></code> can be any of:</p>
<dl>
<dt>~<em>regex</em> <span style="color: black">or</span> !~<em>regex</em></dt><dd>(default for <code><em>op</em></code> is <code>~</code>) Tests <code><em>pat</em></code> against the regular expression or its negation.</dd>
<dt>@<em>attribute</em> <span style="color: black">or</span> !@<em>attribute</em></dt><dd>Tests whether <code><em>pat</em></code> is an element (<code>@</code>), or not an element (<code>!@</code>), of an array of strings defined by <code><em>attribute</em></code>.</dd>
<dt>==<em>str</em> <span style="color: black">or</span> !=<em>str</em></dt><dd>Tests if <code><em>pat</em></code> is equal or unequal to the given string <code><em>str</em></code>.</dd>
</dl>
<p>For example, here is how to check if the second group is not equal to <code>foo</code> or <code>bar</code>: <code>$2!~foo|bar</code>, or if the first captured group equals the name of the current lexer state: <code>$1==$S0</code>.</p>
<p>If both <code><em>op</em></code> and <code><em>match</em></code> are empty and there is just a pattern, then the guard succeeds if the pattern is non-empty. This can be used for example to improve efficiency. In the Koka language, an upper case identifier followed by a dot is module name, but without the following dot it is a constructor. This can be matched for in one go using:</p>
<pre class="highlight">[/([A-Z](?:[a-zA-Z0-9_]|\-[a-zA-Z])*)(\.?)/,
{ cases: { '$2' : ['identifier.namespace','keyword.dot']
, '@default': 'identifier.constructor' }}
]</pre>
</dd>
</dl>
</dl>
<p> </p>
<h2 id="complexmatch">Advanced: complex brace matching</h2>
<p>This section gives some advanced examples of brace matching using the <a href="#bracket"><code class="dt">bracket</code></a> attribute in an action. Usually, we can match braces just using the <a href="#brackets"><code>brackets</code></a> attribute in combination with the <a href="#@brackets"><code>@brackets</code></a> token class. But sometimes we need more
fine grained control. For example, in Ruby many declarations like <code class="token keyword">class</code> or <code class="token keyword">def</code> are ended with the <code class="token keyword">end</code> keyword. To make them match, we all give them the same token class (<code>keyword.decl</code>) and use bracket <code>@close</code> for <code class="token keyword">end</code> and <code>@open</code> for all declarations:</p>
<pre class="highlight">declarations: ['class','def','module', ... ]
tokenizer: {
root: {
[/[a-zA-Z]\w*/,
{ cases: { 'end' : { token: 'keyword.decl', bracket: '@close' }
, '@declarations': { token: 'keyword.decl', bracket: '@open' }
, '@keywords' : 'keyword'
, '@default' : 'identifier' }
}
],</pre>
<p>Note that to make <em>outdentation</em> work on the <code>end</code> keyword, you would also need to include the <code>'d'</code> character in the <a href="#outdentTriggers"><code class="dt">outdentTriggers</code></a> string.</p>
<p>Another example of complex matching is HTML where we would like to match starting tags, like <code><div></code> with an ending tag <code></div></code>. To make an end tag only match its specific open tag, we need to dynamically generate token classes that make the braces match correctly. This can be done using <code>$</code> expansion in the token class:</p>
<pre class="highlight">tokenizer: {
root: {
[/<(\w+)(>?)/, { token: 'tag-$1', bracket: '@open' }],
[/<\/(\w+)\s*>/, { token: 'tag-$1', bracket: '@close' }],</pre>
<p>Note how we captured the actual tag name as a group and used that to generate the right token class. Again, to make outdentation work on the closing tag, you would also need to include the <code>'>'</code> character in the <a href="#outdentTriggers"><code class="dt">outdentTriggers</code></a> string.</p>
<p>A final advanced example of brace matching is Visual Basic where declarations like <code class="token keyword">Structure</code> are matched with end declarations as <code class="token keyword">End Structure</code>. Just like HTML we need to dynamically set token classes so that an <code class="token keyword">End Enum</code> does not match with a <code class="token keyword">Structure</code>. A tricky part is that we now need to match multiple tokens at once, and we match a construct like <code class="token keyword">End Enum</code> as one closing token, but non declaration endings, like <code class="token keyword">End</code> <code class="token constructor"> Foo</code>, as three tokens:</p>
<pre class="highlight">decls: ["Structure","Class","Enum","Function",...],
tokenizer: {
root: {
[/(End)(\s+)([A-Z]\w*)/, { cases: { '$3@decls': { token: 'keyword.decl-$3', bracket: '@close'},
'@default': ['keyword','white','identifier.invalid'] }}],
[/[A-Z]\w*/, { cases: { '@decls' : { token: 'keyword.decl-$0', bracket: '@open' },
'@default': 'constructor' } }],</pre>
<p>Note how we used <code>$3</code> to first test if the third group is a declaration, and then use <code>$3</code> in the <code>token</code> attribute to generate a declaration specific token class (so we match correctly). Also, to make outdentation work correctly, we would need to include all the ending characters of the declarations in the <a href="#outdentTriggers"><code class="dt">outdentTriggers</code></a> string.</p>
<p> </p>
<h2 id="moreattr">Advanced: more attributes on the language definition</h2>
<p>Here are more advanced attributes that can be defined in the language definition:</p>
<dl>
<dt>tokenPostfix</dt><dd>(optional=<code>"." + name</code>, string) Optional postfix attached to all returned tokens. By default this attaches the language name so in the CSS you can refer to your specific language. For example, for the Java language, we could use <code>.identifier.java</code> to target all Java identifiers specifically in CSS.</dd>
<dt>start</dt><dd>(optional, string) The start state of the tokenizer. By default, this is the first entry in the tokenizer attribute.</dd>
<dt id="outdentTriggers">outdentTriggers</dt><dd>(optional, string) Optional string that defines characters that when typed could cause <em>outdentation</em>. This attribute is only used when using advanced brace matching in combination with the <a href="#bracket"><code class="dt">bracket</code></a> attribute. By default it always includes the last characters of the closing brackets in the <a href="#brackets"><code class="dt">brackets</code></a> list.
Outdentation happens when the user types a closing bracket word on an line that starts with only white space. If the closing bracket matches a open bracket it is indented to the same amount of that bracket. Usually, this causes the bracket to outdent. For example, in the Ruby language, the <code class="token keyword">end</code> keyword would match with an open declaration like <code class="token keyword">def</code> or <code class="token keyword">class</code>. To make outdentation happen though, we would need to include the <code>d</code> character in the <a href="#outdentTriggers"><code class="dt">outdentTriggers</code></a> attribute so it is checked when the users type <code class="token keyword">end</code>:
<pre class="highlight">outdentTriggers: 'd',</pre>
</dd>
</dl>
<p> </p>
<h2 id="htmlembed">Über Advanced: complex embeddings with dynamic end tags</h2>
<p>Many times, embedding other language fragments is easy as shown in the earlier CSS example, but sometimes it is more dynamic. For example, in HTML we would like to start embeddings on a <code class="token tag html">script</code> tag and <code class="token tag html">style</code> tag. By default, the script language is <code>javascript</code> but if the <code class="token key js">type</code> attribute is set, that defines the script language mime type. First, we define general tag open and close rules:</p>
<pre class="highlight">[/<(\w+)/, { token: 'tag.tag-$1', bracket: '@open', next: '@tag.$1' }],
[/<\/(\w+)\s*>/, { token: 'tag.tag-$1', bracket: '@close' } ],</pre>
<p>Here, we use the <code>$1</code> to capture the open tag name in both the token class and the next state. By putting the tag name in the token class, the brace matching will match and auto indent corresponding tags automatically. Next we define the <code>@tag</code> state that matches content within an HTML tag. Because the open tag rule will set the next state to <code>@tag.<em>tagname</em></code>, this will match the <code>@tag</code> state due to dot seperation.</p>
<pre class="highlight">tag: [
[/[ \t\r\n]+/, 'white'],
[/(type)(\s*=\s*)(['"])([^'"]+)(['"])/, [ 'attribute', 'delimiter', 'string', // todo: should match up quotes properly
{token: 'string', switchTo: '@tag.$S2.$4' },
'string'] ],
[/(\w+)(\s*=\s*)(['"][^'"]+['"])/, ['keyword', 'delimiter', 'string' ]],
[/>/, { cases: { '$S2==style' : { token: 'delimiter', switchTo: '@embedded.$S2', nextEmbedded: 'text/css'}
, '$S2==script': { cases: { '$S3' : { token: 'delimiter', switchTo: '@embedded.$S2', nextEmbedded: '$S3' },
'@default': { token: 'delimiter', switchTo: '@embedded.$S2', nextEmbedded: 'javascript' } }
, '@default' : { token: 'delimiter', next: '@pop' } } }]
[/[^>]/,''] // catch all
],</pre>
<p>Inside the <code>@tag.<em>tagname</em></code> state, we access the <code><em>tagname</em></code> through <code>$S2</code>. This is used to test if the tag name matches a script of style tag, in which case we start an embedded mode. We also need <a href="#switchTo"><code class="dt">switchTo</code></a> here since we do not want to get back to the <code>@tag</code> state at that point. Also, on a <code class="token key js">type</code> attribute we extend the state to <code>@tag.<em>tagname</em>.<em>mimetype</em></code> which allows us to access the mime type as <code>$S3</code> if it was set. This is used to determine the script language (or default to <code>javascript</code>). Finally, the script and style start an embedded mode and switch to a state <code>@embedded.<em>tagname</em></code>. The tag name is included in the state so we can scan for exactly a matching end tag:</p>
<pre class="highlight">embedded: [
[/[^"<]+/, ''],
[/<\/(\w+)\s*>/, { cases: { '$1==$S2' : { token: '@rematch', next: '@pop', nextEmbedded: '@pop' },
'@default': '' } }],
[/"/, 'string', '@string' ],
[/</, '']
],</pre>
<p>Only when we find a matching end tag (outside a string), <code>$1==$S2</code>, we pop the state and exit the embedded mode. Note that we need <a href="#@rematch"><code class="dt">@rematch</code></a> since the editor is ignoring our token classes until we actually exit the embedded mode (and we handle the close tag again in the <code>@root</code> state).</p>
</div> <!-- documentation -->
</div> <!-- main -->
<!--******************************************
Samples are included as PRE elements
**********************************************-->
<div id="samples" style="display: none">
<pre id="mylang-sample">// Type source code in your language here...
class MyClass {
@attribute
void main() {
Console.writeln( "Hello Monarch world\n");
}
}
</pre>
<pre id='mylang'>// Create your own language definition here
// You can safely look at other samples without losing modifications.
// Modifications are not saved on browser refresh/close though -- copy often!
return {
// Set defaultToken to invalid to see what you do not tokenize yet
// defaultToken: 'invalid',
keywords: [
'abstract', 'continue', 'for', 'new', 'switch', 'assert', 'goto', 'do',
'if', 'private', 'this', 'break', 'protected', 'throw', 'else', 'public',
'enum', 'return', 'catch', 'try', 'interface', 'static', 'class',
'finally', 'const', 'super', 'while', 'true', 'false'
],
typeKeywords: [
'boolean', 'double', 'byte', 'int', 'short', 'char', 'void', 'long', 'float'
],
operators: [
'=', '>', '<', '!', '~', '?', ':', '==', '<=', '>=', '!=',
'&&', '||', '++', '--', '+', '-', '*', '/', '&', '|', '^', '%',
'<<', '>>', '>>>', '+=', '-=', '*=', '/=', '&=', '|=', '^=',
'%=', '<<=', '>>=', '>>>='
],
// we include these common regular expressions
symbols: /[=><!~?:&|+\-*\/\^%]+/,
// C# style strings
escapes: /\\(?:[abfnrtv\\"']|x[0-9A-Fa-f]{1,4}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})/,
// The main tokenizer for our languages
tokenizer: {
root: [
// identifiers and keywords
[/[a-z_$][\w$]*/, { cases: { '@typeKeywords': 'keyword',
'@keywords': 'keyword',
'@default': 'identifier' } }],
[/[A-Z][\w\$]*/, 'type.identifier' ], // to show class names nicely
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/[<>](?!@symbols)/, '@brackets'],
[/@symbols/, { cases: { '@operators': 'operator',
'@default' : '' } } ],
// @ annotations.
// As an example, we emit a debugging log message on these tokens.
// Note: message are supressed during the first load -- change some lines to see them.
[/@\s*[a-zA-Z_\$][\w\$]*/, { token: 'annotation', log: 'annotation token: $0' }],
// numbers
[/\d*\.\d+([eE][\-+]?\d+)?/, 'number.float'],
[/0[xX][0-9a-fA-F]+/, 'number.hex'],
[/\d+/, 'number'],
// delimiter: after number because of .\d floats
[/[;,.]/, 'delimiter'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, { token: 'string.quote', bracket: '@open', next: '@string' } ],
// characters
[/'[^\\']'/, 'string'],
[/(')(@escapes)(')/, ['string','string.escape','string']],
[/'/, 'string.invalid']
],
comment: [
[/[^\/*]+/, 'comment' ],
[/\/\*/, 'comment', '@push' ], // nested comment
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
],
},
};
</pre>
<pre id="java-sample">// Type source code in your Java here...
public class HelloWorld {
public static void main(String[] args) {
System.out.println("Hello, World");
}
}
</pre>
<pre id="java">// Difficulty: "Easy"
// Language definition for Java
return {
// Set defaultToken to invalid to see what you do not tokenize yet
// defaultToken: 'invalid',
keywords: [
'abstract', 'continue', 'for', 'new', 'switch', 'assert', 'default',
'goto', 'package', 'synchronized', 'boolean', 'do', 'if', 'private',
'this', 'break', 'double', 'implements', 'protected', 'throw', 'byte',
'else', 'import', 'public', 'throws', 'case', 'enum', 'instanceof', 'return',
'transient', 'catch', 'extends', 'int', 'short', 'try', 'char', 'final',
'interface', 'static', 'void', 'class', 'finally', 'long', 'strictfp',
'volatile', 'const', 'float', 'native', 'super', 'while', 'true', 'false'
],
typeKeywords: [
'boolean', 'double', 'byte', 'int', 'short', 'char', 'void', 'long', 'float'
],
operators: [
'=', '>', '<', '!', '~', '?', ':',
'==', '<=', '>=', '!=', '&&', '||', '++', '--',
'+', '-', '*', '/', '&', '|', '^', '%', '<<',
'>>', '>>>', '+=', '-=', '*=', '/=', '&=', '|=',
'^=', '%=', '<<=', '>>=', '>>>='
],
// we include these common regular expressions
symbols: /[=><!~?:&|+\-*\/\^%]+/,
escapes: /\\(?:[abfnrtv\\"']|x[0-9A-Fa-f]{1,4}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})/,
// The main tokenizer for our languages
tokenizer: {
root: [
// identifiers and keywords
[/[a-z_$][\w$]*/, { cases: { '@typeKeywords': 'keyword',
'@keywords': 'keyword',
'@default': 'identifier' } }],
[/[A-Z][\w\$]*/, 'type.identifier' ], // to show class names nicely
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/[<>](?!@symbols)/, '@brackets'],
[/@symbols/, { cases: { '@operators': 'operator',
'@default' : '' } } ],
// @ annotations.
// As an example, we emit a debugging log message on these tokens.
// Note: message are supressed during the first load -- change some lines to see them.
[/@\s*[a-zA-Z_\$][\w\$]*/, { token: 'annotation', log: 'annotation token: $0' }],
// numbers
[/\d*\.\d+([eE][\-+]?\d+)?[fFdD]?/, 'number.float'],
[/0[xX][0-9a-fA-F_]*[0-9a-fA-F][Ll]?/, 'number.hex'],
[/0[0-7_]*[0-7][Ll]?/, 'number.octal'],
[/0[bB][0-1_]*[0-1][Ll]?/, 'number.binary'],
[/\d+[lL]?/, 'number'],
// delimiter: after number because of .\d floats
[/[;,.]/, 'delimiter'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, 'string', '@string' ],
// characters
[/'[^\\']'/, 'string'],
[/(')(@escapes)(')/, ['string','string.escape','string']],
[/'/, 'string.invalid']
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
],
comment: [
[/[^\/*]+/, 'comment' ],
// [/\/\*/, 'comment', '@push' ], // nested comment not allowed :-(
[/\/\*/, 'comment.invalid' ],
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, 'string', '@pop' ]
],
},
};
</pre>
<!--******************************************
Javascript
**********************************************-->
<pre id="javascript-sample">// Type source code in JavaScript here...
define('module',[],function()
{
function test(s) {
return s.replace(/[a-z$]oo\noo$/, 'bar');
}
return {
main: alert(test("hello monarch world\n"))
}
});</pre>
<pre id="javascript">// Difficulty: "Moderate"
// This is the JavaScript tokenizer that is actually used to highlight
// all code in the syntax definition editor and the documentation!
//
// This definition takes special care to highlight regular
// expressions correctly, which is convenient when writing
// syntax highlighter specifications.
return {
tokenPostfix: '.js',
keywords: [
'boolean', 'break', 'byte', 'case', 'catch', 'char', 'class', 'const', 'continue', 'debugger',
'default', 'delete', 'do', 'double', 'else', 'enum', 'export', 'extends', 'false', 'final',
'finally', 'float', 'for', 'function', 'goto', 'if', 'implements', 'import', 'in',
'instanceof', 'int', 'interface', 'long', 'native', 'new', 'null', 'package', 'private',
'protected', 'public', 'return', 'short', 'static', 'super', 'switch', 'synchronized', 'this',
'throw', 'throws', 'transient', 'true', 'try', 'typeof', 'var', 'void', 'volatile', 'while',
'with'
],
builtins: [
'define','require','window','document','undefined'
],
operators: [
'=', '>', '<', '!', '~', '?', ':',
'==', '<=', '>=', '!=', '&&', '||', '++', '--',
'+', '-', '*', '/', '&', '|', '^', '%', '<<',
'>>', '>>>', '+=', '-=', '*=', '/=', '&=', '|=',
'^=', '%=', '<<=', '>>=', '>>>='
],
// define our own brackets as '<' and '>' do not match in javascript
brackets: [
['(',')','bracket.parenthesis'],
['{','}','bracket.curly'],
['[',']','bracket.square']
],
// common regular expressions
symbols: /[~!@#%\^&*-+=|\\:`<>.?\/]+/,
escapes: /\\(?:[btnfr\\"']|[0-7][0-7]?|[0-3][0-7]{2})/,
exponent: /[eE][\-+]?[0-9]+/,
regexpctl: /[(){}\[\]\$\^|\-*+?\.]/,
regexpesc: /\\(?:[bBdDfnrstvwWn0\\\/]|@regexpctl|c[A-Z]|x[0-9a-fA-F]{2}|u[0-9a-fA-F]{4})/,
tokenizer: {
root: [
// identifiers and keywords
[/([a-zA-Z_\$][\w\$]*)(\s*)(:?)/, {
cases: { '$1@keywords': ['keyword','white','delimiter'],
'$3': ['key.identifier','white','delimiter'], // followed by :
'$1@builtins': ['predefined.identifier','white','delimiter'],
'@default': ['identifier','white','delimiter'] } }],
// whitespace
{ include: '@whitespace' },
// regular expression: ensure it is terminated before beginning (otherwise it is an opeator)
[/\/(?=([^\\\/]|\\.)+\/)/, { token: 'regexp.slash', bracket: '@open', next: '@regexp'}],
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/[;,.]/, 'delimiter'],
[/@symbols/, { cases: {'@operators': 'operator',
'@default': '' }}],
// numbers
[/\d+\.\d*(@exponent)?/, 'number.float'],
[/\.\d+(@exponent)?/, 'number.float'],
[/\d+@exponent/, 'number.float'],
[/0[xX][\da-fA-F]+/, 'number.hex'],
[/0[0-7]+/, 'number.octal'],
[/\d+/, 'number'],
// strings: recover on non-terminated strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/'([^'\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, 'string', '@string."' ],
[/'/, 'string', '@string.\'' ],
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
],
comment: [
[/[^\/*]+/, 'comment' ],
// [/\/\*/, 'comment', '@push' ], // nested comment not allowed :-(
[/\/\*/, 'comment.invalid' ],
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
string: [
[/[^\\"']+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/["']/, { cases: { '$#==$S2' : { token: 'string', next: '@pop' },
'@default': 'string' }} ]
],
// We match regular expression quite precisely
regexp: [
[/(\{)(\d+(?:,\d*)?)(\})/, ['@brackets.regexp.escape.control', 'regexp.escape.control', '@brackets.regexp.escape.control'] ],
[/(\[)(\^?)(?=(?:[^\]\\\/]|\\.)+)/, ['@brackets.regexp.escape.control',{ token: 'regexp.escape.control', next: '@regexrange'}]],
[/(\()(\?:|\?=|\?!)/, ['@brackets.regexp.escape.control','regexp.escape.control'] ],
[/[()]/, '@brackets.regexp.escape.control'],
[/@regexpctl/, 'regexp.escape.control'],
[/[^\\\/]/, 'regexp' ],
[/@regexpesc/, 'regexp.escape' ],
[/\\\./, 'regexp.invalid' ],
['/', { token: 'regexp.slash', bracket: '@close'}, '@pop' ],
],
regexrange: [
[/-/, 'regexp.escape.control'],
[/\^/, 'regexp.invalid'],
[/@regexpesc/, 'regexp.escape'],
[/[^\]]/, 'regexp'],
[/\]/, '@brackets.regexp.escape.control', '@pop'],
],
},
};
</pre>
<!--******************************************
Dafny
**********************************************-->
<pre id="dafny-sample">
// This method computes the sum and max of a given array of
// integers. The method's postcondition only promises that
// 'sum' will be no greater than 'max'. Can you write a
// different method body that also achieves this postcondition?
// Hint: Your program does not have to compute the sum and
// max of the array, despite the suggestive names of the
// out-parameters.
method M(N: int, a: array<int>) returns (sum: int, max: int)
requires 0 <= N & a != null & a.Length == N;
ensures sum <= N * max;
{
sum := 0;
max := 0;
var i := 0;
while (i < N)
invariant i <= N & sum <= i * max;
{
if (max < a[i]) {
max := a[i];
}
sum := sum + a[i];
i := i + 1;
}
}
</pre>
<pre id='dafny'>// Difficulty: "Easy"
// Language definition sample for the Dafny language.
// See 'http://rise4fun.com/Dafny'.
return {
keywords: [
'class','datatype','codatatype','type','function',
'ghost','var','method','constructor',
'module','import','default','as','opened','static','refines',
'returns','break','then','else','if','label','return','while','print','where',
'new','parallel', 'in','this','fresh','choose',
'match','case','assert','assume', 'predicate','copredicate',
'forall','exists', 'false','true','null','old',
'calc','iterator','yields','yield'
],
verifyKeywords: [
'requires','ensures','modifies','reads','free', 'invariant','decreases',
],
types: [
'bool','multiset','map','nat','int','object','set','seq', 'array'
],
brackets: [
['{','}','delimiter.curly'],
['[',']','delimiter.square'],
['(',')','delimiter.parenthesis']
],
// Dafny uses C# style strings
escapes: /\\(?:[abfnrtv\\"']|x[0-9A-Fa-f]{1,4}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})/,
tokenizer: {
root: [
// identifiers
[/array([2-9]\d*|1\d+)/, 'type.keyword' ],
[/[a-zA-Z'_\?\\][\w'\?\\]*/, { cases: {'@keywords': 'keyword',
'@verifyKeywords': 'constructor.identifier',
'@types' : 'type.keyword',
'@default' : 'identifier' }}],
[':=','keyword'],
// whitespace
{ include: '@whitespace' },
[/[{}()\[\]]/, '@brackets'],
[/[;,]/, 'delimiter'],
// literals
[/[0-9]+/, 'number'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, 'string', '@string' ],
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
],
comment: [
[/[^\/*]+/, 'comment' ],
[/\/\*/, 'comment', '@push' ], // nested comment
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, 'string', '@pop' ]
],
}
};</pre>
<!--******************************************
Koka
**********************************************-->
<pre id="koka-sample">// This module implements the Garcia-Wachs algorithm.
// It is an adaptation of the algorithm in ML as described by Jean-Christophe Filli�tre:
// in ''A functional implementation of the Garsia-Wachs algorithm. (functional pearl). ML workshop 2008, pages 91--96''.
// See: http://www.lri.fr/~filliatr/publis/gw-wml08.pdf
//
// The algorithm is interesting since it uses mutable references shared between a list and tree but the
// side-effects are not observable from outside. Koka automatically infers that final algorithm is pure.
module garcia-wachs
//----------------------------------------------------
// Trees
//----------------------------------------------------
public type tree<a> {
con Leaf(value :a)
con Node(left :tree<a>, right :tree<a>)
}
fun show( t : tree<char> ) : string
{
match(t) {
Leaf(c) -> Core.show(c)
Node(l,r) -> "Node(" + show(l) + "," + show(r) + ")"
}
}
//----------------------------------------------------
// Non empty lists
//----------------------------------------------------
public type list1<a> {
Cons1( head : a, tail : list<a> )
}
fun map( xs, f ) {
val Cons1(y,ys) = xs
return Cons1(f(y), Core.map(ys,f))
}
fun zip( xs :list1<a>, ys :list1<b> ) : list1<(a,b)> {
Cons1( (xs.head, ys.head), Core.zip(xs.tail, ys.tail))
}
//----------------------------------------------------
// Phase 1
// note: koka cannot yet prove that the mutual recursive
// functions "insert" and "extract" always terminate :-(
//----------------------------------------------------
fun insert( after : list<(tree<a>,int)>, t : (tree<a>,int), before : list<(tree<a>,int)> ) : div tree<a>
{
match(before) {
Nil -> extract( [], Cons1(t,after) )
Cons(x,xs) -> {
if (x.snd < t.snd) then return insert( Cons(x,after), t, xs )
match(xs) {
Nil -> extract( [], Cons1(x,Cons(t,after)) )
Cons(y,ys) -> extract( ys, Cons1(y,Cons(x,Cons(t,after))) )
}
}
}
}
fun extract( before : list<(tree<a>,int)>, after : list1<(tree<a>,int)> ) : div tree<a>
{
val Cons1((t1,w1) as x, xs ) = after
match(xs) {
Nil -> t1
Cons((t2,w2) as y, ys) -> match(ys) {
Nil -> insert( [], (Node(t1,t2), w1+w2), before )
Cons((_,w3),_zs) ->
if (w1 <= w3)
then insert(ys, (Node(t1,t2), w1+w2), before)
else extract(Cons(x,before), Cons1(y,ys))
}
}
}
fun balance( xs : list1<(tree<a>,int)> ) : div tree<a>
{
extract( [], xs )
}
fun mark( depth :int, t :tree<(a,ref<h,int>)> ) : <write<h>> ()
{
match(t) {
Leaf((_,d)) -> d := depth
Node(l,r) -> { mark(depth+1,l); mark(depth+1,r) }
}
}
fun build( depth :int, xs :list1<(a,ref<h,int>)> ) : <read<h>,div> (tree<a>,list<(a,ref<h,int>)>)
{
if (!xs.head.snd == depth) return (Leaf(xs.head.fst), xs.tail)
l = build(depth+1, xs)
match(l.snd) {
Nil -> (l.fst, Nil)
Cons(y,ys) -> {
r = build(depth+1, Cons1(y,ys))
(Node(l.fst,r.fst), r.snd)
}
}
}
public function garciawachs( xs : list1<(a,int)> ) : div tree<a>
{
refs = xs.map(fst).map( fun(x) { (x, ref(0)) } )
wleafs = zip( refs.map(Leaf), xs.map(snd) )
tree = balance(wleafs)
mark(0,tree)
build(0,refs).fst
}
public function main() {
wlist = Cons1(('a',3), [('b',2),('c',1),('d',4),('e',5)])
tree = wlist.garciawachs()
tree.show.print()
}
</pre>
<pre id='koka'>// Difficulty: "Moderate"
// Language definition for the Koka language
// See 'rise4fun.com/Koka' for more information.
// This definition uses states extensively to color types correctly
// where it matches up brackets inside nested types.
return {
keywords: [
'infix', 'infixr', 'infixl', 'prefix', 'postfix',
'type', 'cotype', 'rectype', 'alias', 'struct', 'enum', 'con',