+
+
// 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 {
+ // Set defaultToken to invalid to see what you do not tokenize yet
+ // defaultToken: 'invalid',
+
+ keywords: [
+ 'abstract', 'continue', 'for', 'new', 'switch', 'assert', 'default',
+ 'goto', 'package', 'synchronized', 'boolean', 'do', 'if', 'private',
+ 'this', 'break', 'double', 'implements', 'protected', 'throw', 'byte',
+ 'else', 'import', 'public', 'throws', 'case', 'enum', 'instanceof', 'return',
+ 'transient', 'catch', 'extends', 'int', 'short', 'try', 'char', 'final',
+ 'interface', 'static', 'void', 'class', 'finally', 'long', 'strictfp',
+ 'volatile', 'const', 'float', 'native', 'super', 'while', 'true', 'false'
+ ],
+
+ typeKeywords: [
+ 'boolean', 'double', 'byte', 'int', 'short', 'char', 'void', 'long', 'float'
+ ],
+
+ operators: [
+ '=', '>', '<', '!', '~', '?', ':',
+ '==', '<=', '>=', '!=', '&&', '||', '++', '--',
+ '+', '-', '*', '/', '&', '|', '^', '%', '<<',
+ '>>', '>>>', '+=', '-=', '*=', '/=', '&=', '|=',
+ '^=', '%=', '<<=', '>>=', '>>>='
+ ],
+
+ // we include these common regular expressions
+ symbols: /[=><!~?:&|+\-*\/\^%]+/,
+ escapes: /\\(?:[abfnrtv\\"']|x[0-9A-Fa-f]{1,4}|u[0-9A-Fa-f]{4}|U[0-9A-Fa-f]{8})/,
+
+ // The main tokenizer for our languages
+ tokenizer: {
+ root: [
+ // identifiers and keywords
+ [/[a-z_$][\w$]*/, { cases: { '@typeKeywords': 'keyword',
+ '@keywords': 'keyword',
+ '@default': 'identifier' } }],
+ [/[A-Z][\w\$]*/, 'type.identifier' ], // to show class names nicely
+
+ // whitespace
+ { include: '@whitespace' },
+
+ // delimiters and operators
+ [/[{}()\[\]]/, '@brackets'],
+ [/[<>](?!@symbols)/, '@brackets'],
+ [/@symbols/, { cases: { '@operators': 'operator',
+ '@default' : '' } } ],
+
+ // @ annotations.
+ // As an example, we emit a debugging log message on these tokens.
+ // Note: message are supressed during the first load -- change some lines to see them.
+ [/@\s*[a-zA-Z_\$][\w\$]*/, { token: 'annotation', log: 'annotation token: $0' }],
+
+ // numbers
+ [/\d*\.\d+([eE][\-+]?\d+)?[fFdD]?/, 'number.float'],
+ [/0[xX][0-9a-fA-F_]*[0-9a-fA-F][Ll]?/, 'number.hex'],
+ [/0[0-7_]*[0-7][Ll]?/, 'number.octal'],
+ [/0[bB][0-1_]*[0-1][Ll]?/, 'number.binary'],
+ [/\d+[lL]?/, 'number'],
+
+ // delimiter: after number because of .\d floats
+ [/[;,.]/, 'delimiter'],
+
+ // strings
+ [/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/"/, 'string', '@string' ],
+
+ // characters
+ [/'[^\\']'/, 'string'],
+ [/(')(@escapes)(')/, ['string','string.escape','string']],
+ [/'/, 'string.invalid']
+ ],
+
+ whitespace: [
+ [/[ \t\r\n]+/, 'white'],
+ [/\/\*/, 'comment', '@comment' ],
+ [/\/\/.*$/, 'comment'],
+ ],
+
+ comment: [
+ [/[^\/*]+/, 'comment' ],
+ // [/\/\*/, 'comment', '@push' ], // nested comment not allowed :-(
+ [/\/\*/, 'comment.invalid' ],
+ ["\\*/", 'comment', '@pop' ],
+ [/[\/*]/, 'comment' ]
+ ],
+
+ string: [
+ [/[^\\"]+/, 'string'],
+ [/@escapes/, 'string.escape'],
+ [/\\./, 'string.escape.invalid'],
+ [/"/, 'string', '@pop' ]
+ ],
+ },
+};
+
+
+
+
+
+
// 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 {
+ tokenPostfix: '.js',
+
+ keywords: [
+ 'boolean', 'break', 'byte', 'case', 'catch', 'char', 'class', 'const', 'continue', 'debugger',
+ 'default', 'delete', 'do', 'double', 'else', 'enum', 'export', 'extends', 'false', 'final',
+ 'finally', 'float', 'for', 'function', 'goto', 'if', 'implements', 'import', 'in',
+ 'instanceof', 'int', 'interface', 'long', 'native', 'new', 'null', 'package', 'private',
+ 'protected', 'public', 'return', 'short', 'static', 'super', 'switch', 'synchronized', 'this',
+ 'throw', 'throws', 'transient', 'true', 'try', 'typeof', 'var', 'void', 'volatile', 'while',
+ 'with'
+ ],
+
+ builtins: [
+ 'define','require','window','document','undefined'
+ ],
+
+ operators: [
+ '=', '>', '<', '!', '~', '?', ':',
+ '==', '<=', '>=', '!=', '&&', '||', '++', '--',
+ '+', '-', '*', '/', '&', '|', '^', '%', '<<',
+ '>>', '>>>', '+=', '-=', '*=', '/=', '&=', '|=',
+ '^=', '%=', '<<=', '>>=', '>>>='
+ ],
+
+ // define our own brackets as '<' and '>' do not match in javascript
+ brackets: [
+ ['(',')','bracket.parenthesis'],
+ ['{','}','bracket.curly'],
+ ['[',']','bracket.square']
+ ],
+
+ // common regular expressions
+ symbols: /[~!@#%\^&*-+=|\\:`<>.?\/]+/,
+ escapes: /\\(?:[btnfr\\"']|[0-7][0-7]?|[0-3][0-7]{2})/,
+ exponent: /[eE][\-+]?[0-9]+/,
+
+ regexpctl: /[(){}\[\]\$\^|\-*+?\.]/,
+ regexpesc: /\\(?:[bBdDfnrstvwWn0\\\/]|@regexpctl|c[A-Z]|x[0-9a-fA-F]{2}|u[0-9a-fA-F]{4})/,
+
+ tokenizer: {
+ root: [
+ // identifiers and keywords
+ [/([a-zA-Z_\$][\w\$]*)(\s*)(:?)/, {
+ cases: { '$1@keywords': ['keyword','white','delimiter'],
+ '$3': ['key.identifier','white','delimiter'], // followed by :
+ '$1@builtins': ['predefined.identifier','white','delimiter'],
+ '@default': ['identifier','white','delimiter'] } }],
+
+ // whitespace
+ { include: '@whitespace' },
+
+ // regular expression: ensure it is terminated before beginning (otherwise it is an opeator)
+ [/\/(?=([^\\\/]|\\.)+\/)/, { token: 'regexp.slash', bracket: '@open', next: '@regexp'}],
+
+ // delimiters and operators
+ [/[{}()\[\]]/, '@brackets'],
+ [/[;,.]/, 'delimiter'],
+ [/@symbols/, { cases: {'@operators': 'operator',
+ '@default': '' }}],
+
+ // numbers
+ [/\d+\.\d*(@exponent)?/, 'number.float'],
+ [/\.\d+(@exponent)?/, 'number.float'],
+ [/\d+@exponent/, 'number.float'],
+ [/0[xX][\da-fA-F]+/, 'number.hex'],
+ [/0[0-7]+/, 'number.octal'],
+ [/\d+/, 'number'],
+
+ // strings: recover on non-terminated strings
+ [/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/'([^'\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/"/, 'string', '@string."' ],
+ [/'/, 'string', '@string.\'' ],
+ ],
+
+ whitespace: [
+ [/[ \t\r\n]+/, 'white'],
+ [/\/\*/, 'comment', '@comment' ],
+ [/\/\/.*$/, 'comment'],
+ ],
+
+ comment: [
+ [/[^\/*]+/, 'comment' ],
+ // [/\/\*/, 'comment', '@push' ], // nested comment not allowed :-(
+ [/\/\*/, 'comment.invalid' ],
+ ["\\*/", 'comment', '@pop' ],
+ [/[\/*]/, 'comment' ]
+ ],
+
+ string: [
+ [/[^\\"']+/, 'string'],
+ [/@escapes/, 'string.escape'],
+ [/\\./, 'string.escape.invalid'],
+ [/["']/, { cases: { '$#==$S2' : { token: 'string', next: '@pop' },
+ '@default': 'string' }} ]
+ ],
+
+ // We match regular expression quite precisely
+ regexp: [
+ [/(\{)(\d+(?:,\d*)?)(\})/, ['@brackets.regexp.escape.control', 'regexp.escape.control', '@brackets.regexp.escape.control'] ],
+ [/(\[)(\^?)(?=(?:[^\]\\\/]|\\.)+)/, ['@brackets.regexp.escape.control',{ token: 'regexp.escape.control', next: '@regexrange'}]],
+ [/(\()(\?:|\?=|\?!)/, ['@brackets.regexp.escape.control','regexp.escape.control'] ],
+ [/[()]/, '@brackets.regexp.escape.control'],
+ [/@regexpctl/, 'regexp.escape.control'],
+ [/[^\\\/]/, 'regexp' ],
+ [/@regexpesc/, 'regexp.escape' ],
+ [/\\\./, 'regexp.invalid' ],
+ ['/', { token: 'regexp.slash', bracket: '@close'}, '@pop' ],
+ ],
+
+ regexrange: [
+ [/-/, 'regexp.escape.control'],
+ [/\^/, 'regexp.invalid'],
+ [/@regexpesc/, 'regexp.escape'],
+ [/[^\]]/, 'regexp'],
+ [/\]/, '@brackets.regexp.escape.control', '@pop'],
+ ],
+ },
+};
+
+
+
+
+
+// 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) 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 {
+ ignoreCase: true,
+
+ // escape codes for javascript/CSS strings
+ escapes: /\\(?:[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: [
+ [/[^<&]+/,''],
+ { include: '@whitespace' },
+ [/<!DOCTYPE/, 'metatag', '@doctype' ],
+ [/<(\w+)\/>/, 'tag.tag-$1' ],
+ [/<(\w+)/, {cases: { '@empty': { token: 'tag.tag-$1', next: '@tag.$1' },
+ '@default': { token: 'tag.tag-$1', bracket: '@open', next: '@tag.$1' } }}],
+ [/<\/(\w+)\s*>/, { token: 'tag.tag-$1', bracket: '@close' } ],
+ [/&\w+;/, 'string.escape'],
+ ],
+
+ doctype: [
+ [/[^>]+/, 'metatag.content' ],
+ [/>/, 'metatag', '@pop' ]
+ ],
+
+ // tag mode is used to scan inside a tag
+ // tag.<name>.<type> where name is the tag name (i.e. 'div')
+ // and where 'type' is the value of the 'type' attribute
+ // (used to see what language to embed in a script tag)
+ tag: [
+ [/[ \t\r\n]+/, 'white' ],
+ [/(type)(\s*=\s*)(")([^"]+)(")/, [ 'attribute.name', 'delimiter', 'attribute.value',
+ {token: 'attribute.value', switchTo: '@tag.$S2.$4' },
+ 'attribute.value'] ],
+ [/(type)(\s*=\s*)(')([^']+)(')/, [ 'attribute.name', 'delimiter', 'attribute.value',
+ {token: 'attribute.value', switchTo: '@tag.$S2.$4' },
+ 'attribute.value'] ],
+ [/(\w+)(\s*=\s*)("[^"]*"|'[^']*')/, ['attribute.name','delimiter','attribute.value']],
+ [/\w+/, 'attribute.name' ],
+ [/\/>/, 'tag.tag-$S2', '@pop'],
+ [/>/, { cases: { '$S2==style' : { token: 'tag.tag-$S2', switchTo: '@embedded.$S2', nextEmbedded: 'text/css'},
+ '$S2==script': { cases: { '$S3' : { token: 'tag.tag-$S2', switchTo: '@embedded.$S2', nextEmbedded: '$S3' },
+ '@default': { token: 'tag.tag-$S2', switchTo: '@embedded.$S2', nextEmbedded: 'mjavascript' } } },
+ '@default' : { token: 'tag.tag-$S2', next: '@pop' } } }],
+ ],
+
+ // Scan embedded code in a script/style tag
+ // embedded.<endtag>
+ embedded: [
+ [/[^"'<]+/, ''],
+ [/<\/(\w+)\s*>/, { cases: { '$1==$S2' : { token: '@rematch', next: '@pop', nextEmbedded: '@pop' },
+ '@default': '' } }],
+ [/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/'([^'\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/"/, 'string', '@string."' ],
+ [/'/, 'string', '@string.\'' ],
+ [/</, '']
+ ],
+
+ // scan embedded strings in javascript or css
+ // string.<delimiter>
+ string: [
+ [/[^\\"']+/, 'string'],
+ [/@escapes/, 'string.escape'],
+ [/\\./, 'string.escape.invalid'],
+ [/["']/, { cases: { '$#==$S2' : { token: 'string', next: '@pop' },
+ '@default': 'string' }} ]
+ ],
+
+
+ whitespace: [
+ [/[ \t\r\n]+/, 'white'],
+ [/<!--/, 'comment', '@comment']
+ ],
+
+ comment: [
+ [/[^<\-]+/, 'comment.content' ],
+ [/-->/, 'comment', '@pop' ],
+ [/<!--/, 'comment.content.invalid'],
+ [/[<\-]/, 'comment.content' ]
+ ],
+ },
+};
+
+
+
+
# 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
+
+* * * *
+****
+--------------------------
+
+
+
+## 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 {
+ // 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
+ [/^(\s*)(#+)((?:[^\\#]|@escapes)+)((?:#+)?)/, ['white','keyword.$1','keyword.$1','keyword.$1']],
+ [/^\s*(=+|\-+)\s*$/, 'keyword.header'],
+ [/^\s*((\*[ ]?)+)\s*$/, 'keyword.header'],
+
+ // code & quote
+ [/^\s*>+/, 'string.quote' ],
+ [/^(\t|[ ]{4}).*$/, 'namespace.code'], // code line
+ [/^\s*~+\s*$/, { token: 'namespace.code', bracket: '@open', next: '@codeblock' }],
+
+ // github style code blocks
+ [/^\s*````\s*(\w+)\s*$/, { token: 'namespace.code', bracket: '@open', next: '@codeblockgh', nextEmbedded: 'text/x-$1' }],
+ [/^\s*````\s*((?:\w|[\/\-])+)\s*$/, { token: 'namespace.code', bracket: '@open', next: '@codeblockgh', nextEmbedded: '$1' }],
+
+ // list
+ [/^\s*([\*\-+:]|\d\.)/, 'string.list'],
+
+ // markup within lines
+ { include: '@linecontent' },
+ ],
+
+ codeblock: [
+ [/^\s*~+\s*$/, { token: 'namespace.code', bracket: '@close', next: '@pop' }],
+ [/.*$/, 'namespace.code' ],
+ ],
+
+ // github style code blocks
+ codeblockgh: [
+ [/````\s*$/, { token: '@rematch', bracket: '@close', switchTo: '@codeblockghend', nextEmbedded: '@pop' }],
+ [/[^`]*$/, 'namespace.code' ],
+ ],
+
+ codeblockghend: [
+ [/\s*````/, { token: 'namespace.code', bracket: '@close', next: '@pop' } ],
+ [/./, '@rematch', '@pop'],
+ ],
+
+ linecontent: [
+ // [/\s(?=<(\w+)[^>]*>)/, {token: 'html', next: 'html.$1', nextEmbedded: 'text/html' } ],
+ // [/<(\w+)[^>]*>/, {token: '@rematch', next: 'html.$1', nextEmbedded: 'text/html' } ],
+
+ // escapes
+ [/&\w+;/, 'string.escape'],
+ [/@escapes/, 'escape' ],
+
+ // various markup
+ [/\b__([^\\_]|@escapes|_(?!_))+__\b/, 'strong'],
+ [/\*\*([^\\*]|@escapes|\*(?!\*))+\*\*/, 'strong'],
+ [/\b_[^_]+_\b/, 'emphasis'],
+ [/\*([^\\*]|@escapes)+\*/, 'emphasis'],
+ [/`([^\\`]|@escapes)+`/, 'namespace.code'],
+
+ // links
+ [/\{[^}]+\}/, 'string.target'],
+ [/(!?\[)((?:[^\]\\]|@escapes)+)(\]\([^\)]+\))/, ['string.link', '', 'string.link' ]],
+ [/(!?\[)((?:[^\]\\]|@escapes)+)(\])/, 'string.link'],
+
+ // or html
+ { include: 'html' },
+ ],
+
+ html: [
+ // html tags
+ [/<(\w+)\/>/, 'tag.tag-$1' ],
+ [/<(\w+)/, {cases: { '@empty': { token: 'tag.tag-$1', next: '@tag.$1' },
+ '@default': { token: 'tag.tag-$1', bracket: '@open', next: '@tag.$1' } }}],
+ [/<\/(\w+)\s*>/, { token: 'tag.tag-$1', bracket: '@close', next: '@pop' } ],
+
+ // whitespace
+ { include: '@whitespace' },
+ ],
+
+
+ // whitespace and (html style) comments
+ whitespace: [
+ [/[ ]{2}$/, 'invalid'],
+ [/[ \t\r\n]+/, 'white'],
+ [/<!--/, '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', 'delimiter', 'attribute.value',
+ {token: 'attribute.value', switchTo: '@tag.$S2.$4' },
+ 'attribute.value'] ],
+ [/(type)(\s*=\s*)(')([^']+)(')/, [ 'attribute.name', 'delimiter', 'attribute.value',
+ {token: 'attribute.value', switchTo: '@tag.$S2.$4' },
+ 'attribute.value'] ],
+ [/(\w+)(\s*=\s*)("[^"]*"|'[^']*')/, ['attribute.name','delimiter','attribute.value']],
+ [/\w+/, 'attribute.name' ],
+ [/\/>/, 'tag.tag-$S2', '@pop'],
+ [/>/, { cases: { '$S2==style' : { token: 'tag.tag-$S2', switchTo: '@embedded.$S2', nextEmbedded: 'text/css'},
+ '$S2==script': { cases: { '$S3' : { token: 'tag.tag-$S2', switchTo: '@embedded.$S2', nextEmbedded: '$S3' },
+ '@default': { token: 'tag.tag-$S2', switchTo: '@embedded.$S2', nextEmbedded: 'mjavascript' } } },
+ '@default' : { token: 'tag.tag-$S2', switchTo: 'html' } } }],
+ ],
+
+ embedded: [
+ [/[^"'<]+/, ''],
+ [/<\/(\w+)\s*>/, { cases: { '$1==$S2' : { token: '@rematch', switchTo: '@html', nextEmbedded: '@pop' },
+ '@default': '' } }],
+ [/"([^"\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/'([^'\\]|\\.)*$/, 'string.invalid' ], // non-teminated string
+ [/"/, 'string', '@string."' ],
+ [/'/, 'string', '@string.\'' ],
+ [/</, '']
+ ],
+
+ // scan embedded strings in javascript or css
+ string: [
+ [/[^\\"']+/, 'string'],
+ [/@jsescapes/, 'string.escape'],
+ [/\\./, 'string.escape.invalid'],
+ [/["']/, { cases: { '$#==$S2' : { token: 'string', next: '@pop' },
+ '@default': 'string' }} ]
+ ],
+
+ },
+};
+
+
+
#
+# 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 {
+ 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'
+ ],
+
+ // 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: [
+ ['(',')','delimiter.parenthesis'],
+ ['{','}','delimiter.curly'],
+ ['[',']','delimiter.square']
+ ],
+
+ // trigger outdenting on 'end'
+ outdentTriggers: 'd',
+
+ // 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|[1-9]@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', bracket: '@open', next: '@dodecl.$2' },
+ '@declarations': { token: 'keyword.$2', bracket: '@open', next: '@root.$2' },
+ 'end': { token: 'keyword.$S2', bracket: '@close', next: '@pop' },
+ '@keywords': 'keyword',
+ '@builtins': 'predefined',
+ '@default': 'identifier' } }]],
+ [/[a-z_]\w*[!?=]?/,
+ { cases: { 'if|unless|while|until': { token: 'keyword.$0x', bracket: '@open', next: '@modifier.$0x' },
+ 'for': { token: 'keyword.$2', bracket: '@open', next: '@dodecl.$2' },
+ '@linedecls': { token: 'keyword.$0', bracket: '@open', next: '@root.$0' },
+ 'end': { token: 'keyword.$S2', bracket: '@close', 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
+
+ // whitespace
+ { include: '@whitespace' },
+
+ // strings
+ [/"/, { token: 'string.d.delim', bracket: '@open', next: '@dstring.d."'} ],
+ [/'/, { token: 'string.sq.delim', bracket: '@open', next: '@sstring.sq' } ],
+
+ // % literals. For efficiency, rematch in the 'pstring' state
+ [/%([rsqxwW]|Q?)/, { token: '@rematch', next: 'pstring' } ],
+
+ // here documents
+ [/\-?<<(@heredelim).*/, { token: 'string.heredoc.delimiter', bracket: '@open', next: '@heredoc.$1' } ],
+
+ // commands and symbols
+ [/`/, { token: 'string.x.delim', bracket: '@open', next: '@dstring.x.`' } ],
+ [/:(\w|[$@])\w*[!?=]?/, 'string.s'],
+ [/:"/, { token: 'string.s.delim', bracket: '@open', next: '@dstring.s."' } ],
+ [/:'/, { token: 'string.s.delim', bracket: '@open', next: '@sstring.s' } ],
+
+ // regular expressions
+ ['/', { token: 'regexp.delim', bracket: '@open', 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', bracket: '@close', 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', bracket: '@close', 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', bracket: '@close', 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', bracket: '@close', 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', bracket: '@close', 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', bracket: '@open', switchTo: '@interpolated_compound' }],
+ ['', '', '@pop' ], // just a # is interpreted as a #
+ ],
+
+ // any code
+ interpolated_compound: [
+ [/[}]/, { token: 'string.escape.curly', bracket: '@close', 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', bracket: '@close', next: '@pop' },
+ '$#==$S2' : { token: 'regexp.delim', bracket: '@open', 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', bracket: '@close'}, '@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', bracket: '@open', 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', bracket: '@close', 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', bracket: '@open', switchTo: '@qstring.$1.(.)' } ],
+ [/%([qws])\[/, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qstring.$1.[.]' } ],
+ [/%([qws])\{/, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qstring.$1.{.}' } ],
+ [/%([qws])</, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qstring.$1.<.>' } ],
+ [/%([qws])(@delim)/, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qstring.$1.$2.$2' } ],
+
+ [/%r\(/, { token: 'regexp.delim', bracket: '@open', switchTo: '@pregexp.(.)' } ],
+ [/%r\[/, { token: 'regexp.delim', bracket: '@open', switchTo: '@pregexp.[.]' } ],
+ [/%r\{/, { token: 'regexp.delim', bracket: '@open', switchTo: '@pregexp.{.}' } ],
+ [/%r</, { token: 'regexp.delim', bracket: '@open', switchTo: '@pregexp.<.>' } ],
+ [/%r(@delim)/, { token: 'regexp.delim', bracket: '@open', switchTo: '@pregexp.$1.$1' } ],
+
+ [/%(x|W|Q?)\(/, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qqstring.$1.(.)' } ],
+ [/%(x|W|Q?)\[/, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qqstring.$1.[.]' } ],
+ [/%(x|W|Q?)\{/, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qqstring.$1.{.}' } ],
+ [/%(x|W|Q?)</, { token: 'string.$1.delim', bracket: '@open', switchTo: '@qqstring.$1.<.>' } ],
+ [/%(x|W|Q?)(@delim)/, { token: 'string.$1.delim', bracket: '@open', 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', bracket: '@close', next: '@pop' },
+ '$#==$S3' : { token: 'string.$S2.delim', bracket: '@open', 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]+/, 'white'],
+ [/^\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 {
+ // 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: [
+ '+', '-', '*', '**', '/', '//', '%',
+ '<<', '>>', '&', '|', '^', '~',
+ '<', '>', '<=', '>=', '==', '!=', '<>',
+ '+=', '-=', '*=', '/=', '//=', '%=',
+ '&=', '|=', '^=', '>>=', '<<=', '**=',
+ ],
+
+
+ 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',
+ '@default': 'identifier' } }],
+ [/[A-Z][\w]*/, { cases: { '~[A-Z0-9_]+': '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'],
+ ],
+ },
+};
+
+
+
# 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 {
+ 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',
+ '=',':',
+ ],
+
+ 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' },
+ '@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',
+ '@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'},
+ '@default': 'type.identifier' } }],
+ [/[<]/, '@brackets', '@type_nested' ],
+ [/[>]/, '@brackets', '@pop' ],
+ [/[\.,:]/, { cases: { '@keywords': 'keyword',
+ '@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'],
+ ],
+ },
+};
+
+
+
// 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' ]
+ ],
+ }
+};
+
+
+
+
+
+
+
+