// Type source code in your language here...
class MyClass {
@attribute
void main() {
Console.writeln( "Hello Monarch world\n");
}
}
// 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'],
],
},
};
// Type source code in your Java here...
public class HelloWorld {
public static void main(String[] args) {
System.out.println("Hello, World");
}
}
// Difficulty: "Easy"
// Language definition for Java
return {
defaultToken: '',
tokenPostfix: '.java',
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'
],
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})/,
digits: /\d+(_+\d+)*/,
octaldigits: /[0-7]+(_+[0-7]+)*/,
binarydigits: /[0-1]+(_+[0-1]+)*/,
hexdigits: /[[0-9a-fA-F]+(_+[0-9a-fA-F]+)*/,
// The main tokenizer for our languages
tokenizer: {
root: [
// identifiers and keywords
[/[a-zA-Z_$][\w$]*/, {
cases: {
'@keywords': { token: 'keyword.$0' },
'@default': 'identifier'
}
}],
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/[<>](?!@symbols)/, '@brackets'],
[/@symbols/, {
cases: {
'@operators': 'delimiter',
'@default': ''
}
}],
// @ annotations.
[/@\s*[a-zA-Z_\$][\w\$]*/, 'annotation'],
// numbers
[/(@digits)[eE]([\-+]?(@digits))?[fFdD]?/, 'number.float'],
[/(@digits)\.(@digits)([eE][\-+]?(@digits))?[fFdD]?/, 'number.float'],
[/0[xX](@hexdigits)[Ll]?/, 'number.hex'],
[/0(@octaldigits)[Ll]?/, 'number.octal'],
[/0[bB](@binarydigits)[Ll]?/, 'number.binary'],
[/(@digits)[fFdD]/, 'number.float'],
[/(@digits)[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]+/, ''],
[/\/\*\*(?!\/)/, 'comment.doc', '@javadoc'],
[/\/\*/, 'comment', '@comment'],
[/\/\/.*$/, 'comment'],
],
comment: [
[/[^\/*]+/, 'comment'],
// [/\/\*/, 'comment', '@push' ], // nested comment not allowed :-(
// [/\/\*/, 'comment.invalid' ], // this breaks block comments in the shape of /* //*/
[/\*\//, 'comment', '@pop'],
[/[\/*]/, 'comment']
],
//Identical copy of comment above, except for the addition of .doc
javadoc: [
[/[^\/*]+/, 'comment.doc'],
// [/\/\*/, 'comment.doc', '@push' ], // nested comment not allowed :-(
[/\/\*/, 'comment.doc.invalid'],
[/\*\//, 'comment.doc', '@pop'],
[/[\/*]/, 'comment.doc']
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, 'string', '@pop']
],
},
};
// 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"))
}
});
// 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 {
// Set defaultToken to invalid to see what you do not tokenize yet
defaultToken: 'invalid',
tokenPostfix: '.js',
keywords: [
'break', 'case', 'catch', 'class', 'continue', 'const',
'constructor', 'debugger', 'default', 'delete', 'do', 'else',
'export', 'extends', 'false', 'finally', 'for', 'from', 'function',
'get', 'if', 'import', 'in', 'instanceof', 'let', 'new', 'null',
'return', 'set', 'super', 'switch', 'symbol', 'this', 'throw', 'true',
'try', 'typeof', 'undefined', 'var', 'void', 'while', 'with', 'yield',
'async', 'await', 'of'
],
typeKeywords: [
'any', 'boolean', 'number', 'object', 'string', 'undefined'
],
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})/,
digits: /\d+(_+\d+)*/,
octaldigits: /[0-7]+(_+[0-7]+)*/,
binarydigits: /[0-1]+(_+[0-1]+)*/,
hexdigits: /[[0-9a-fA-F]+(_+[0-9a-fA-F]+)*/,
regexpctl: /[(){}\[\]\$\^|\-*+?\.]/,
regexpesc: /\\(?:[bBdDfnrstvwWn0\\\/]|@regexpctl|c[A-Z]|x[0-9a-fA-F]{2}|u[0-9a-fA-F]{4})/,
// The main tokenizer for our languages
tokenizer: {
root: [
[/[{}]/, 'delimiter.bracket'],
{ include: 'common' }
],
common: [
// identifiers and keywords
[/[a-z_$][\w$]*/, {
cases: {
'@typeKeywords': 'keyword',
'@keywords': 'keyword',
'@default': 'identifier'
}
}],
[/[A-Z][\w\$]*/, 'type.identifier'], // to show class names nicely
// [/[A-Z][\w\$]*/, 'identifier'],
// whitespace
{ include: '@whitespace' },
// regular expression: ensure it is terminated before beginning (otherwise it is an opeator)
[/\/(?=([^\\\/]|\\.)+\/([gimsuy]*)(\s*)(\.|;|\/|,|\)|\]|\}|$))/, { token: 'regexp', bracket: '@open', next: '@regexp' }],
// delimiters and operators
[/[()\[\]]/, '@brackets'],
[/[<>](?!@symbols)/, '@brackets'],
[/@symbols/, {
cases: {
'@operators': 'delimiter',
'@default': ''
}
}],
// numbers
[/(@digits)[eE]([\-+]?(@digits))?/, 'number.float'],
[/(@digits)\.(@digits)([eE][\-+]?(@digits))?/, 'number.float'],
[/0[xX](@hexdigits)/, 'number.hex'],
[/0[oO]?(@octaldigits)/, 'number.octal'],
[/0[bB](@binarydigits)/, 'number.binary'],
[/(@digits)/, 'number'],
// delimiter: after number because of .\d floats
[/[;,.]/, 'delimiter'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid'], // non-teminated string
[/'([^'\\]|\\.)*$/, 'string.invalid'], // non-teminated string
[/"/, 'string', '@string_double'],
[/'/, 'string', '@string_single'],
[/`/, 'string', '@string_backtick'],
],
whitespace: [
[/[ \t\r\n]+/, ''],
[/\/\*\*(?!\/)/, 'comment.doc', '@jsdoc'],
[/\/\*/, 'comment', '@comment'],
[/\/\/.*$/, 'comment'],
],
comment: [
[/[^\/*]+/, 'comment'],
[/\*\//, 'comment', '@pop'],
[/[\/*]/, 'comment']
],
jsdoc: [
[/[^\/*]+/, 'comment.doc'],
[/\*\//, 'comment.doc', '@pop'],
[/[\/*]/, 'comment.doc']
],
// We match regular expression quite precisely
regexp: [
[/(\{)(\d+(?:,\d*)?)(\})/, ['regexp.escape.control', 'regexp.escape.control', 'regexp.escape.control']],
[/(\[)(\^?)(?=(?:[^\]\\\/]|\\.)+)/, ['regexp.escape.control', { token: 'regexp.escape.control', next: '@regexrange' }]],
[/(\()(\?:|\?=|\?!)/, ['regexp.escape.control', 'regexp.escape.control']],
[/[()]/, 'regexp.escape.control'],
[/@regexpctl/, 'regexp.escape.control'],
[/[^\\\/]/, 'regexp'],
[/@regexpesc/, 'regexp.escape'],
[/\\\./, 'regexp.invalid'],
[/(\/)([gimsuy]*)/, [{ token: 'regexp', bracket: '@close', next: '@pop' }, 'keyword.other']],
],
regexrange: [
[/-/, 'regexp.escape.control'],
[/\^/, 'regexp.invalid'],
[/@regexpesc/, 'regexp.escape'],
[/[^\]]/, 'regexp'],
[/\]/, { token: 'regexp.escape.control', next: '@pop', bracket: '@close' }],
],
string_double: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, 'string', '@pop']
],
string_single: [
[/[^\\']+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/'/, 'string', '@pop']
],
string_backtick: [
[/\$\{/, { token: 'delimiter.bracket', next: '@bracketCounting' }],
[/[^\\`$]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/`/, 'string', '@pop']
],
bracketCounting: [
[/\{/, 'delimiter.bracket', '@bracketCounting'],
[/\}/, 'delimiter.bracket', '@pop'],
{ include: 'common' }
],
},
};
// 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;
}
}
// 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' ]
],
}
};
// 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()
}
// 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',
'fun', 'function', 'val', 'var', 'external',
'if', 'then', 'else', 'elif', 'return', 'match',
'forall', 'exists', 'some', 'with',
'private', 'public', 'private',
'module', 'import', 'as',
'=', '.', ':', ':=', '->',
'include', 'inline','rec','try', 'yield',
'interface', 'instance'
],
builtins: [
'for', 'while', 'repeat',
'foreach', 'foreach-indexed',
'error', 'catch', 'finally',
'cs', 'js', 'file', 'ref', 'assigned'
],
typeKeywords: [
'forall', 'exists', 'some', 'with'
],
typeStart: [
'type','cotype','rectype','alias','struct','enum'
],
moduleKeywords: [
'module','import','as'
],
kindConstants: [
'E','P','H','V','X'
],
escapes : /\\(?:[nrt\\"'\?]|x[0-9a-fA-F]{2}|u[0-9a-fA-F]{4}|U[0-9a-fA-F]{6})/,
symbols0: /[\$%&\*\+@!\/\\\^~=\.:\-\?]/,
symbols : /(?:@symbols0|[\|<>])+/,
idchars : /(?:\w|\-[a-zA-Z])*/,
tokenizer: {
root: [
// identifiers and operators
[/[a-z]@idchars/,
{ 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': 'identifier.predefined',
'@default' : 'identifier' }
}
],
[/([A-Z]@idchars)(\.?)/,
{ cases: { '$2': ['identifier.namespace','keyword.dot'],
'@default': 'identifier.constructor' }}
],
[/_@idchars/, 'identifier.wildcard'],
// whitespace
{ include: '@whitespace' },
[/[{}()\[\]]/, '@brackets'],
[/[;,`]/, 'delimiter'],
// do not scan these as operators
[/[<>](?![<>|]*@symbols0)/, '@brackets' ],
[/->(?!@symbols0|[>\|])/, 'keyword' ],
[/::?(?!@symbols0)/, 'type.operator', '@type'],
[/::?(?=\?)/, 'type.operator', '@type'],
// literal string
[/@"/, { token: 'string.quote', bracket: '@open', next: '@litstring' } ],
// operators
[/@symbols/, { cases: { '\\-': 'operator.minus',
'@keywords': 'keyword.operator',
'@default': 'operator' }}
],
// numbers
[/[0-9]+\.[0-9]+([eE][\-+]?[0-9]+)?/, 'number.float'],
[/0[xX][0-9a-fA-F]+/, 'number.hex'],
[/[0-9]+/, 'number'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, { token: 'string.quote', bracket: '@open', next: '@string' } ],
// characters
[/'[^\\']'/, 'string'],
[/(')(@escapes)(')/, ['string','string.escape','string']],
[/'/, 'string.invalid'],
// meta
[/^[ ]*#.*/, 'namespace']
],
whitespace: [
[/[ \r\n]+/, 'white'],
['/\\*', 'comment', '@comment' ],
['//$', 'comment'],
['//', 'comment', '@line_comment']
],
comment: [
[/^\s*["|]\s*$/, 'comment', '@comment_docblock'],
[/[^\/*"|]+/, 'comment' ],
['/\\*', 'comment', '@push' ],
['\\*/', 'comment', '@pop' ],
[/(")((?:[^"]|"")*)(")/, ['comment','comment.doc','comment']],
[/(\|)((?:[^|]|\|\|)*)(\|)/, ['comment','comment.doc','comment']],
[/[\/*"|]/, 'comment']
],
comment_docblock: [
[/\*\/|\/\*/, '@rematch', '@pop'], // recover: back to comment mode
[/^\s*"\s*$/, 'comment', '@pop'],
[/^\s*\|\s*$/, 'comment', '@pop'],
[/[^*\/]+/, 'comment.doc'],
[/./, 'comment.doc'] // catch all
],
line_comment: [
[/[^"|]*$/, 'comment', '@pop' ],
[/[^"|]+/, 'comment' ],
[/(")((?:[^"]|"")*)(")/,
['comment','comment.doc', { cases: { '@eos': { token: 'comment', next: '@pop' },
'@default': 'comment' }}]
],
[/(\|)((?:[^|]|\|\|)*)(\|)/,
['comment','comment.doc', { cases: { '@eos': { token: 'comment', next: '@pop' },
'@default': 'comment' }}]
],
[/.*$/, 'comment', '@pop'] // catch all
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
litstring: [
[/[^"]+/, 'string'],
[/""/, 'string.escape'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
// Module mode: color names as module names
module: [
{ include: '@whitespace' },
[/[a-z]@idchars/,
{ cases: { '@moduleKeywords': 'keyword',
'@keywords': { token: '@rematch', next: '@pop' },
'@default': 'identifier.namespace' }}
],
[/[A-Z]@idchars/, 'identifier.namespace'],
[/\.(?!@symbols)/, 'keyword.operator.dot'],
['','','@pop'] // catch all
],
// Koka type coloring is a bit involved but looks cool :-)
alias_type: [
['=', 'keyword.operator'], // allow equal sign
{ include: '@type' }
],
struct_type: [
[ /\((?!,*\))/, '@brackets', '@pop'], // allow for tuple struct definition
{ include: '@type' }
],
type: [
[ /[(\[<]/, { token: '@brackets.type' }, '@type_nested'],
{ include: '@type_content' }
],
type_nested: [
[/[)\]>]/, { token: '@brackets.type' }, '@pop' ],
[/[(\[<]/, { token: '@brackets.type' }, '@push'],
[/,/, 'delimiter.type'],
[/([a-z]@idchars)(\s*)(:)(?!:)/,['type.identifier.typeparam','white','type.operator']],
{ include: '@type_content' }
],
type_content: [
{ include: '@whitespace' },
// type identifiers
[/[*!](?!@symbols)/, 'type.kind.identifier'],
[/[a-z][0-9]*(?![a-zA-Z_\-])/, 'type.identifier.typevar'],
[/_@idchars/, 'type.identifier.typevar'],
[/[a-z]@idchars/,
{ cases: { '@typeKeywords': 'type.keyword',
'@keywords': { token: '@rematch', next: '@pop' },
'@builtins': 'type.predefined',
'@default': 'type.identifier'
}}
],
[/[A-Z]@idchars(\.?)/,
{ cases: { '$2': ['identifier.namespace','keyword.dot'],
'@kindConstants': 'type.kind.identifier',
'@default': 'type.identifier'
}}
],
[/::|->|[\.:|]/, 'type.operator'],
['','','@pop'] // catch all
]
}
};
<!DOCTYPE html>
<html>
<head>
<title>Monarch Workbench</title>
<meta http-equiv="X-UA-Compatible" content="IE=edge" />
<!-- a comment
-->
<style>
body { font-family: Consolas; } /* nice */
</style>
</head>
<body>
<div class="test">
<script>
function() {
alert("hi </script>"); // javascript
};
</script>
<script type="text/x-dafny">
class Foo {
x : int;
invariant x > 0;
};
</script>
</div>
</body>
</html>
// Difficulty: "Hurt me plenty"
// Language definition for HTML
// This definition uses states extensively to
// - match up tags.
// - and to embed scripts dynamically
// See also the documentation for an explanation of these techniques
return {
defaultToken: '',
tokenPostfix: '.html',
ignoreCase: true,
// The main tokenizer for our languages
tokenizer: {
root: [
[/<!DOCTYPE/, 'metatag', '@doctype'],
[/<!--/, 'comment', '@comment'],
[/(<)((?:[\w\-]+:)?[\w\-]+)(\s*)(\/>)/, ['delimiter', 'tag', '', 'delimiter']],
[/(<)(script)/, ['delimiter', { token: 'tag', next: '@script' }]],
[/(<)(style)/, ['delimiter', { token: 'tag', next: '@style' }]],
[/(<)((?:[\w\-]+:)?[\w\-]+)/, ['delimiter', { token: 'tag', next: '@otherTag' }]],
[/(<\/)((?:[\w\-]+:)?[\w\-]+)/, ['delimiter', { token: 'tag', next: '@otherTag' }]],
[/</, 'delimiter'],
[/[^<]+/], // text
],
doctype: [
[/[^>]+/, 'metatag.content'],
[/>/, 'metatag', '@pop'],
],
comment: [
[/-->/, 'comment', '@pop'],
[/[^-]+/, 'comment.content'],
[/./, 'comment.content']
],
otherTag: [
[/\/?>/, 'delimiter', '@pop'],
[/"([^"]*)"/, 'attribute.value'],
[/'([^']*)'/, 'attribute.value'],
[/[\w\-]+/, 'attribute.name'],
[/=/, 'delimiter'],
[/[ \t\r\n]+/], // whitespace
],
// -- BEGIN <script> tags handling
// After <script
script: [
[/type/, 'attribute.name', '@scriptAfterType'],
[/"([^"]*)"/, 'attribute.value'],
[/'([^']*)'/, 'attribute.value'],
[/[\w\-]+/, 'attribute.name'],
[/=/, 'delimiter'],
[/>/, { token: 'delimiter', next: '@scriptEmbedded', nextEmbedded: 'text/javascript' }],
[/[ \t\r\n]+/], // whitespace
[/(<\/)(script\s*)(>)/, ['delimiter', 'tag', { token: 'delimiter', next: '@pop' }]]
],
// After <script ... type
scriptAfterType: [
[/=/, 'delimiter', '@scriptAfterTypeEquals'],
[/>/, { token: 'delimiter', next: '@scriptEmbedded', nextEmbedded: 'text/javascript' }], // cover invalid e.g. <script type>
[/[ \t\r\n]+/], // whitespace
[/<\/script\s*>/, { token: '@rematch', next: '@pop' }]
],
// After <script ... type =
scriptAfterTypeEquals: [
[/"([^"]*)"/, { token: 'attribute.value', switchTo: '@scriptWithCustomType.$1' }],
[/'([^']*)'/, { token: 'attribute.value', switchTo: '@scriptWithCustomType.$1' }],
[/>/, { token: 'delimiter', next: '@scriptEmbedded', nextEmbedded: 'text/javascript' }], // cover invalid e.g. <script type=>
[/[ \t\r\n]+/], // whitespace
[/<\/script\s*>/, { token: '@rematch', next: '@pop' }]
],
// After <script ... type = $S2
scriptWithCustomType: [
[/>/, { token: 'delimiter', next: '@scriptEmbedded.$S2', nextEmbedded: '$S2' }],
[/"([^"]*)"/, 'attribute.value'],
[/'([^']*)'/, 'attribute.value'],
[/[\w\-]+/, 'attribute.name'],
[/=/, 'delimiter'],
[/[ \t\r\n]+/], // whitespace
[/<\/script\s*>/, { token: '@rematch', next: '@pop' }]
],
scriptEmbedded: [
[/<\/script/, { token: '@rematch', next: '@pop', nextEmbedded: '@pop' }],
[/[^<]+/, '']
],
// -- END <script> tags handling
// -- BEGIN <style> tags handling
// After <style
style: [
[/type/, 'attribute.name', '@styleAfterType'],
[/"([^"]*)"/, 'attribute.value'],
[/'([^']*)'/, 'attribute.value'],
[/[\w\-]+/, 'attribute.name'],
[/=/, 'delimiter'],
[/>/, { token: 'delimiter', next: '@styleEmbedded', nextEmbedded: 'text/css' }],
[/[ \t\r\n]+/], // whitespace
[/(<\/)(style\s*)(>)/, ['delimiter', 'tag', { token: 'delimiter', next: '@pop' }]]
],
// After <style ... type
styleAfterType: [
[/=/, 'delimiter', '@styleAfterTypeEquals'],
[/>/, { token: 'delimiter', next: '@styleEmbedded', nextEmbedded: 'text/css' }], // cover invalid e.g. <style type>
[/[ \t\r\n]+/], // whitespace
[/<\/style\s*>/, { token: '@rematch', next: '@pop' }]
],
// After <style ... type =
styleAfterTypeEquals: [
[/"([^"]*)"/, { token: 'attribute.value', switchTo: '@styleWithCustomType.$1' }],
[/'([^']*)'/, { token: 'attribute.value', switchTo: '@styleWithCustomType.$1' }],
[/>/, { token: 'delimiter', next: '@styleEmbedded', nextEmbedded: 'text/css' }], // cover invalid e.g. <style type=>
[/[ \t\r\n]+/], // whitespace
[/<\/style\s*>/, { token: '@rematch', next: '@pop' }]
],
// After <style ... type = $S2
styleWithCustomType: [
[/>/, { token: 'delimiter', next: '@styleEmbedded.$S2', nextEmbedded: '$S2' }],
[/"([^"]*)"/, 'attribute.value'],
[/'([^']*)'/, 'attribute.value'],
[/[\w\-]+/, 'attribute.name'],
[/=/, 'delimiter'],
[/[ \t\r\n]+/], // whitespace
[/<\/style\s*>/, { token: '@rematch', next: '@pop' }]
],
styleEmbedded: [
[/<\/style/, { token: '@rematch', next: '@pop', nextEmbedded: '@pop' }],
[/[^<]+/, '']
],
// -- END <style> tags handling
},
};
# Header 1 #
## Header 2 ##
### Header 3 ### (Hashes on right are optional)
## Markdown plus h2 with a custom ID ## {#id-goes-here}
[Link back to H2](#id-goes-here)
<!-- html madness -->
<div class="custom-class" markdown="1">
<div>
nested div
</div>
<script type='text/x-koka'>
function( x: int ) { return x*x; }
</script>
This is a div _with_ underscores
and a & <b class="bold">bold</b> element.
<style>
body { font: "Consolas" }
</style>
</div>
* Bullet lists are easy too
- Another one
+ Another one
This is a paragraph, which is text surrounded by
whitespace. Paragraphs can be on one
line (or many), and can drone on for hours.
Now some inline markup like _italics_, **bold**,
and `code()`. Note that underscores
in_words_are ignored.
````dafny
method Foo() {
requires "github style code blocks"
}
````
````application/json
{ value: ["or with a mime type"] }
````
> Blockquotes are like quoted text in email replies
>> And, they can be nested
1. A numbered list
2. Which is numbered
3. With periods and a space
And now some code:
// Code is just text indented a bit
which(is_easy) to_remember();
And a block
~~~
// Markdown extra adds un-indented code blocks too
if (this_is_more_code == true && !indented) {
// tild wrapped code blocks, also not indented
}
~~~
Text with
two trailing spaces
(on the right)
can be used
for things like poems
### Horizontal rules
* * * *
****
--------------------------
![picture alt](/images/photo.jpeg "Title is optional")
## Markdown plus tables ##
| Header | Header | Right |
| ------ | ------ | -----: |
| Cell | Cell | $10 |
| Cell | Cell | $20 |
* Outer pipes on tables are optional
* Colon used for alignment (right versus left)
## Markdown plus definition lists ##
Bottled water
: $ 1.25
: $ 1.55 (Large)
Milk
Pop
: $ 1.75
* Multiple definitions and terms are possible
* Definitions can include multiple paragraphs too
*[ABBR]: Markdown plus abbreviations (produces an <abbr> tag)
// Difficulty: "Ultra-Violence"
// Language definition for Markdown
// Quite complex definition mostly due to almost full inclusion
// of the HTML mode (so we can properly match nested HTML tag definitions)
return {
defaultToken: '',
tokenPostfix: '.md',
// escape codes
control: /[\\`*_\[\]{}()#+\-\.!]/,
noncontrol: /[^\\`*_\[\]{}()#+\-\.!]/,
escapes: /\\(?:@control)/,
// escape codes for javascript/CSS strings
jsescapes: /\\(?:[btnfr\\"']|[0-7][0-7]?|[0-3][0-7]{2})/,
// non matched elements
empty: [
'area', 'base', 'basefont', 'br', 'col', 'frame',
'hr', 'img', 'input', 'isindex', 'link', 'meta', 'param'
],
tokenizer: {
root: [
// headers (with #)
[/^(\s{0,3})(#+)((?:[^\\#]|@escapes)+)((?:#+)?)/, ['white', 'keyword', 'keyword', 'keyword']],
// headers (with =)
[/^\s*(=+|\-+)\s*$/, 'keyword'],
// headers (with ***)
[/^\s*((\*[ ]?)+)\s*$/, 'meta.separator'],
// quote
[/^\s*>+/, 'comment'],
// list (starting with * or number)
[/^\s*([\*\-+:]|\d+\.)\s/, 'keyword'],
// code block (4 spaces indent)
[/^(\t|[ ]{4})[^ ].*$/, 'string'],
// code block (3 tilde)
[/^\s*~~~\s*((?:\w|[\/\-#])+)?\s*$/, { token: 'string', next: '@codeblock' }],
// github style code blocks (with backticks and language)
[/^\s*```\s*((?:\w|[\/\-#])+)\s*$/, { token: 'string', next: '@codeblockgh', nextEmbedded: '$1' }],
// github style code blocks (with backticks but no language)
[/^\s*```\s*$/, { token: 'string', next: '@codeblock' }],
// markup within lines
{ include: '@linecontent' },
],
codeblock: [
[/^\s*~~~\s*$/, { token: 'string', next: '@pop' }],
[/^\s*```\s*$/, { token: 'string', next: '@pop' }],
[/.*$/, 'variable.source'],
],
// github style code blocks
codeblockgh: [
[/```\s*$/, { token: 'variable.source', next: '@pop', nextEmbedded: '@pop' }],
[/[^`]+/, 'variable.source'],
],
linecontent: [
// escapes
[/&\w+;/, 'string.escape'],
[/@escapes/, 'escape'],
// various markup
[/\b__([^\\_]|@escapes|_(?!_))+__\b/, 'strong'],
[/\*\*([^\\*]|@escapes|\*(?!\*))+\*\*/, 'strong'],
[/\b_[^_]+_\b/, 'emphasis'],
[/\*([^\\*]|@escapes)+\*/, 'emphasis'],
[/`([^\\`]|@escapes)+`/, 'variable'],
// links
[/\{+[^}]+\}+/, 'string.target'],
[/(!?\[)((?:[^\]\\]|@escapes)*)(\]\([^\)]+\))/, ['string.link', '', 'string.link']],
[/(!?\[)((?:[^\]\\]|@escapes)*)(\])/, 'string.link'],
// or html
{ include: 'html' },
],
// Note: it is tempting to rather switch to the real HTML mode instead of building our own here
// but currently there is a limitation in Monarch that prevents us from doing it: The opening
// '<' would start the HTML mode, however there is no way to jump 1 character back to let the
// HTML mode also tokenize the opening angle bracket. Thus, even though we could jump to HTML,
// we cannot correctly tokenize it in that mode yet.
html: [
// html tags
[/<(\w+)\/>/, 'tag'],
[/<(\w+)/, {
cases: {
'@empty': { token: 'tag', next: '@tag.$1' },
'@default': { token: 'tag', next: '@tag.$1' }
}
}],
[/<\/(\w+)\s*>/, { token: 'tag' }],
[/<!--/, 'comment', '@comment']
],
comment: [
[/[^<\-]+/, 'comment.content'],
[/-->/, 'comment', '@pop'],
[/<!--/, 'comment.content.invalid'],
[/[<\-]/, 'comment.content']
],
// Almost full HTML tag matching, complete with embedded scripts & styles
tag: [
[/[ \t\r\n]+/, 'white'],
[/(type)(\s*=\s*)(")([^"]+)(")/, ['attribute.name.html', 'delimiter.html', 'string.html',
{ token: 'string.html', switchTo: '@tag.$S2.$4' },
'string.html']],
[/(type)(\s*=\s*)(')([^']+)(')/, ['attribute.name.html', 'delimiter.html', 'string.html',
{ token: 'string.html', switchTo: '@tag.$S2.$4' },
'string.html']],
[/(\w+)(\s*=\s*)("[^"]*"|'[^']*')/, ['attribute.name.html', 'delimiter.html', 'string.html']],
[/\w+/, 'attribute.name.html'],
[/\/>/, 'tag', '@pop'],
[/>/, {
cases: {
'$S2==style': { token: 'tag', switchTo: 'embeddedStyle', nextEmbedded: 'text/css' },
'$S2==script': {
cases: {
'$S3': { token: 'tag', switchTo: 'embeddedScript', nextEmbedded: '$S3' },
'@default': { token: 'tag', switchTo: 'embeddedScript', nextEmbedded: 'text/javascript' }
}
},
'@default': { token: 'tag', next: '@pop' }
}
}],
],
embeddedStyle: [
[/[^<]+/, ''],
[/<\/style\s*>/, { token: '@rematch', next: '@pop', nextEmbedded: '@pop' }],
[/</, '']
],
embeddedScript: [
[/[^<]+/, ''],
[/<\/script\s*>/, { token: '@rematch', next: '@pop', nextEmbedded: '@pop' }],
[/</, '']
],
}
};
#
# This program evaluates polynomials. It first asks for the coefficients
# of a polynomial, which must be entered on one line, highest-order first.
# It then requests values of x and will compute the value of the poly for
# each x. It will repeatly ask for x values, unless you the user enters
# a blank line. It that case, it will ask for another polynomial. If the
# user types quit for either input, the program immediately exits.
#
#
# Function to evaluate a polynomial at x. The polynomial is given
# as a list of coefficients, from the greatest to the least.
def polyval(x, coef)
sum = 0
coef = coef.clone # Don't want to destroy the original
while true
sum += coef.shift # Add and remove the next coef
break if coef.empty? # If no more, done entirely.
sum *= x # This happens the right number of times.
end
return sum
end
#
# Function to read a line containing a list of integers and return
# them as an array of integers. If the string conversion fails, it
# throws TypeError. If the input line is the word 'quit', then it
# converts it to an end-of-file exception
def readints(prompt)
# Read a line
print prompt
line = readline.chomp
raise EOFError.new if line == 'quit' # You can also use a real EOF.
# Go through each item on the line, converting each one and adding it
# to retval.
retval = [ ]
for str in line.split(/\s+/)
if str =~ /^\-?\d+$/
retval.push(str.to_i)
else
raise TypeError.new
end
end
return retval
end
#
# Take a coeff and an exponent and return the string representation, ignoring
# the sign of the coefficient.
def term_to_str(coef, exp)
ret = ""
# Show coeff, unless it's 1 or at the right
coef = coef.abs
ret = coef.to_s unless coef == 1 && exp > 0
ret += "x" if exp > 0 # x if exponent not 0
ret += "^" + exp.to_s if exp > 1 # ^exponent, if > 1.
return ret
end
#
# Create a string of the polynomial in sort-of-readable form.
def polystr(p)
# Get the exponent of first coefficient, plus 1.
exp = p.length
# Assign exponents to each term, making pairs of coeff and exponent,
# Then get rid of the zero terms.
p = (p.map { |c| exp -= 1; [ c, exp ] }).select { |p| p[0] != 0 }
# If there's nothing left, it's a zero
return "0" if p.empty?
# *** Now p is a non-empty list of [ coef, exponent ] pairs. ***
# Convert the first term, preceded by a "-" if it's negative.
result = (if p[0][0] < 0 then "-" else "" end) + term_to_str(*p[0])
# Convert the rest of the terms, in each case adding the appropriate
# + or - separating them.
for term in p[1...p.length]
# Add the separator then the rep. of the term.
result += (if term[0] < 0 then " - " else " + " end) +
term_to_str(*term)
end
return result
end
#
# Run until some kind of endfile.
begin
# Repeat until an exception or quit gets us out.
while true
# Read a poly until it works. An EOF will except out of the
# program.
print "\n"
begin
poly = readints("Enter a polynomial coefficients: ")
rescue TypeError
print "Try again.\n"
retry
end
break if poly.empty?
# Read and evaluate x values until the user types a blank line.
# Again, an EOF will except out of the pgm.
while true
# Request an integer.
print "Enter x value or blank line: "
x = readline.chomp
break if x == ''
raise EOFError.new if x == 'quit'
# If it looks bad, let's try again.
if x !~ /^\-?\d+$/
print "That doesn't look like an integer. Please try again.\n"
next
end
# Convert to an integer and print the result.
x = x.to_i
print "p(x) = ", polystr(poly), "\n"
print "p(", x, ") = ", polyval(x, poly), "\n"
end
end
rescue EOFError
print "\n=== EOF ===\n"
rescue Interrupt, SignalException
print "\n=== Interrupted ===\n"
else
print "--- Bye ---\n"
end
// Difficulty: "Nightmare!"
/*
Ruby language definition
Quite a complex language due to elaborate escape sequences
and quoting of literate strings/regular expressions, and
an 'end' keyword that does not always apply to modifiers like until and while,
and a 'do' keyword that sometimes starts a block, but sometimes is part of
another statement (like 'while').
(1) end blocks:
'end' may end declarations like if or until, but sometimes 'if' or 'until'
are modifiers where there is no 'end'. Also, 'do' sometimes starts a block
that is ended by 'end', but sometimes it is part of a 'while', 'for', or 'until'
To do proper brace matching we do some elaborate state manipulation.
some examples:
until bla do
work until tired
list.each do
foo if test
end
end
or
if test
foo (if test then x end)
bar if bla
end
or, how about using class as a property..
class Foo
def endpoint
self.class.endpoint || routes
end
end
(2) quoting:
there are many kinds of strings and escape sequences. But also, one can
start many string-like things as '%qx' where q specifies the kind of string
(like a command, escape expanded, regular expression, symbol etc.), and x is
some character and only another 'x' ends the sequence. Except for brackets
where the closing bracket ends the sequence.. and except for a nested bracket
inside the string like entity. Also, such strings can contain interpolated
ruby expressions again (and span multiple lines). Moreover, expanded
regular expression can also contain comments.
*/
return {
tokenPostfix: '.ruby',
keywords: [
'__LINE__', '__ENCODING__', '__FILE__', 'BEGIN', 'END', 'alias', 'and', 'begin',
'break', 'case', 'class', 'def', 'defined?', 'do', 'else', 'elsif', 'end',
'ensure', 'for', 'false', 'if', 'in', 'module', 'next', 'nil', 'not', 'or', 'redo',
'rescue', 'retry', 'return', 'self', 'super', 'then', 'true', 'undef', 'unless',
'until', 'when', 'while', 'yield',
],
keywordops: [
'::', '..', '...', '?', ':', '=>'
],
builtins: [
'require', 'public', 'private', 'include', 'extend', 'attr_reader',
'protected', 'private_class_method', 'protected_class_method', 'new'
],
// these are closed by 'end' (if, while and until are handled separately)
declarations: [
'module', 'class', 'def', 'case', 'do', 'begin', 'for', 'if', 'while', 'until', 'unless'
],
linedecls: [
'def', 'case', 'do', 'begin', 'for', 'if', 'while', 'until', 'unless'
],
operators: [
'^', '&', '|', '<=>', '==', '===', '!~', '=~', '>', '>=', '<', '<=', '<<', '>>', '+',
'-', '*', '/', '%', '**', '~', '+@', '-@', '[]', '[]=', '`',
'+=', '-=', '*=', '**=', '/=', '^=', '%=', '<<=', '>>=', '&=', '&&=', '||=', '|='
],
brackets: [
{ open: '(', close: ')', token: 'delimiter.parenthesis' },
{ open: '{', close: '}', token: 'delimiter.curly' },
{ open: '[', close: ']', token: 'delimiter.square' }
],
// we include these common regular expressions
symbols: /[=><!~?:&|+\-*\/\^%\.]+/,
// escape sequences
escape: /(?:[abefnrstv\\"'\n\r]|[0-7]{1,3}|x[0-9A-Fa-f]{1,2}|u[0-9A-Fa-f]{4})/,
escapes: /\\(?:C\-(@escape|.)|c(@escape|.)|@escape)/,
decpart: /\d(_?\d)*/,
decimal: /0|@decpart/,
delim: /[^a-zA-Z0-9\s\n\r]/,
heredelim: /(?:\w+|'[^']*'|"[^"]*"|`[^`]*`)/,
regexpctl: /[(){}\[\]\$\^|\-*+?\.]/,
regexpesc: /\\(?:[AzZbBdDfnrstvwWn0\\\/]|@regexpctl|c[A-Z]|x[0-9a-fA-F]{2}|u[0-9a-fA-F]{4})?/,
// The main tokenizer for our languages
tokenizer: {
// Main entry.
// root.<decl> where decl is the current opening declaration (like 'class')
root: [
// identifiers and keywords
// most complexity here is due to matching 'end' correctly with declarations.
// We distinguish a declaration that comes first on a line, versus declarations further on a line (which are most likey modifiers)
[/^(\s*)([a-z_]\w*[!?=]?)/, ['white',
{
cases: {
'for|until|while': { token: 'keyword.$2', next: '@dodecl.$2' },
'@declarations': { token: 'keyword.$2', next: '@root.$2' },
'end': { token: 'keyword.$S2', next: '@pop' },
'@keywords': 'keyword',
'@builtins': 'predefined',
'@default': 'identifier'
}
}]],
[/[a-z_]\w*[!?=]?/,
{
cases: {
'if|unless|while|until': { token: 'keyword.$0x', next: '@modifier.$0x' },
'for': { token: 'keyword.$2', next: '@dodecl.$2' },
'@linedecls': { token: 'keyword.$0', next: '@root.$0' },
'end': { token: 'keyword.$S2', next: '@pop' },
'@keywords': 'keyword',
'@builtins': 'predefined',
'@default': 'identifier'
}
}],
[/[A-Z][\w]*[!?=]?/, 'constructor.identifier'], // constant
[/\$[\w]*/, 'global.constant'], // global
[/@[\w]*/, 'namespace.instance.identifier'], // instance
[/@@[\w]*/, 'namespace.class.identifier'], // class
// here document
[/<<[-~](@heredelim).*/, { token: 'string.heredoc.delimiter', next: '@heredoc.$1' }],
[/[ \t\r\n]+<<(@heredelim).*/, { token: 'string.heredoc.delimiter', next: '@heredoc.$1' }],
[/^<<(@heredelim).*/, { token: 'string.heredoc.delimiter', next: '@heredoc.$1' }],
// whitespace
{ include: '@whitespace' },
// strings
[/"/, { token: 'string.d.delim', next: '@dstring.d."' }],
[/'/, { token: 'string.sq.delim', next: '@sstring.sq' }],
// % literals. For efficiency, rematch in the 'pstring' state
[/%([rsqxwW]|Q?)/, { token: '@rematch', next: 'pstring' }],
// commands and symbols
[/`/, { token: 'string.x.delim', next: '@dstring.x.`' }],
[/:(\w|[$@])\w*[!?=]?/, 'string.s'],
[/:"/, { token: 'string.s.delim', next: '@dstring.s."' }],
[/:'/, { token: 'string.s.delim', next: '@sstring.s' }],
// regular expressions. Lookahead for a (not escaped) closing forwardslash on the same line
[/\/(?=(\\\/|[^\/\n])+\/)/, { token: 'regexp.delim', next: '@regexp' }],
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/@symbols/, {
cases: {
'@keywordops': 'keyword',
'@operators': 'operator',
'@default': ''
}
}],
[/[;,]/, 'delimiter'],
// numbers
[/0[xX][0-9a-fA-F](_?[0-9a-fA-F])*/, 'number.hex'],
[/0[_oO][0-7](_?[0-7])*/, 'number.octal'],
[/0[bB][01](_?[01])*/, 'number.binary'],
[/0[dD]@decpart/, 'number'],
[/@decimal((\.@decpart)?([eE][\-+]?@decpart)?)/, {
cases: {
'$1': 'number.float',
'@default': 'number'
}
}],
],
// used to not treat a 'do' as a block opener if it occurs on the same
// line as a 'do' statement: 'while|until|for'
// dodecl.<decl> where decl is the declarations started, like 'while'
dodecl: [
[/^/, { token: '', switchTo: '@root.$S2' }], // get out of do-skipping mode on a new line
[/[a-z_]\w*[!?=]?/, {
cases: {
'end': { token: 'keyword.$S2', next: '@pop' }, // end on same line
'do': { token: 'keyword', switchTo: '@root.$S2' }, // do on same line: not an open bracket here
'@linedecls': { token: '@rematch', switchTo: '@root.$S2' }, // other declaration on same line: rematch
'@keywords': 'keyword',
'@builtins': 'predefined',
'@default': 'identifier'
}
}],
{ include: '@root' }
],
// used to prevent potential modifiers ('if|until|while|unless') to match
// with 'end' keywords.
// modifier.<decl>x where decl is the declaration starter, like 'if'
modifier: [
[/^/, '', '@pop'], // it was a modifier: get out of modifier mode on a new line
[/[a-z_]\w*[!?=]?/, {
cases: {
'end': { token: 'keyword.$S2', next: '@pop' }, // end on same line
'then|else|elsif|do': { token: 'keyword', switchTo: '@root.$S2' }, // real declaration and not a modifier
'@linedecls': { token: '@rematch', switchTo: '@root.$S2' }, // other declaration => not a modifier
'@keywords': 'keyword',
'@builtins': 'predefined',
'@default': 'identifier'
}
}],
{ include: '@root' }
],
// single quote strings (also used for symbols)
// sstring.<kind> where kind is 'sq' (single quote) or 's' (symbol)
sstring: [
[/[^\\']+/, 'string.$S2'],
[/\\\\|\\'|\\$/, 'string.$S2.escape'],
[/\\./, 'string.$S2.invalid'],
[/'/, { token: 'string.$S2.delim', next: '@pop' }]
],
// double quoted "string".
// dstring.<kind>.<delim> where kind is 'd' (double quoted), 'x' (command), or 's' (symbol)
// and delim is the ending delimiter (" or `)
dstring: [
[/[^\\`"#]+/, 'string.$S2'],
[/#/, 'string.$S2.escape', '@interpolated'],
[/\\$/, 'string.$S2.escape'],
[/@escapes/, 'string.$S2.escape'],
[/\\./, 'string.$S2.escape.invalid'],
[/[`"]/, {
cases: {
'$#==$S3': { token: 'string.$S2.delim', next: '@pop' },
'@default': 'string.$S2'
}
}]
],
// literal documents
// heredoc.<close> where close is the closing delimiter
heredoc: [
[/^(\s*)(@heredelim)$/, {
cases: {
'$2==$S2': ['string.heredoc', { token: 'string.heredoc.delimiter', next: '@pop' }],
'@default': ['string.heredoc', 'string.heredoc']
}
}],
[/.*/, 'string.heredoc'],
],
// interpolated sequence
interpolated: [
[/\$\w*/, 'global.constant', '@pop'],
[/@\w*/, 'namespace.class.identifier', '@pop'],
[/@@\w*/, 'namespace.instance.identifier', '@pop'],
[/[{]/, { token: 'string.escape.curly', switchTo: '@interpolated_compound' }],
['', '', '@pop'], // just a # is interpreted as a #
],
// any code
interpolated_compound: [
[/[}]/, { token: 'string.escape.curly', next: '@pop' }],
{ include: '@root' },
],
// %r quoted regexp
// pregexp.<open>.<close> where open/close are the open/close delimiter
pregexp: [
{ include: '@whitespace' },
// turns out that you can quote using regex control characters, aargh!
// for example; %r|kgjgaj| is ok (even though | is used for alternation)
// so, we need to match those first
[/[^\(\{\[\\]/, {
cases: {
'$#==$S3': { token: 'regexp.delim', next: '@pop' },
'$#==$S2': { token: 'regexp.delim', next: '@push' }, // nested delimiters are allowed..
'~[)}\\]]': '@brackets.regexp.escape.control',
'~@regexpctl': 'regexp.escape.control',
'@default': 'regexp'
}
}],
{ include: '@regexcontrol' },
],
// We match regular expression quite precisely
regexp: [
{ include: '@regexcontrol' },
[/[^\\\/]/, 'regexp'],
['/[ixmp]*', { token: 'regexp.delim' }, '@pop'],
],
regexcontrol: [
[/(\{)(\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']],
[/\(\?#/, { token: 'regexp.escape.control', next: '@regexpcomment' }],
[/[()]/, '@brackets.regexp.escape.control'],
[/@regexpctl/, 'regexp.escape.control'],
[/\\$/, 'regexp.escape'],
[/@regexpesc/, 'regexp.escape'],
[/\\\./, 'regexp.invalid'],
[/#/, 'regexp.escape', '@interpolated'],
],
regexrange: [
[/-/, 'regexp.escape.control'],
[/\^/, 'regexp.invalid'],
[/\\$/, 'regexp.escape'],
[/@regexpesc/, 'regexp.escape'],
[/[^\]]/, 'regexp'],
[/\]/, '@brackets.regexp.escape.control', '@pop'],
],
regexpcomment: [
[/[^)]+/, 'comment'],
[/\)/, { token: 'regexp.escape.control', next: '@pop' }]
],
// % quoted strings
// A bit repetitive since we need to often special case the kind of ending delimiter
pstring: [
[/%([qws])\(/, { token: 'string.$1.delim', switchTo: '@qstring.$1.(.)' }],
[/%([qws])\[/, { token: 'string.$1.delim', switchTo: '@qstring.$1.[.]' }],
[/%([qws])\{/, { token: 'string.$1.delim', switchTo: '@qstring.$1.{.}' }],
[/%([qws])</, { token: 'string.$1.delim', switchTo: '@qstring.$1.<.>' }],
[/%([qws])(@delim)/, { token: 'string.$1.delim', switchTo: '@qstring.$1.$2.$2' }],
[/%r\(/, { token: 'regexp.delim', switchTo: '@pregexp.(.)' }],
[/%r\[/, { token: 'regexp.delim', switchTo: '@pregexp.[.]' }],
[/%r\{/, { token: 'regexp.delim', switchTo: '@pregexp.{.}' }],
[/%r</, { token: 'regexp.delim', switchTo: '@pregexp.<.>' }],
[/%r(@delim)/, { token: 'regexp.delim', switchTo: '@pregexp.$1.$1' }],
[/%(x|W|Q?)\(/, { token: 'string.$1.delim', switchTo: '@qqstring.$1.(.)' }],
[/%(x|W|Q?)\[/, { token: 'string.$1.delim', switchTo: '@qqstring.$1.[.]' }],
[/%(x|W|Q?)\{/, { token: 'string.$1.delim', switchTo: '@qqstring.$1.{.}' }],
[/%(x|W|Q?)</, { token: 'string.$1.delim', switchTo: '@qqstring.$1.<.>' }],
[/%(x|W|Q?)(@delim)/, { token: 'string.$1.delim', switchTo: '@qqstring.$1.$2.$2' }],
[/%([rqwsxW]|Q?)./, { token: 'invalid', next: '@pop' }], // recover
[/./, { token: 'invalid', next: '@pop' }], // recover
],
// non-expanded quoted string.
// qstring.<kind>.<open>.<close>
// kind = q|w|s (single quote, array, symbol)
// open = open delimiter
// close = close delimiter
qstring: [
[/\\$/, 'string.$S2.escape'],
[/\\./, 'string.$S2.escape'],
[/./, {
cases: {
'$#==$S4': { token: 'string.$S2.delim', next: '@pop' },
'$#==$S3': { token: 'string.$S2.delim', next: '@push' }, // nested delimiters are allowed..
'@default': 'string.$S2'
}
}],
],
// expanded quoted string.
// qqstring.<kind>.<open>.<close>
// kind = Q|W|x (double quote, array, command)
// open = open delimiter
// close = close delimiter
qqstring: [
[/#/, 'string.$S2.escape', '@interpolated'],
{ include: '@qstring' }
],
// whitespace & comments
whitespace: [
[/[ \t\r\n]+/, ''],
[/^\s*=begin\b/, 'comment', '@comment'],
[/#.*$/, 'comment'],
],
comment: [
[/[^=]+/, 'comment'],
[/^\s*=begin\b/, 'comment.invalid'], // nested comment
[/^\s*=end\b.*/, 'comment', '@pop'],
[/[=]/, 'comment']
],
}
};
from Tkinter import *
import Pmw, string
class SLabel(Frame):
""" SLabel defines a 2-sided label within a Frame. The
left hand label has blue letters the right has white letters """
def __init__(self, master, leftl, rightl):
Frame.__init__(self, master, bg='gray40')
self.pack(side=LEFT, expand=YES, fill=BOTH)
Label(self, text=leftl, fg='steelblue1',
font=("arial", 6, "bold"), width=5, bg='gray40').pack(
side=LEFT, expand=YES, fill=BOTH)
Label(self, text=rightl, fg='white',
font=("arial", 6, "bold"), width=1, bg='gray40').pack(
side=RIGHT, expand=YES, fill=BOTH)
class Key(Button):
def __init__(self, master, font=('arial', 8, 'bold'),
fg='white',width=5, borderwidth=5, **kw):
kw['font'] = font
kw['fg'] = fg
kw['width'] = width
kw['borderwidth'] = borderwidth
apply(Button.__init__, (self, master), kw)
self.pack(side=LEFT, expand=NO, fill=NONE)
class Calculator(Frame):
def __init__(self, parent=None):
Frame.__init__(self, bg='gray40')
self.pack(expand=YES, fill=BOTH)
self.master.title('Tkinter Toolkit TT-42')
self.master.iconname('Tk-42')
self.calc = Evaluator() # This is our evaluator
self.buildCalculator() # Build the widgets
# This is an incomplete dictionary - a good exercise!
self.actionDict = {'second': self.doThis, 'mode': self.doThis,
'delete': self.doThis, 'alpha': self.doThis,
'stat': self.doThis, 'math': self.doThis,
'matrix': self.doThis, 'program': self.doThis,
'vars': self.doThis, 'clear': self.clearall,
'sin': self.doThis, 'cos': self.doThis,
'tan': self.doThis, 'up': self.doThis,
'X1': self.doThis, 'X2': self.doThis,
'log': self.doThis, 'ln': self.doThis,
'store': self.doThis, 'off': self.turnoff,
'neg': self.doThis, 'enter': self.doEnter,
}
self.current = ""
def doThis(self,action):
print '"%s" has not been implemented' % action
def turnoff(self, *args):
self.quit()
def clearall(self, *args):
self.current = ""
self.display.component('text').delete(1.0, END)
def doEnter(self, *args):
result = self.calc.runpython(self.current)
if result:
self.display.insert(END, '\n')
self.display.insert(END, '%s\n' % result, 'ans')
self.current = ""
def doKeypress(self, event):
key = event.char
if not key in ['\b']:
self.current = self.current + event.char
if key == '\b':
self.current = self.current[:-1]
def keyAction(self, key):
self.display.insert(END, key)
self.current = self.current + key
def evalAction(self, action):
try:
self.actionDict[action](action)
except KeyError:
pass
def buildCalculator(self):
FUN = 1 # Designates a Function
KEY = 0 # Designates a Key
KC1 = 'gray30' # Dark Keys
KC2 = 'gray50' # Light Keys
KC3 = 'steelblue1' # Light Blue Key
KC4 = 'steelblue' # Dark Blue Key
keys = [
[('2nd', '', '', KC3, FUN, 'second'), # Row 1
('Mode', 'Quit', '', KC1, FUN, 'mode'),
('Del', 'Ins', '', KC1, FUN, 'delete'),
('Alpha','Lock', '', KC2, FUN, 'alpha'),
('Stat', 'List', '', KC1, FUN, 'stat')],
[('Math', 'Test', 'A', KC1, FUN, 'math'), # Row 2
('Mtrx', 'Angle','B', KC1, FUN, 'matrix'),
('Prgm', 'Draw', 'C', KC1, FUN, 'program'),
('Vars', 'YVars','', KC1, FUN, 'vars'),
('Clr', '', '', KC1, FUN, 'clear')],
[('X-1', 'Abs', 'D', KC1, FUN, 'X1'), # Row 3
('Sin', 'Sin-1','E', KC1, FUN, 'sin'),
('Cos', 'Cos-1','F', KC1, FUN, 'cos'),
('Tan', 'Tan-1','G', KC1, FUN, 'tan'),
('^', 'PI', 'H', KC1, FUN, 'up')],
[('X2', 'Root', 'I', KC1, FUN, 'X2'), # Row 4
(',', 'EE', 'J', KC1, KEY, ','),
('(', '{', 'K', KC1, KEY, '('),
(')', '}', 'L', KC1, KEY, ')'),
('/', '', 'M', KC4, KEY, '/')],
[('Log', '10x', 'N', KC1, FUN, 'log'), # Row 5
('7', 'Un-1', 'O', KC2, KEY, '7'),
('8', 'Vn-1', 'P', KC2, KEY, '8'),
('9', 'n', 'Q', KC2, KEY, '9'),
('X', '[', 'R', KC4, KEY, '*')],
[('Ln', 'ex', 'S', KC1, FUN, 'ln'), # Row 6
('4', 'L4', 'T', KC2, KEY, '4'),
('5', 'L5', 'U', KC2, KEY, '5'),
('6', 'L6', 'V', KC2, KEY, '6'),
('-', ']', 'W', KC4, KEY, '-')],
[('STO', 'RCL', 'X', KC1, FUN, 'store'), # Row 7
('1', 'L1', 'Y', KC2, KEY, '1'),
('2', 'L2', 'Z', KC2, KEY, '2'),
('3', 'L3', '', KC2, KEY, '3'),
('+', 'MEM', '"', KC4, KEY, '+')],
[('Off', '', '', KC1, FUN, 'off'), # Row 8
('0', '', '', KC2, KEY, '0'),
('.', ':', '', KC2, KEY, '.'),
('(-)', 'ANS', '?', KC2, FUN, 'neg'),
('Enter','Entry','', KC4, FUN, 'enter')]]
self.display = Pmw.ScrolledText(self, hscrollmode='dynamic',
vscrollmode='dynamic', hull_relief='sunken',
hull_background='gray40', hull_borderwidth=10,
text_background='honeydew4', text_width=16,
text_foreground='black', text_height=6,
text_padx=10, text_pady=10, text_relief='groove',
text_font=('arial', 12, 'bold'))
self.display.pack(side=TOP, expand=YES, fill=BOTH)
self.display.tag_config('ans', foreground='white')
self.display.component('text').bind('<Key>', self.doKeypress)
self.display.component('text').bind('<Return>', self.doEnter)
for row in keys:
rowa = Frame(self, bg='gray40')
rowb = Frame(self, bg='gray40')
for p1, p2, p3, color, ktype, func in row:
if ktype == FUN:
a = lambda s=self, a=func: s.evalAction(a)
else:
a = lambda s=self, k=func: s.keyAction(k)
SLabel(rowa, p2, p3)
Key(rowb, text=p1, bg=color, command=a)
rowa.pack(side=TOP, expand=YES, fill=BOTH)
rowb.pack(side=TOP, expand=YES, fill=BOTH)
class Evaluator:
def __init__(self):
self.myNameSpace = {}
self.runpython("from math import *")
def runpython(self, code):
try:
return 'eval(code, self.myNameSpace, self.myNameSpace)'
except SyntaxError:
try:
exec code in self.myNameSpace, self.myNameSpace
except:
return 'Error'
Calculator().mainloop()
// Difficulty: "Moderate"
// Python language definition.
// Only trickiness is that we need to check strings before identifiers
// since they have letter prefixes. We also treat ':' as an @open bracket
// in order to get auto identation.
return {
defaultToken: '',
tokenPostfix: '.python',
keywords: [
'and',
'as',
'assert',
'break',
'class',
'continue',
'def',
'del',
'elif',
'else',
'except',
'exec',
'finally',
'for',
'from',
'global',
'if',
'import',
'in',
'is',
'lambda',
'None',
'not',
'or',
'pass',
'print',
'raise',
'return',
'self',
'try',
'while',
'with',
'yield',
'int',
'float',
'long',
'complex',
'hex',
'abs',
'all',
'any',
'apply',
'basestring',
'bin',
'bool',
'buffer',
'bytearray',
'callable',
'chr',
'classmethod',
'cmp',
'coerce',
'compile',
'complex',
'delattr',
'dict',
'dir',
'divmod',
'enumerate',
'eval',
'execfile',
'file',
'filter',
'format',
'frozenset',
'getattr',
'globals',
'hasattr',
'hash',
'help',
'id',
'input',
'intern',
'isinstance',
'issubclass',
'iter',
'len',
'locals',
'list',
'map',
'max',
'memoryview',
'min',
'next',
'object',
'oct',
'open',
'ord',
'pow',
'print',
'property',
'reversed',
'range',
'raw_input',
'reduce',
'reload',
'repr',
'reversed',
'round',
'set',
'setattr',
'slice',
'sorted',
'staticmethod',
'str',
'sum',
'super',
'tuple',
'type',
'unichr',
'unicode',
'vars',
'xrange',
'zip',
'True',
'False',
'__dict__',
'__methods__',
'__members__',
'__class__',
'__bases__',
'__name__',
'__mro__',
'__subclasses__',
'__init__',
'__import__'
],
brackets: [
{ open: '{', close: '}', token: 'delimiter.curly' },
{ open: '[', close: ']', token: 'delimiter.bracket' },
{ open: '(', close: ')', token: 'delimiter.parenthesis' }
],
tokenizer: {
root: [
{ include: '@whitespace' },
{ include: '@numbers' },
{ include: '@strings' },
[/[,:;]/, 'delimiter'],
[/[{}\[\]()]/, '@brackets'],
[/@[a-zA-Z]\w*/, 'tag'],
[/[a-zA-Z]\w*/, {
cases: {
'@keywords': 'keyword',
'@default': 'identifier'
}
}]
],
// Deal with white space, including single and multi-line comments
whitespace: [
[/\s+/, 'white'],
[/(^#.*$)/, 'comment'],
[/('''.*''')|(""".*""")/, 'string'],
[/'''.*$/, 'string', '@endDocString'],
[/""".*$/, 'string', '@endDblDocString']
],
endDocString: [
[/\\'/, 'string'],
[/.*'''/, 'string', '@popall'],
[/.*$/, 'string']
],
endDblDocString: [
[/\\"/, 'string'],
[/.*"""/, 'string', '@popall'],
[/.*$/, 'string']
],
// Recognize hex, negatives, decimals, imaginaries, longs, and scientific notation
numbers: [
[/-?0x([abcdef]|[ABCDEF]|\d)+[lL]?/, 'number.hex'],
[/-?(\d*\.)?\d+([eE][+\-]?\d+)?[jJ]?[lL]?/, 'number']
],
// Recognize strings, including those broken across lines with \ (but not without)
strings: [
[/'$/, 'string.escape', '@popall'],
[/'/, 'string.escape', '@stringBody'],
[/"$/, 'string.escape', '@popall'],
[/"/, 'string.escape', '@dblStringBody']
],
stringBody: [
[/[^\\']+$/, 'string', '@popall'],
[/[^\\']+/, 'string'],
[/\\./, 'string'],
[/'/, 'string.escape', '@popall'],
[/\\$/, 'string']
],
dblStringBody: [
[/[^\\"]+$/, 'string', '@popall'],
[/[^\\"]+/, 'string'],
[/\\./, 'string'],
[/"/, 'string.escape', '@popall'],
[/\\$/, 'string']
]
}
};
# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]
# each cell contains a value in {1, ..., 9}
cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]
# each row contains a digit at most once
rows_c = [ Distinct(X[i]) for i in range(9) ]
# each column contains a digit at most once
cols_c = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]
# each 3x3 square contains a digit at most once
sq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3) ]
sudoku_c = cells_c + rows_c + cols_c + sq_c
# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
(0,0,0,5,1,0,0,0,7),
(0,8,9,0,0,0,0,4,0),
(0,0,0,0,0,0,2,0,8),
(0,6,0,2,0,1,0,5,0),
(1,0,2,0,0,0,0,0,0),
(0,7,0,0,0,0,5,2,0),
(9,0,0,0,6,5,0,0,0),
(0,4,0,9,7,0,0,0,0))
instance_c = [ If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9) ]
s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print "failed to solve"
// Difficulty: "Moderate"
// This is the Python language definition but specialized for use with Z3
// See also: http://www.rise4fun.com/Z3Py
return {
// Set defaultToken to invalid to see what you do not tokenize yet
// defaultToken: 'invalid',
keywords: [
'and', 'del', 'from', 'not', 'while',
'as', 'elif', 'global', 'or', 'with',
'assert', 'else', 'if', 'pass', 'yield',
'break', 'except', 'import', 'print',
'class', 'exec', 'in', 'raise', 'continue', 'finally', 'is',
'return', 'def', 'for', 'lambda', 'try',
':','=',
'isinstance','__debug__',
],
operators: [
'+', '-', '*', '**', '/', '//', '%',
'<<', '>>', '&', '|', '^', '~',
'<', '>', '<=', '>=', '==', '!=', '<>',
'+=', '-=', '*=', '/=', '//=', '%=',
'&=', '|=', '^=', '>>=', '<<=', '**=',
],
builtins: [
'set_option', 'solve', 'simplify', 'Int', 'Real', 'Bool', 'open_log',
'append_log', 'is_sort', 'DeclareSort', 'Function', 'is_func_decl', 'is_expr',
'is_app', 'is_const', 'is_var', 'get_var_index', 'is_app_of',
'If', 'Distinct', 'Const', 'Consts', 'Var', 'is_bool',
'is_true', 'is_false', 'is_and', 'is_or', 'is_not', 'is_eq',
'BoolSort', 'BoolVal', 'Bools', 'BoolVector', 'FreshBool',
'Implies', 'Not', 'And', 'Or', 'MultiPattern', 'ForAll',
'Exists', 'is_int', 'is_real', 'is_int_value', 'is_rational_value',
'is_algebraic_value', 'IntSort', 'RealSort', 'IntVal',
'RealVal', 'RatVal', 'Q', 'Ints', 'Reals', 'IntVector', 'RealVector',
'FreshInt', 'FreshReal', 'ToReal', 'ToInt', 'IsInt',
'Sqrt', 'Cbrt', 'is_bv', 'BV2Int', 'BitVecSort', 'BitVecVal',
'BitVec', 'BitVecs', 'Concat', 'Extract', 'ULE', 'ULT',
'UGE', 'UGT', 'UDiv', 'URem', 'SRem', 'LShR', 'RotateLeft',
'RotateRight', 'SignExt', 'ZeroExt', 'RepeatBitVec',
'is_array', 'ArraySort', 'Array', 'Update', 'Store',
'Select', 'Map', 'K', 'CreateDatatypes', 'EnumSort', 'Solver',
'SolverFor', 'SimpleSolver', 'FixedPoint', 'Tactic', 'AndThen',
'Then', 'OrElse', 'ParOr', 'ParThen', 'ParAndThen',
'With', 'Repeat', 'TryFor', 'Probe', 'When', 'FailIf', 'Cond',
'substitute', 'Sum', 'Product', 'solve_using', 'prove', 'init', 'sat', 'unsat',
'unknown'
],
brackets: [
['(',')','delimiter.parenthesis'],
['{','}','delimiter.curly'],
['[',']','delimiter.square']
],
// operator symbols
symbols: /[=><!~&|+\-*\/\^%]+/,
delimiters: /[;=.@:,`]/,
// strings
escapes: /\\(?:[abfnrtv\\"'\n\r]|x[0-9A-Fa-f]{2}|[0-7]{3}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8}|N\{\w+\})/,
rawpre: /(?:[rR]|ur|Ur|uR|UR|br|Br|bR|BR)/,
strpre: /(?:[buBU])/,
// The main tokenizer for our languages
tokenizer: {
root: [
// strings: need to check first due to the prefix
[/@strpre?("""|''')/, { token: 'string.delim', bracket: '@open', next: '@mstring.$1' } ],
[/@strpre?"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/@strpre?'([^'\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/@strpre?(["'])/, { token: 'string.delim', bracket: '@open', next: '@string.$1' } ],
[/@rawpre("""|''')/, { token: 'string.delim', bracket: '@open', next: '@mrawstring.$1' } ],
[/@rawpre"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/@rawpre'([^'\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/@rawpre(["'])/, { token: 'string.delim', bracket: '@open', next: '@rawstring.$1' } ],
// identifiers and keywords
[/__[\w$]*/, 'predefined' ],
[/[a-z_$][\w$]*/, { cases: { '@keywords': 'keyword',
'@builtins': 'constructor.identifier',
'@default': 'identifier' } }],
[/[A-Z][\w]*/, { cases: { '~[A-Z0-9_]+': 'constructor.identifier',
'@builtins' : 'constructor.identifier',
'@default' : 'namespace.identifier' }}], // to show class names nicely
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/@symbols/, { cases: { '@keywords' : 'keyword',
'@operators': 'operator',
'@default' : '' } } ],
// numbers
[/\d*\.\d+([eE][\-+]?\d+)?/, 'number.float'],
[/0[xX][0-9a-fA-F]+[lL]?/, 'number.hex'],
[/0[bB][0-1]+[lL]?/, 'number.binary'],
[/(0[oO][0-7]+|0[0-7]+)[lL]?/, 'number.octal'],
[/(0|[1-9]\d*)[lL]?/, 'number'],
// delimiter: after number because of .\d floats
[':', { token: 'keyword', bracket: '@open' }], // bracket for indentation
[/@delimiters/, { cases: { '@keywords': 'keyword',
'@default': 'delimiter' }}],
],
comment: [
[/[^\/*]+/, 'comment' ],
[/\/\*/, 'comment', '@push' ], // nested comment
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
// Regular strings
mstring: [
{ include: '@strcontent' },
[/"""|'''/, { cases: { '$#==$S2': { token: 'string.delim', bracket: '@close', next: '@pop' },
'@default': { token: 'string' } } }],
[/["']/, 'string' ],
[/./, 'string.invalid'],
],
string: [
{ include: '@strcontent' },
[/["']/, { cases: { '$#==$S2': { token: 'string.delim', bracket: '@close', next: '@pop' },
'@default': { token: 'string' } } } ],
[/./, 'string.invalid'],
],
strcontent: [
[/[^\\"']+/, 'string'],
[/\\$/, 'string.escape'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
],
// Raw strings: we distinguish them to color escape sequences correctly
mrawstring: [
{ include: '@rawstrcontent' },
[/"""|'''/, { cases: { '$#==$S2': { token: 'string.delim', bracket: '@close', next: '@pop' },
'@default': { token: 'string' } } }],
[/["']/, 'string' ],
[/./, 'string.invalid'],
],
rawstring: [
{ include: '@rawstrcontent' },
[/["']/, { cases: { '$#==$S2': { token: 'string.delim', bracket: '@close', next: '@pop' },
'@default': { token: 'string' } } } ],
[/./, 'string.invalid'],
],
rawstrcontent: [
[/[^\\"']+/, 'string'],
[/\\["']/, 'string'],
[/\\u[0-9A-Fa-f]{4}/, 'string.escape'],
[/\\/, 'string' ],
],
// whitespace
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/#.*$/, 'comment'],
],
},
};
; This example illustrates different uses of the arrays
; supported in Z3.
; This includes Combinatory Array Logic (de Moura & Bjorner, FMCAD 2009).
;
(define-sort A () (Array Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun a1 () A)
(declare-fun a2 () A)
(declare-fun a3 () A)
(push) ; illustrate select-store
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)
(assert (not (= x y)))
(check-sat)
(pop)
(define-fun all1_array () A ((as const A) 1))
(simplify (select all1_array x))
(define-sort IntSet () (Array Int Bool))
(declare-fun a () IntSet)
(declare-fun b () IntSet)
(declare-fun c () IntSet)
(push) ; illustrate map
(assert (not (= ((_ map and) a b) ((_ map not) ((_ map or) ((_ map not) b) ((_ map not) a))))))
(check-sat)
(pop)
(push)
(assert (and (select ((_ map and) a b) x) (not (select a x))))
(check-sat)
(pop)
(push)
(assert (and (select ((_ map or) a b) x) (not (select a x))))
(check-sat)
(get-model)
(assert (and (not (select b x))))
(check-sat)
;; unsat, so there is no model.
(pop)
(push) ; illustrate default
(assert (= (default a1) 1))
(assert (not (= a1 ((as const A) 1))))
(check-sat)
(get-model)
(assert (= (default a2) 1))
(assert (not (= a1 a2)))
(check-sat)
(get-model)
(pop)
(exit)
// Difficulty: "Easy"
// SMT 2.0 language
// See http://www.rise4fun.com/z3 or http://www.smtlib.org/ for more information
return {
// Set defaultToken to invalid to see what you do not tokenize yet
// defaultToken: 'invalid',
keywords: [
'define-fun', 'define-const', 'assert', 'push', 'pop', 'assert', 'check-sat',
'declare-const', 'declare-fun', 'get-model', 'get-value', 'declare-sort',
'declare-datatypes', 'reset', 'eval', 'set-logic', 'help', 'get-assignment',
'exit', 'get-proof', 'get-unsat-core', 'echo', 'let', 'forall', 'exists',
'define-sort', 'set-option', 'get-option', 'set-info', 'check-sat-using', 'apply', 'simplify',
'display', 'as', '!', 'get-info', 'declare-map', 'declare-rel', 'declare-var', 'rule',
'query', 'get-user-tactics'
],
operators: [
'=', '>', '<', '<=', '>=', '=>', '+', '-', '*', '/',
],
builtins: [
'mod', 'div', 'rem', '^', 'to_real', 'and', 'or', 'not', 'distinct',
'to_int', 'is_int', '~', 'xor', 'if', 'ite', 'true', 'false', 'root-obj',
'sat', 'unsat', 'const', 'map', 'store', 'select', 'sat', 'unsat',
'bit1', 'bit0', 'bvneg', 'bvadd', 'bvsub', 'bvmul', 'bvsdiv', 'bvudiv', 'bvsrem',
'bvurem', 'bvsmod', 'bvule', 'bvsle', 'bvuge', 'bvsge', 'bvult',
'bvslt', 'bvugt', 'bvsgt', 'bvand', 'bvor', 'bvnot', 'bvxor', 'bvnand',
'bvnor', 'bvxnor', 'concat', 'sign_extend', 'zero_extend', 'extract',
'repeat', 'bvredor', 'bvredand', 'bvcomp', 'bvshl', 'bvlshr', 'bvashr',
'rotate_left', 'rotate_right', 'get-assertions'
],
brackets: [
['(',')','delimiter.parenthesis'],
['{','}','delimiter.curly'],
['[',']','delimiter.square']
],
// 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: { '@builtins': 'predefined.identifier',
'@keywords': 'keyword',
'@default': 'identifier' } }],
[/[A-Z][\w\-\.']*/, 'type.identifier' ],
[/[:][\w\-\.']*/, 'string.identifier' ],
[/[$?][\w\-\.']*/, 'constructor.identifier' ],
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/[()\[\]]/, '@brackets'],
[/@symbols/, { cases: { '@operators': 'predefined.operator',
'@default' : 'operator' } } ],
// numbers
[/\d*\.\d+([eE][\-+]?\d+)?/, 'number.float'],
[/0[xX][0-9a-fA-F]+/, 'number.hex'],
[/#[xX][0-9a-fA-F]+/, 'number.hex'],
[/#b[0-1]+/, 'number.binary'],
[/\d+/, 'number'],
// delimiter: after number because of .\d floats
[/[,.]/, 'delimiter'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, { token: 'string.quote', bracket: '@open', next: '@string' } ],
// user values
[/\{/, { token: 'string.curly', bracket: '@open', next: '@uservalue' } ],
],
uservalue: [
[/[^\\\}]+/, 'string' ],
[/\}/, { token: 'string.curly', bracket: '@close', next: '@pop' } ],
[/\\\}/, 'string.escape'],
[/./, 'string'] // recover
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/;.*$/, 'comment'],
],
},
};
digraph "If.try_if_then"
{
label = "If.try_if_then";
rankdir="TD";
node [fontname="Helvetica", shape=record, fontsize="12", color="lightblue", style="filled"];
edge [fontname="Helvetica", fontsize="10", color="black"];
subgraph "cluster_node_57"
{ /* block node_57 */
label = "";
node_57 [label = "Block [57]"];
node_58 [label = "Return [58@57]"];
node_50 -> node_58 [label = "mem", dir = back];
node_48 -> node_58 [label = "int", dir = back];
} /* block node_57 */
subgraph "cluster_node_43"
{ /* block node_43 */
label = "";
node_43 [label = "Block [43]"];
node_50 [label = "Proj (mem) [50@43]"];
node_45 -> node_50 [label = "tuple", dir = back];
node_49 [label = "Proj (arg_2) [49@43]"];
node_45 -> node_49 [label = "tuple", dir = back];
node_48 [label = "Proj (arg_1) [48@43]"];
node_45 -> node_48 [label = "tuple", dir = back];
node_45 [label = "Start [45@43]"];
node_51 [label = "Proj (exe(4)) [51@43]"];
node_45 -> node_51 [label = "tuple", dir = back];
} /* block node_43 */
subgraph "cluster_node_52"
{ /* block node_52 */
label = "";
node_52 [label = "Block [52]"];
node_56 [label = "Proj (exe(0)) [56@52]"];
node_54 -> node_56 [label = "tuple", dir = back];
node_53 [label = "Compare [53@52]"];
node_48 -> node_53 [label = "int", dir = back];
node_49 -> node_53 [label = "int", dir = back];
node_54 [label = "Cond (2) [54@52]"];
node_53 -> node_54 [label = "condition", dir = back];
node_55 [label = "Proj (exe(1)) [55@52]"];
node_54 -> node_55 [label = "tuple", dir = back];
} /* block node_52 */
subgraph "cluster_node_60"
{ /* block node_60 */
label = "";
node_60 [label = "Block [60]"];
node_61 [label = "Return [61@60]"];
node_50 -> node_61 [label = "mem", dir = back];
node_49 -> node_61 [label = "int", dir = back];
} /* block node_60 */
subgraph "cluster_node_44"
{ /* block node_44 */
label = "";
node_44 [label = "Block [44]"];
node_46 [label = "End [46@44]"];
} /* block node_44 */
node_56 -> node_60 [label = "exe", dir = back];
node_51 -> node_52 [label = "exe", dir = back];
node_55 -> node_57 [label = "exe", dir = back];
node_58 -> node_44 [label = "exe", dir = back];
node_61 -> node_44 [label = "exe", dir = back];
} /* Graph "If.try_if_then" */
// Difficulty: Easy
// Dot graph language.
// See http://www.rise4fun.com/Agl
return {
// Set defaultToken to invalid to see what you do not tokenize yet
// defaultToken: 'invalid',
keywords: [
'strict','graph','digraph','node','edge','subgraph','rank','abstract',
'n','ne','e','se','s','sw','w','nw','c','_',
'->',':','=',',',
],
builtins: [
'rank','rankdir','ranksep','size','ratio',
'label','headlabel','taillabel',
'arrowhead','samehead','samearrowhead',
'arrowtail','sametail','samearrowtail','arrowsize',
'labeldistance', 'labelangle', 'labelfontsize',
'dir','width','height','angle',
'fontsize','fontcolor', 'same','weight','color',
'bgcolor','style','shape','fillcolor','nodesep','id',
],
attributes: [
'doublecircle','circle','diamond','box','point','ellipse','record',
'inv','invdot','dot','dashed','dotted','filled','back','forward',
],
// we include these common regular expressions
symbols: /[=><!~?:&|+\-*\/\^%]+/,
// The main tokenizer for our languages
tokenizer: {
root: [
// identifiers and keywords
[/[a-zA-Z_\x80-\xFF][\w\x80-\xFF]*/, {
cases: { '@keywords': 'keyword',
'@builtins': 'predefined',
'@attributes': 'constructor',
'@default': 'identifier' } }],
// whitespace
{ include: '@whitespace' },
// html identifiers
[/<(?!@symbols)/, { token: 'string.html.quote', bracket: '@open', next: 'html' } ],
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/@symbols/, { cases: { '@keywords': 'keyword',
'@default' : 'operator' } } ],
// delimiter
[/[;,]/, 'delimiter'],
// numbers
[/\d*\.\d+([eE][\-+]?\d+)?/, 'number.float'],
[/0[xX][0-9a-fA-F]+/, 'number.hex'],
[/\d+/, 'number'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, { token: 'string.quote', bracket: '@open', next: '@string' } ],
],
comment: [
[/[^\/*]+/, 'comment' ],
[/\/\*/, 'comment', '@push' ], // nested comment
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
html: [
[/[^<>&]+/, 'string.html'],
[/&\w+;/, 'string.html.escape' ],
[/&/, 'string.html'],
[/</, { token: 'string.html.quote', bracket: '@open', next: '@push' } ], //nested bracket
[/>/, { token: 'string.html.quote', bracket: '@close', next: '@pop' } ],
],
string: [
[/[^\\"&]+/, 'string'],
[/\\"/, 'string.escape'],
[/&\w+;/, 'string.escape'],
[/[\\&]/, 'string'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
[/#.*$/, 'comment'],
],
},
};
// CSharp 4.0 ray-tracer sample by Luke Hoban
using System.Drawing;
using System.Linq;
using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Windows.Forms;
namespace RayTracer {
public class RayTracer {
private int screenWidth;
private int screenHeight;
private const int MaxDepth = 5;
public Action<int, int, System.Drawing.Color> setPixel;
public RayTracer(int screenWidth, int screenHeight, Action<int,int, System.Drawing.Color> setPixel) {
this.screenWidth = screenWidth;
this.screenHeight = screenHeight;
this.setPixel = setPixel;
}
private IEnumerable<ISect> Intersections(Ray ray, Scene scene)
{
return scene.Things
.Select(obj => obj.Intersect(ray))
.Where(inter => inter != null)
.OrderBy(inter => inter.Dist);
}
private double TestRay(Ray ray, Scene scene) {
var isects = Intersections(ray, scene);
ISect isect = isects.FirstOrDefault();
if (isect == null)
return 0;
return isect.Dist;
}
private Color TraceRay(Ray ray, Scene scene, int depth) {
var isects = Intersections(ray, scene);
ISect isect = isects.FirstOrDefault();
if (isect == null)
return Color.Background;
return Shade(isect, scene, depth);
}
private Color GetNaturalColor(SceneObject thing, Vector pos, Vector norm, Vector rd, Scene scene) {
Color ret = Color.Make(0, 0, 0);
foreach (Light light in scene.Lights) {
Vector ldis = Vector.Minus(light.Pos, pos);
Vector livec = Vector.Norm(ldis);
double neatIsect = TestRay(new Ray() { Start = pos, Dir = livec }, scene);
bool isInShadow = !((neatIsect > Vector.Mag(ldis)) || (neatIsect == 0));
if (!isInShadow) {
double illum = Vector.Dot(livec, norm);
Color lcolor = illum > 0 ? Color.Times(illum, light.Color) : Color.Make(0, 0, 0);
double specular = Vector.Dot(livec, Vector.Norm(rd));
Color scolor = specular > 0 ? Color.Times(Math.Pow(specular, thing.Surface.Roughness), light.Color) : Color.Make(0, 0, 0);
ret = Color.Plus(ret, Color.Plus(Color.Times(thing.Surface.Diffuse(pos), lcolor),
Color.Times(thing.Surface.Specular(pos), scolor)));
}
}
return ret;
}
private Color GetReflectionColor(SceneObject thing, Vector pos, Vector norm, Vector rd, Scene scene, int depth) {
return Color.Times(thing.Surface.Reflect(pos), TraceRay(new Ray() { Start = pos, Dir = rd }, scene, depth + 1));
}
private Color Shade(ISect isect, Scene scene, int depth) {
var d = isect.Ray.Dir;
var pos = Vector.Plus(Vector.Times(isect.Dist, isect.Ray.Dir), isect.Ray.Start);
var normal = isect.Thing.Normal(pos);
var reflectDir = Vector.Minus(d, Vector.Times(2 * Vector.Dot(normal, d), normal));
Color ret = Color.DefaultColor;
ret = Color.Plus(ret, GetNaturalColor(isect.Thing, pos, normal, reflectDir, scene));
if (depth >= MaxDepth) {
return Color.Plus(ret, Color.Make(.5, .5, .5));
}
return Color.Plus(ret, GetReflectionColor(isect.Thing, Vector.Plus(pos, Vector.Times(.001, reflectDir)), normal, reflectDir, scene, depth));
}
private double RecenterX(double x) {
return (x - (screenWidth / 2.0)) / (2.0 * screenWidth);
}
private double RecenterY(double y) {
return -(y - (screenHeight / 2.0)) / (2.0 * screenHeight);
}
private Vector GetPoint(double x, double y, Camera camera) {
return Vector.Norm(Vector.Plus(camera.Forward, Vector.Plus(Vector.Times(RecenterX(x), camera.Right),
Vector.Times(RecenterY(y), camera.Up))));
}
internal void Render(Scene scene) {
for (int y = 0; y < screenHeight; y++)
{
for (int x = 0; x < screenWidth; x++)
{
Color color = TraceRay(new Ray() { Start = scene.Camera.Pos, Dir = GetPoint(x, y, scene.Camera) }, scene, 0);
setPixel(x, y, color.ToDrawingColor());
}
}
}
internal readonly Scene DefaultScene =
new Scene() {
Things = new SceneObject[] {
new Plane() {
Norm = Vector.Make(0,1,0),
Offset = 0,
Surface = Surfaces.CheckerBoard
},
new Sphere() {
Center = Vector.Make(0,1,0),
Radius = 1,
Surface = Surfaces.Shiny
},
new Sphere() {
Center = Vector.Make(-1,.5,1.5),
Radius = .5,
Surface = Surfaces.Shiny
}},
Lights = new Light[] {
new Light() {
Pos = Vector.Make(-2,2.5,0),
Color = Color.Make(.49,.07,.07)
},
new Light() {
Pos = Vector.Make(1.5,2.5,1.5),
Color = Color.Make(.07,.07,.49)
},
new Light() {
Pos = Vector.Make(1.5,2.5,-1.5),
Color = Color.Make(.07,.49,.071)
},
new Light() {
Pos = Vector.Make(0,3.5,0),
Color = Color.Make(.21,.21,.35)
}},
Camera = Camera.Create(Vector.Make(3,2,4), Vector.Make(-1,.5,0))
};
}
static class Surfaces {
// Only works with X-Z plane.
public static readonly Surface CheckerBoard =
new Surface() {
Diffuse = pos => ((Math.Floor(pos.Z) + Math.Floor(pos.X)) % 2 != 0)
? Color.Make(1,1,1)
: Color.Make(0,0,0),
Specular = pos => Color.Make(1,1,1),
Reflect = pos => ((Math.Floor(pos.Z) + Math.Floor(pos.X)) % 2 != 0)
? .1
: .7,
Roughness = 150
};
public static readonly Surface Shiny =
new Surface() {
Diffuse = pos => Color.Make(1,1,1),
Specular = pos => Color.Make(.5,.5,.5),
Reflect = pos => .6,
Roughness = 50
};
}
class Vector {
public double X;
public double Y;
public double Z;
public Vector(double x, double y, double z) { X = x; Y = y; Z = z; }
public Vector(string str) {
string[] nums = str.Split(',');
if (nums.Length != 3) throw new ArgumentException();
X = double.Parse(nums[0]);
Y = double.Parse(nums[1]);
Z = double.Parse(nums[2]);
}
public static Vector Make(double x, double y, double z) { return new Vector(x, y, z); }
public static Vector Times(double n, Vector v) {
return new Vector(v.X * n, v.Y * n, v.Z * n);
}
public static Vector Minus(Vector v1, Vector v2) {
return new Vector(v1.X - v2.X, v1.Y - v2.Y, v1.Z - v2.Z);
}
public static Vector Plus(Vector v1, Vector v2) {
return new Vector(v1.X + v2.X, v1.Y + v2.Y, v1.Z + v2.Z);
}
public static double Dot(Vector v1, Vector v2) {
return (v1.X * v2.X) + (v1.Y * v2.Y) + (v1.Z * v2.Z);
}
public static double Mag(Vector v) { return Math.Sqrt(Dot(v, v)); }
public static Vector Norm(Vector v) {
double mag = Mag(v);
double div = mag == 0 ? double.PositiveInfinity : 1 / mag;
return Times(div, v);
}
public static Vector Cross(Vector v1, Vector v2) {
return new Vector(((v1.Y * v2.Z) - (v1.Z * v2.Y)),
((v1.Z * v2.X) - (v1.X * v2.Z)),
((v1.X * v2.Y) - (v1.Y * v2.X)));
}
public static bool Equals(Vector v1, Vector v2) {
return (v1.X == v2.X) && (v1.Y == v2.Y) && (v1.Z == v2.Z);
}
}
public class Color {
public double R;
public double G;
public double B;
public Color(double r, double g, double b) { R = r; G = g; B = b; }
public Color(string str) {
string[] nums = str.Split(',');
if (nums.Length != 3) throw new ArgumentException();
R = double.Parse(nums[0]);
G = double.Parse(nums[1]);
B = double.Parse(nums[2]);
}
public static Color Make(double r, double g, double b) { return new Color(r, g, b); }
public static Color Times(double n, Color v) {
return new Color(n * v.R, n * v.G, n * v.B);
}
public static Color Times(Color v1, Color v2) {
return new Color(v1.R * v2.R, v1.G * v2.G,v1.B * v2.B);
}
public static Color Plus(Color v1, Color v2) {
return new Color(v1.R + v2.R, v1.G + v2.G,v1.B + v2.B);
}
public static Color Minus(Color v1, Color v2) {
return new Color(v1.R - v2.R, v1.G - v2.G,v1.B - v2.B);
}
public static readonly Color Background = Make(0, 0, 0);
public static readonly Color DefaultColor = Make(0, 0, 0);
public double Legalize(double d) {
return d > 1 ? 1 : d;
}
internal System.Drawing.Color ToDrawingColor() {
return System.Drawing.Color.FromArgb((int)(Legalize(R) * 255), (int)(Legalize(G) * 255), (int)(Legalize(B) * 255));
}
}
class Ray {
public Vector Start;
public Vector Dir;
}
class ISect {
public SceneObject Thing;
public Ray Ray;
public double Dist;
}
class Surface {
public Func<Vector, Color> Diffuse;
public Func<Vector, Color> Specular;
public Func<Vector, double> Reflect;
public double Roughness;
}
class Camera {
public Vector Pos;
public Vector Forward;
public Vector Up;
public Vector Right;
public static Camera Create(Vector pos, Vector lookAt) {
Vector forward = Vector.Norm(Vector.Minus(lookAt, pos));
Vector down = new Vector(0, -1, 0);
Vector right = Vector.Times(1.5, Vector.Norm(Vector.Cross(forward, down)));
Vector up = Vector.Times(1.5, Vector.Norm(Vector.Cross(forward, right)));
return new Camera() { Pos = pos, Forward = forward, Up = up, Right = right };
}
}
class Light {
public Vector Pos;
public Color Color;
}
abstract class SceneObject {
public Surface Surface;
public abstract ISect Intersect(Ray ray);
public abstract Vector Normal(Vector pos);
}
class Sphere : SceneObject {
public Vector Center;
public double Radius;
public override ISect Intersect(Ray ray) {
Vector eo = Vector.Minus(Center, ray.Start);
double v = Vector.Dot(eo, ray.Dir);
double dist;
if (v < 0) {
dist = 0;
}
else {
double disc = Math.Pow(Radius,2) - (Vector.Dot(eo, eo) - Math.Pow(v,2));
dist = disc < 0 ? 0 : v - Math.Sqrt(disc);
}
if (dist == 0) return null;
return new ISect() {
Thing = this,
Ray = ray,
Dist = dist};
}
public override Vector Normal(Vector pos) {
return Vector.Norm(Vector.Minus(pos, Center));
}
}
class Plane : SceneObject {
public Vector Norm;
public double Offset;
public override ISect Intersect(Ray ray) {
double denom = Vector.Dot(Norm, ray.Dir);
if (denom > 0) return null;
return new ISect() {
Thing = this,
Ray = ray,
Dist = (Vector.Dot(Norm, ray.Start) + Offset) / (-denom)};
}
public override Vector Normal(Vector pos) {
return Norm;
}
}
class Scene {
public SceneObject[] Things;
public Light[] Lights;
public Camera Camera;
public IEnumerable<ISect> Intersect(Ray r) {
return from thing in Things
select thing.Intersect(r);
}
}
public delegate void Action<T,U,V>(T t, U u, V v);
public partial class RayTracerForm : Form
{
Bitmap bitmap;
PictureBox pictureBox;
const int width = 600;
const int height = 600;
public RayTracerForm()
{
bitmap = new Bitmap(width,height);
pictureBox = new PictureBox();
pictureBox.Dock = DockStyle.Fill;
pictureBox.SizeMode = PictureBoxSizeMode.StretchImage;
pictureBox.Image = bitmap;
ClientSize = new System.Drawing.Size(width, height + 24);
Controls.Add(pictureBox);
Text = "Ray Tracer";
Load += RayTracerForm_Load;
Show();
}
private void RayTracerForm_Load(object sender, EventArgs e)
{
this.Show();
RayTracer rayTracer = new RayTracer(width, height, (int x, int y, System.Drawing.Color color) =>
{
bitmap.SetPixel(x, y, color);
if (x == 0) pictureBox.Refresh();
});
rayTracer.Render(rayTracer.DefaultScene);
pictureBox.Invalidate();
}
[STAThread]
static void Main() {
Application.EnableVisualStyles();
Application.Run(new RayTracerForm());
}
}
}
// Difficulty: Moderate
// CSharp language definition
// Takes special care to color types and namespaces nicely.
// (note: this can't be done completely accurately though on a lexical level,
// but we are getting quite close :-) )
//
// Todo: support unicode identifiers
// Todo: special color for documentation comments and attributes
return {
defaultToken: '',
tokenPostfix: '.cs',
brackets: [
{ open: '{', close: '}', token: 'delimiter.curly' },
{ open: '[', close: ']', token: 'delimiter.square' },
{ open: '(', close: ')', token: 'delimiter.parenthesis' },
{ open: '<', close: '>', token: 'delimiter.angle' }
],
keywords: [
'extern', 'alias', 'using', 'bool', 'decimal', 'sbyte', 'byte', 'short',
'ushort', 'int', 'uint', 'long', 'ulong', 'char', 'float', 'double',
'object', 'dynamic', 'string', 'assembly', 'is', 'as', 'ref',
'out', 'this', 'base', 'new', 'typeof', 'void', 'checked', 'unchecked',
'default', 'delegate', 'var', 'const', 'if', 'else', 'switch', 'case',
'while', 'do', 'for', 'foreach', 'in', 'break', 'continue', 'goto',
'return', 'throw', 'try', 'catch', 'finally', 'lock', 'yield', 'from',
'let', 'where', 'join', 'on', 'equals', 'into', 'orderby', 'ascending',
'descending', 'select', 'group', 'by', 'namespace', 'partial', 'class',
'field', 'event', 'method', 'param', 'property', 'public', 'protected',
'internal', 'private', 'abstract', 'sealed', 'static', 'struct', 'readonly',
'volatile', 'virtual', 'override', 'params', 'get', 'set', 'add', 'remove',
'operator', 'true', 'false', 'implicit', 'explicit', 'interface', 'enum',
'null', 'async', 'await', 'fixed', 'sizeof', 'stackalloc', 'unsafe', 'nameof',
'when'
],
namespaceFollows: [
'namespace', 'using',
],
parenFollows: [
'if', 'for', 'while', 'switch', 'foreach', 'using', 'catch', 'when'
],
operators: [
'=', '??', '||', '&&', '|', '^', '&', '==', '!=', '<=', '>=', '<<',
'+', '-', '*', '/', '%', '!', '~', '++', '--', '+=',
'-=', '*=', '/=', '%=', '&=', '|=', '^=', '<<=', '>>=', '>>', '=>'
],
symbols: /[=><!~?:&|+\-*\/\^%]+/,
// escape sequences
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-zA-Z_]\w*/, {
cases: {
'@namespaceFollows': { token: 'keyword.$0', next: '@namespace' },
'@keywords': { token: 'keyword.$0', next: '@qualified' },
'@default': { token: 'identifier', next: '@qualified' }
}
}],
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/}/, {
cases: {
'$S2==interpolatedstring': { token: 'string.quote', next: '@pop' },
'$S2==litinterpstring': { token: 'string.quote', next: '@pop' },
'@default': '@brackets'
}
}],
[/[{}()\[\]]/, '@brackets'],
[/[<>](?!@symbols)/, '@brackets'],
[/@symbols/, {
cases: {
'@operators': 'delimiter',
'@default': ''
}
}],
// numbers
[/[0-9_]*\.[0-9_]+([eE][\-+]?\d+)?[fFdD]?/, 'number.float'],
[/0[xX][0-9a-fA-F_]+/, 'number.hex'],
[/0[bB][01_]+/, 'number.hex'], // binary: use same theme style as hex
[/[0-9_]+/, 'number'],
// delimiter: after number because of .\d floats
[/[;,.]/, 'delimiter'],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid'], // non-teminated string
[/"/, { token: 'string.quote', next: '@string' }],
[/\$\@"/, { token: 'string.quote', next: '@litinterpstring' }],
[/\@"/, { token: 'string.quote', next: '@litstring' }],
[/\$"/, { token: 'string.quote', next: '@interpolatedstring' }],
// characters
[/'[^\\']'/, 'string'],
[/(')(@escapes)(')/, ['string', 'string.escape', 'string']],
[/'/, 'string.invalid']
],
qualified: [
[/[a-zA-Z_][\w]*/, {
cases: {
'@keywords': { token: 'keyword.$0' },
'@default': 'identifier'
}
}],
[/\./, 'delimiter'],
['', '', '@pop'],
],
namespace: [
{ include: '@whitespace' },
[/[A-Z]\w*/, 'namespace'],
[/[\.=]/, 'delimiter'],
['', '', '@pop'],
],
comment: [
[/[^\/*]+/, 'comment'],
// [/\/\*/, 'comment', '@push' ], // no nested comments :-(
['\\*/', 'comment', '@pop'],
[/[\/*]/, 'comment']
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, { token: 'string.quote', next: '@pop' }]
],
litstring: [
[/[^"]+/, 'string'],
[/""/, 'string.escape'],
[/"/, { token: 'string.quote', next: '@pop' }]
],
litinterpstring: [
[/[^"{]+/, 'string'],
[/""/, 'string.escape'],
[/{{/, 'string.escape'],
[/}}/, 'string.escape'],
[/{/, { token: 'string.quote', next: 'root.litinterpstring' }],
[/"/, { token: 'string.quote', next: '@pop' }]
],
interpolatedstring: [
[/[^\\"{]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/{{/, 'string.escape'],
[/}}/, 'string.escape'],
[/{/, { token: 'string.quote', next: 'root.interpolatedstring' }],
[/"/, { token: 'string.quote', next: '@pop' }]
],
whitespace: [
[/^[ \t\v\f]*#((r)|(load))(?=\s)/, 'directive.csx'],
[/^[ \t\v\f]*#\w.*$/, 'namespace.cpp'],
[/[ \t\v\f\r\n]+/, ''],
[/\/\*/, 'comment', '@comment'],
[/\/\/.*$/, 'comment'],
],
},
};
// This example shows a use of a channel. Properties of the messages
// passed along the channel, as well as permissions and channel credits,
// are specified in the channel's "where" clause.
channel NumberStream(x: int) where 2 <= x ==> credit(this);
class Sieve {
method Counter(n: NumberStream, to: int) // sends the plurals along n
requires rd(n.mu) && credit(n,-1) && 0 <= to;
{
var i := 2;
while (i < to)
invariant rd(n.mu);
invariant 2 <= i;
invariant credit(n, -1)
{
send n(i);
i := i + 1;
}
send n(-1);
}
method Filter(prime: int, r: NumberStream, s: NumberStream)
requires 2 <= prime;
requires rd(r.mu) && waitlevel << r.mu;
requires rd(s.mu) && s.mu << r.mu && credit(r) && credit(s, -1);
{
receive x := r;
while (2 <= x)
invariant rd(r.mu) && rd(s.mu) && s << r && waitlevel << r.mu;
invariant 2<= x ==> credit(r);
invariant credit(s, -1);
{
if (x % prime != 0) { // suppress multiples of prime
send s(x);
}
receive x := r;
}
send s(-1);
}
method Start()
{
var ch := new NumberStream;
fork Counter(ch, 101);
var p: int;
receive p := ch;
while (2 <= p)
invariant ch != null;
invariant 2 <= p ==> credit(ch, 1);
invariant rd*(ch.mu) && waitlevel << ch.mu;
{
// print p--it's a prime!
var cp := new ChalicePrint; call cp.Int(p);
var n := new NumberStream between waitlevel and ch;
fork Filter(p, ch, n);
ch := n;
receive p := ch;
}
}
}
external class ChalicePrint {
method Int(x: int) { }
}
// Difficulty: "Easy"
// Language definition sample for the Chalice language.
// See 'http://rise4fun.com/Chalice'.
return {
keywords: [
'class','ghost','var','const','method','channel','condition',
'assert','assume','new','this','reorder',
'between','and','above','below','share','unshare','acquire','release','downgrade',
'call','if','else','while','lockchange',
'returns','where',
'false','true','null',
'waitlevel','lockbottom',
'module','external',
'predicate','function',
'forall','exists',
'nil','result','eval','token',
'unlimited',
'refines','transforms','replaces','by','spec',
],
builtins: [
'lock','fork','join','rd','acc','credit','holds','old','assigned',
'send','receive',
'ite','fold','unfold','unfolding','in',
'wait','signal',
],
verifyKeywords: [
'requires','ensures','free','invariant'
],
types: [
'bool','int','string','seq'
],
brackets: [
['{','}','delimiter.curly'],
['[',']','delimiter.square'],
['(',')','delimiter.parenthesis']
],
// Chalice 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',
'@builtins': 'keyword',
'@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' ]
],
}
};
// This example shows many of the features of Spec#, including pre-
// and postcondition of methods and object invariants. The basic
// idea in the example is to implement a "chunker", which returns
// successive portions of a given string. The main work is done
// in the NextChunk() method.
// For a full demo showing this example, check out the "The Chunker"
// episode on Verification Corner
// (http://research.microsoft.com/verificationcorner)
public class Chunker
{
string src;
int ChunkSize;
invariant 0 <= ChunkSize;
int n; // the number of characters returned so far
invariant 0 <= n;
public string NextChunk()
ensures result.Length <= ChunkSize;
{
string s;
if (n + ChunkSize <= src.Length) {
s = src.Substring(n, ChunkSize);
} else {
s = src.Substring(n);
}
return s;
}
public Chunker(string source, int chunkSize)
{
src = source;
ChunkSize = chunkSize;
n = 0;
}
}
// Difficulty: Moderate
// SpecSharp language definition. This is an extension of the C# language definition.
// See: http://rise4fun.com/SpecSharp for more information
//
// Takes special care to color types and namespaces nicely.
// (note: this can't be done completely accurately though on a lexical level,
// but we are getting quite close :-) )
//
// Todo: support unicode identifiers
// Todo: special color for documentation comments and attributes
return {
keywords: [
'extern', 'alias', 'using', 'bool', 'decimal', 'sbyte', 'byte', 'short',
'ushort', 'int', 'uint', 'long', 'ulong', 'char', 'float', 'double',
'object', 'dynamic', 'string', 'assembly', 'module', 'is', 'as', 'ref',
'out', 'this', 'base', 'new', 'typeof', 'void', 'checked', 'unchecked',
'default', 'delegate', 'var', 'const', 'if', 'else', 'switch', 'case',
'while', 'do', 'for', 'foreach', 'in', 'break', 'continue', 'goto',
'return', 'throw', 'try', 'catch', 'finally', 'lock', 'yield', 'from',
'let', 'where', 'join', 'on', 'equals', 'into', 'orderby', 'ascending',
'descending', 'select', 'group', 'by', 'namespace', 'partial', 'class',
'field', 'event', 'method', 'param', 'property', 'public', 'protected',
'internal', 'private', 'abstract', 'sealed', 'static', 'struct', 'readonly',
'volatile', 'virtual', 'override', 'params', 'get', 'set', 'add', 'remove',
'operator', 'true', 'false', 'implicit', 'explicit', 'interface', 'enum',
'null',
'=',':',
'expose', 'assert', 'assume',
'additive', 'model', 'throws',
'forall', 'exists', 'unique', 'count', 'max', 'min', 'product', 'sum',
'result'
],
verifyKeywords: [
'requires', 'modifies', 'ensures', 'otherwise', 'satisfies', 'witness', 'invariant',
],
typeKeywords: [
'bool', 'byte', 'char', 'decimal', 'double', 'fixed', 'float',
'int', 'long','object','sbyte','short','string','uint','ulong',
'ushort','void'
],
keywordInType: [
'struct','new','where','class'
],
typeFollows: [
'as', 'class', 'interface', 'struct', 'enum', 'new','where',
':',
],
namespaceFollows: [
'namespace', 'using',
],
operators: [
'??', '||', '&&', '|', '^', '&', '==', '!=', '<=', '>=', '<<',
'+', '-', '*', '/', '%', '!', '~', '++', '--','+=',
'-=', '*=', '/=', '%=', '&=', '|=', '^=', '<<=', '>>=', '>>', '=>'
],
symbols: /[=><!~?:&|+\-*\/\^%]+/,
// escape sequences
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: [
// Try to show type names nicely: for parameters: Type name
[/[A-Z][\w]*(?=[\.\w]*(\s|\/\*!\*\/)+\w)/, 'type.identifier' ],
// Generic types List<int>.
// Unfortunately, colors explicit nested generic method instantiation as Method<List<int>>(x) wrongly
[/([A-Z][\w]*[\.\w]*)(<)(?![^>]+>\s*(?:\(|$))/, ['type.identifier', { token: '@brackets', next: '@type' } ]],
[/([A-Z][\w]*[\.\w]*)(<)/, ['identifier', { token: '@brackets', next: '@type' } ]],
// These take care of 'System.Console.WriteLine'.
// These two rules are not 100% right: if a non-qualified field has an uppercase name
// it colors it as a type.. but you could use this.Field to circumenvent this.
[/[A-Z][\w]*(?=\.[A-Z])/, 'type.identifier' ],
[/[A-Z][\w]*(?=\.[a-z_])/, 'type.identifier', '@qualified' ],
// identifiers and keywords
[/[a-zA-Z_]\w*/, { cases: {'@typeFollows': { token: 'keyword', next: '@type' },
'@namespaceFollows': { token: 'keyword', next: '@namespace' },
'@typeKeywords': { token: 'type.identifier', next: '@qualified' },
'@keywords': { token: 'keyword', next: '@qualified' },
'@verifyKeywords': { token: 'constructor', next: '@qualified' },
'@default': { token: 'identifier', next: '@qualified' } } }],
// whitespace
{ include: '@whitespace' },
// delimiters and operators
[/[{}()\[\]]/, '@brackets'],
[/[<>](?!@symbols)/, '@brackets'],
[/@symbols/, { cases: { '@operators': 'operator',
'@default' : '' } } ],
// literal string
[/@"/, { token: 'string.quote', bracket: '@open', next: '@litstring' } ],
// 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']
],
qualified: [
[/[a-zA-Z_][\w]*/, { cases: { '@typeFollows': { token: 'keyword', next: '@type' },
'@typeKeywords': 'type.identifier',
'@keywords': 'keyword',
'@verifyKeywords': 'constructor',
'@default': 'identifier' } }],
[/\./, 'delimiter'],
['','','@pop'],
],
type: [
{ include: '@whitespace' },
[/[A-Z]\w*/, 'type.identifier'],
// identifiers and keywords
[/[a-zA-Z_]\w*/, { cases: {'@typeKeywords': 'type.identifier',
'@keywordInType': 'keyword',
'@keywords': {token: '@rematch', next: '@popall'},
'@verifyKeywords': {token: '@rematch', next: '@popall'},
'@default': 'type.identifier' } }],
[/[<]/, '@brackets', '@type_nested' ],
[/[>]/, '@brackets', '@pop' ],
[/[\.,:]/, { cases: { '@keywords': 'keyword',
'@verifyKeywords': 'constructor',
'@default': 'delimiter' }}],
['','','@popall'], // catch all
],
type_nested: [
[/[<]/, '@brackets', '@type_nested' ],
{ include: 'type' }
],
namespace: [
{ include: '@whitespace' },
[/[A-Z]\w*/, 'namespace'],
[/[\.=]/, 'keyword'],
['','','@pop'],
],
comment: [
[/[^\/*]+/, 'comment' ],
// [/\/\*/, 'comment', '@push' ], // no nested comments :-(
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
string: [
[/[^\\"]+/, 'string'],
[/@escapes/, 'string.escape'],
[/\\./, 'string.escape.invalid'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
litstring: [
[/[^"]+/, 'string'],
[/""/, 'string.escape'],
[/"/, { token: 'string.quote', bracket: '@close', next: '@pop' } ]
],
whitespace: [
[/^[ \t\v\f]*#\w.*$/, 'namespace.cpp' ],
[/[ \t\v\f\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
],
},
};
// The partition step of Quick Sort picks a 'pivot' element from a specified subsection
// of a given integer array. It then partially sorts the elements of the array so that
// elements smaller than the pivot end up to the left of the pivot and elements larger
// than the pivot end up to the right of the pivot. Finally, the index of the pivot is
// returned.
// The procedure below always picks the first element of the subregion as the pivot.
// The specification of the procedure talks about the ordering of the elements, but
// does not say anything about keeping the multiset of elements the same.
var A: [int]int;
const N: int;
procedure Partition(l: int, r: int) returns (result: int)
requires 0 <= l && l+2 <= r && r <= N;
modifies A;
ensures l <= result && result < r;
ensures (forall k: int, j: int :: l <= k && k < result && result <= j && j < r ==> A[k] <= A[j]);
ensures (forall k: int :: l <= k && k < result ==> A[k] <= old(A)[l]);
ensures (forall k: int :: result <= k && k < r ==> old(A)[l] <= A[k]);
{
var pv, i, j, tmp: int;
pv := A[l];
i := l;
j := r-1;
// swap A[l] and A[j]
tmp := A[l];
A[l] := A[j];
A[j] := tmp;
goto LoopHead;
// The following loop iterates while 'i < j'. In each iteration,
// one of the three alternatives (A, B, or C) is chosen in such
// a way that the assume statements will evaluate to true.
LoopHead:
// The following the assert statements give the loop invariant
assert (forall k: int :: l <= k && k < i ==> A[k] <= pv);
assert (forall k: int :: j <= k && k < r ==> pv <= A[k]);
assert l <= i && i <= j && j < r;
goto A, B, C, exit;
A:
assume i < j;
assume A[i] <= pv;
i := i + 1;
goto LoopHead;
B:
assume i < j;
assume pv <= A[j-1];
j := j - 1;
goto LoopHead;
C:
assume i < j;
assume A[j-1] < pv && pv < A[i];
// swap A[j-1] and A[i]
tmp := A[i];
A[i] := A[j-1];
A[j-1] := tmp;
assert A[i] < pv && pv < A[j-1];
i := i + 1;
j := j - 1;
goto LoopHead;
exit:
assume i == j;
result := i;
}
// Difficulty: "Easy"
// Language definition sample for the Boogie language.
// See 'http://rise4fun.com/Boogie'.
return {
keywords: [
'type','const','function','axiom','var','procedure','implementation',
'returns',
'assert','assume','break','call','then','else','havoc','if','goto','return','while',
'old','forall','exists','lambda','cast',
'false','true'
],
verifyKeywords: [
'where','requires','ensures','modifies','free','invariant',
'unique','extends','complete'
],
types: [
'bool','int'
],
escapes: '\\\\(?:[abfnrtv\\\\""\']|x[0-9A-Fa-f]{1,4}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})',
tokenizer: {
root: [
// identifiers
['bv(0|[1-9]\\d*)', 'type.keyword' ],
[/\\?[a-zA-Z_'\~#\$\^\.\?\\`][\w_'\~#\$\^\.\?\\`]*(\s*:\s*$)?/,
{ cases: {'$1': 'constructor',
'@keywords': 'keyword',
'@verifyKeywords': 'constructor.identifier',
'@types' : 'type.keyword',
'@default' : 'identifier' }}],
[':=','keyword'],
// whitespace
{ include: '@whitespace' },
['[\\{\\}\\(\\)\\[\\]]', '@brackets'],
['[;,]', 'delimiter'],
// literals
['[0-9]+bv[0-9]+', 'number'], // this is perhaps not so much a 'number' as it is a 'bitvector literal'
['[0-9]+', 'number'],
['""$', 'string.invalid'], // recover
['""', 'string', '@string' ],
],
whitespace: [
['[ \\t\\r\\n]+', 'white'],
['/\\*', 'comment', '@comment' ],
['//.*', 'comment']
],
comment: [
['[^/\\*]+', 'comment' ],
['/\\*', 'comment', '@push' ],
['\\*/', 'comment', '@pop' ],
['[/\\*]', 'comment']
],
string: [
['[^\\\\""]+$', 'string.invalid', '@pop'], // recover on end of line
['@escapes$', 'string.escape.invalid', '@pop'], // more recovery
['[^\\\\""]+', 'string'],
['@escapes', 'string.escape'],
['""', 'string', '@pop' ]
]
}
}
/*
This Formula specificatin models a problem in graph theory. It tries to find
a Eulerian walk within a specified graph. The problem is to find a walk through
the graph with the following properties:
- all edges in the graph must be used
- every edge must be used only once
A well known example of this problem is the so called German "Das-ist-das-Haus-vom-Nikolaus"
problem, which is modeled within this file.
*/
domain EulerWay
{
primitive BaseEdge ::= (x:PosInteger, y:PosInteger).
primitive SolutionEdge ::= (pos:PosInteger, x : PosInteger, y : PosInteger).
// Make sure we have used all BaseEdge terms in the solution
usedBaseEdge ::= (x:PosInteger, y:PosInteger).
usedBaseEdge(x,y) :- BaseEdge(x,y), SolutionEdge(_,x,y).
usedBaseEdge(x,y) :- BaseEdge(x,y), SolutionEdge(_,y,x).
unusedBaseEdge := BaseEdge(x,y), fail usedBaseEdge(x,y).
// Make sure our index values are one based and not bigger than the number of base edges
indexTooBig := SolutionEdge(x,_,_), x > count(BaseEdge(_,_)).
// Make sure that no index is used twice
doubleIndex := s1 is SolutionEdge, s2 is SolutionEdge, s1 != s2, s1.pos = s2.pos.
// Exclude edges that don't line up
//wrongSequence := SolutionEdge(x, Edge(_,b)), SolutionEdge(y, Edge(c,_)), y = x + 1, b != c.
wrongSequence := SolutionEdge(pos1,_,y1), SolutionEdge(pos2,x2,_), pos2 = pos1 + 1, y1 != x2.
// Avoid using edges twice
doubleEdge := SolutionEdge(pos1,x,y), SolutionEdge(pos2,x,y), pos1 != pos2.
// Exclude mirrors of already used edges
mirrorEdge := SolutionEdge(_,x,y), SolutionEdge(_,y,x).
conforms := !unusedBaseEdge & !indexTooBig & !doubleIndex & !wrongSequence & !doubleEdge & !mirrorEdge.
}
/*
Nikolaus graph:
5
/ \
3---4
|\ /|
| X |
|/ \|
1---2
*/
partial model nikolaus2 of EulerWay
{
BaseEdge(1,2)
BaseEdge(1,3)
BaseEdge(1,4)
BaseEdge(2,4)
BaseEdge(2,3)
BaseEdge(3,4)
BaseEdge(3,5)
BaseEdge(4,5)
SolutionEdge(1,_,_)
SolutionEdge(2,_,_)
SolutionEdge(3,_,_)
SolutionEdge(4,_,_)
SolutionEdge(5,_,_)
SolutionEdge(6,_,_)
SolutionEdge(7,_,_)
SolutionEdge(8,_,_)
}
// Difficulty: 'Easy'
// Language definition for the Formula language
// More information at: http://rise4fun.com/formula
return {
brackets: [
['{','}','delimiter.curly'],
['[',']','delimiter.square'],
['(',')','delimiter.parenthesis']
],
keywords: [
'domain', 'model', 'transform', 'system',
'includes', 'extends', 'of', 'returns',
'at', 'machine', 'is', 'no',
'new', 'fun', 'inj', 'bij',
'sur', 'any', 'ensures', 'requires',
'some', 'atleast', 'atmost', 'partial',
'initially', 'next', 'property', 'boot',
'primitive'
],
operators: [
':', '::', '..', '::=',
':-', '|', ';', ',',
'=', '!=', '<', '<=',
'>', '>=', '+', '-',
'%', '/', '*'
],
// operators
symbols: /([\.]{2})|([=><!:\|\+\-\*\/%,;]+)/,
// escape sequences
escapes: /\\(?:[abfnrtv\\"']|x[0-9A-Fa-f]{1,4}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})/,
tokenizer: {
root : [
{ include: '@whitespace' },
[ /[a-zA-Z_][\w_]*('*)/, {
cases: {
'@keywords': 'keyword',
'@default': 'identifier'
} } ],
// delimiters
[ /[\{\}\(\)\[\]]/, '@brackets' ],
[ /`/, { token: 'delimiter.quote', next: '@quotation', bracket: "@open" } ],
[ /\./, 'delimiter' ],
// numbers
[ /[\-\+]?\d+\/[\-\+]?\d*[1-9]/, 'string' ],
[ /[\-\+]?\d+(\.\d+)?/, 'string' ],
[ /@symbols/, { cases:{ '@operators': 'keyword',
'@default': 'symbols' } } ],
// strings
[/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
[/"/, 'string', '@string' ],
],
unquote: [
{ 'include' : '@root' },
[ /\$/, 'predefined.identifier', '@pop' ]
],
quotation:
[
[ /[^`\$]/, 'metatag' ],
[ /`/, { token: 'delimiter.quote', bracket: '@close', next: '@pop' } ],
[ /\$/, 'predefined.identifier', '@unquote' ]
],
whitespace: [
[/[ \t\r\n]+/, 'white'],
[/\/\*/, 'comment', '@comment' ],
[/\/\/.*$/, 'comment'],
],
comment: [
[/[^\/*]+/, 'comment' ],
[/\/\*/, 'comment', '@push' ], // nested comments
[/\/\*/, 'comment.invalid' ],
["\\*/", 'comment', '@pop' ],
[/[\/*]/, 'comment' ]
],
string: [
[/[^"]+/, 'string'],
// [/@escapes/, 'string.escape'],
// [/\\./, 'string.escape.invalid'],
[/"/, 'string', '@pop' ]
],
}
};