mirror of
				https://github.com/KevinMidboe/linguist.git
				synced 2025-10-29 17:50:22 +00:00 
			
		
		
		
	merge master; regen samples
This commit is contained in:
		| @@ -1,6 +1,6 @@ | ||||
| Gem::Specification.new do |s| | ||||
|   s.name    = 'github-linguist' | ||||
|   s.version = '2.10.11' | ||||
|   s.version = '2.10.12' | ||||
|   s.summary = "GitHub Language detection" | ||||
|   s.description = 'We use this library at GitHub to detect blob languages, highlight code, ignore binary files, suppress generated files in diffs, and generate language breakdown graphs.' | ||||
|  | ||||
|   | ||||
| @@ -62,7 +62,8 @@ module Linguist | ||||
|         generated_protocol_buffer? || | ||||
|         generated_jni_header? || | ||||
|         composer_lock? || | ||||
|         node_modules? | ||||
|         node_modules? || | ||||
|         vcr_cassette? | ||||
|     end | ||||
|  | ||||
|     # Internal: Is the blob an XCode project file? | ||||
| @@ -235,5 +236,15 @@ module Linguist | ||||
|     def composer_lock? | ||||
|       !!name.match(/composer.lock/) | ||||
|     end | ||||
|  | ||||
|     # Is the blob a VCR Cassette file? | ||||
|     # | ||||
|     # Returns true or false | ||||
|     def vcr_cassette? | ||||
|       return false unless extname == '.yml' | ||||
|       return false unless lines.count > 2 | ||||
|       # VCR Cassettes have "recorded_with: VCR" in the second last line. | ||||
|       return lines[-2].include?("recorded_with: VCR") | ||||
|     end | ||||
|   end | ||||
| end | ||||
|   | ||||
| @@ -19,6 +19,9 @@ module Linguist | ||||
|         if languages.all? { |l| ["Perl", "Prolog"].include?(l) } | ||||
|           disambiguate_pl(data, languages) | ||||
|         end | ||||
|         if languages.all? { |l| ["ECL", "Prolog"].include?(l) } | ||||
|           disambiguate_ecl(data, languages) | ||||
|         end | ||||
|         if languages.all? { |l| ["TypeScript", "XML"].include?(l) } | ||||
|           disambiguate_ts(data, languages) | ||||
|         end | ||||
| @@ -46,6 +49,13 @@ module Linguist | ||||
|       matches | ||||
|     end | ||||
|  | ||||
|     def self.disambiguate_ecl(data, languages) | ||||
|       matches = [] | ||||
|       matches << Language["Prolog"] if data.include?(":-") | ||||
|       matches << Language["ECL"] if data.include?(":=") | ||||
|       matches | ||||
|     end | ||||
|  | ||||
|     def self.disambiguate_ts(data, languages) | ||||
|       matches = [] | ||||
|       if (data.include?("</translation>")) | ||||
|   | ||||
| @@ -53,6 +53,18 @@ ASP: | ||||
|   - .aspx | ||||
|   - .axd | ||||
|  | ||||
| ATS: | ||||
|   type: programming | ||||
|   color: "#1ac620" | ||||
|   primary_extension: .dats | ||||
|   lexer: OCaml | ||||
|   aliases: | ||||
|   - ats2 | ||||
|   extensions: | ||||
|   - .atxt | ||||
|   - .hats | ||||
|   - .sats | ||||
|  | ||||
| ActionScript: | ||||
|   type: programming | ||||
|   lexer: ActionScript 3 | ||||
| @@ -92,6 +104,8 @@ AppleScript: | ||||
|   primary_extension: .applescript | ||||
|   extensions: | ||||
|   - .scpt | ||||
|   interpreters: | ||||
|   - osascript | ||||
|  | ||||
| Arc: | ||||
|   type: programming | ||||
| @@ -115,6 +129,12 @@ AsciiDoc: | ||||
|   - .adoc | ||||
|   - .asc | ||||
|  | ||||
| AspectJ: | ||||
|   type: programming | ||||
|   lexer: AspectJ | ||||
|   color: "#1957b0" | ||||
|   primary_extension: .aj | ||||
|  | ||||
| Assembly: | ||||
|   type: programming | ||||
|   lexer: NASM | ||||
| @@ -214,6 +234,7 @@ C: | ||||
|   color: "#555" | ||||
|   primary_extension: .c | ||||
|   extensions: | ||||
|   - .cats | ||||
|   - .w | ||||
|  | ||||
| C#: | ||||
| @@ -239,6 +260,7 @@ C++: | ||||
|   extensions: | ||||
|   - .C | ||||
|   - .c++ | ||||
|   - .cc | ||||
|   - .cxx | ||||
|   - .H | ||||
|   - .h++ | ||||
| @@ -284,7 +306,7 @@ COBOL: | ||||
|  | ||||
| CSS: | ||||
|   ace_mode: css | ||||
|   color: "#1f085e" | ||||
|   color: "#563d7c" | ||||
|   primary_extension: .css | ||||
|  | ||||
| Ceylon: | ||||
| @@ -326,6 +348,7 @@ Clojure: | ||||
|   - .cljscm | ||||
|   - .cljx | ||||
|   - .hic | ||||
|   - .cljs.hl | ||||
|   filenames: | ||||
|   - riemann.config | ||||
|  | ||||
| @@ -475,6 +498,9 @@ Dylan: | ||||
|   type: programming | ||||
|   color: "#3ebc27" | ||||
|   primary_extension: .dylan | ||||
|   extensions: | ||||
|   - .intr | ||||
|   - .lid | ||||
|  | ||||
| Ecere Projects: | ||||
|   type: data | ||||
| @@ -540,6 +566,14 @@ F#: | ||||
|   - .fsi | ||||
|   - .fsx | ||||
|  | ||||
| FLUX: | ||||
|   type: programming | ||||
|   color: "#33CCFF" | ||||
|   primary_extension: .fx | ||||
|   lexer: Text only | ||||
|   extensions: | ||||
|   - .flux | ||||
|  | ||||
| FORTRAN: | ||||
|   type: programming | ||||
|   lexer: Fortran | ||||
| @@ -578,7 +612,7 @@ Fancy: | ||||
|   - .fancypack | ||||
|   filenames: | ||||
|   - Fakefile | ||||
|  | ||||
|    | ||||
| Fantom: | ||||
|   type: programming | ||||
|   color: "#dbded5" | ||||
| @@ -684,6 +718,7 @@ HTML: | ||||
|   extensions: | ||||
|   - .htm | ||||
|   - .xhtml | ||||
|   - .html.hl | ||||
|  | ||||
| HTML+Django: | ||||
|   type: markup | ||||
| @@ -832,6 +867,13 @@ JSON5: | ||||
|   lexer: JavaScript | ||||
|   primary_extension: .json5 | ||||
|  | ||||
| JSONLD: | ||||
|   type: data | ||||
|   group: JavaScript | ||||
|   ace_mode: json | ||||
|   lexer: JavaScript | ||||
|   primary_extension: .jsonld | ||||
|  | ||||
| Jade: | ||||
|   group: HTML | ||||
|   type: markup | ||||
| @@ -854,7 +896,7 @@ Java Server Pages: | ||||
| JavaScript: | ||||
|   type: programming | ||||
|   ace_mode: javascript | ||||
|   color: "#f15501" | ||||
|   color: "#f7df1e" | ||||
|   aliases: | ||||
|   - js | ||||
|   - node | ||||
| @@ -874,6 +916,8 @@ JavaScript: | ||||
|   - .ssjs | ||||
|   filenames: | ||||
|   - Jakefile | ||||
|   interpreters: | ||||
|   - node | ||||
|  | ||||
| Julia: | ||||
|   type: programming | ||||
| @@ -1025,6 +1069,13 @@ Mathematica: | ||||
|   primary_extension: .mathematica | ||||
|   lexer: Text only | ||||
|  | ||||
| Mask: | ||||
|   type: markup | ||||
|   lexer: SCSS | ||||
|   color: "#f97732" | ||||
|   ace_mode: scss | ||||
|   primary_extension: .mask | ||||
|  | ||||
| Matlab: | ||||
|   type: programming | ||||
|   color: "#bb92ac" | ||||
| @@ -1328,6 +1379,7 @@ Prolog: | ||||
|   color: "#74283c" | ||||
|   primary_extension: .prolog | ||||
|   extensions: | ||||
|   - .ecl | ||||
|   - .pl | ||||
|  | ||||
| Protocol Buffer: | ||||
| @@ -1392,6 +1444,7 @@ R: | ||||
|   primary_extension: .r | ||||
|   extensions: | ||||
|   - .R | ||||
|   - .rsx | ||||
|   filenames: | ||||
|   - .Rprofile | ||||
|   interpreters: | ||||
| @@ -1505,6 +1558,7 @@ Ruby: | ||||
|   - Appraisals | ||||
|   - Berksfile | ||||
|   - Gemfile | ||||
|   - Gemfile.lock | ||||
|   - Guardfile | ||||
|   - Podfile | ||||
|   - Thorfile | ||||
| @@ -1556,6 +1610,7 @@ Scheme: | ||||
|   color: "#1e4aec" | ||||
|   primary_extension: .scm | ||||
|   extensions: | ||||
|   - .sld | ||||
|   - .sls | ||||
|   - .ss | ||||
|   interpreters: | ||||
| @@ -1594,6 +1649,12 @@ Shell: | ||||
|   filenames: | ||||
|   - Dockerfile | ||||
|  | ||||
| Shen: | ||||
|   type: programming | ||||
|   color: "#120F14" | ||||
|   lexer: Text only | ||||
|   primary_extension: .shen | ||||
|  | ||||
| Slash: | ||||
|   type: programming | ||||
|   color: "#007eff" | ||||
| @@ -1633,6 +1694,15 @@ SuperCollider: | ||||
|   lexer: Text only | ||||
|   primary_extension: .scd | ||||
|  | ||||
| SystemVerilog: | ||||
|   type: programming | ||||
|   color: "#343761" | ||||
|   lexer: systemverilog | ||||
|   primary_extension: .sv | ||||
|   extensions: | ||||
|   - .svh | ||||
|   - .vh | ||||
|  | ||||
| TOML: | ||||
|   type: data | ||||
|   primary_extension: .toml | ||||
| @@ -1810,6 +1880,7 @@ XML: | ||||
|   - .kml | ||||
|   - .launch | ||||
|   - .mxml | ||||
|   - .osm | ||||
|   - .plist | ||||
|   - .pluginspec | ||||
|   - .ps1xml | ||||
|   | ||||
										
											
												File diff suppressed because it is too large
												Load Diff
											
										
									
								
							| @@ -47,6 +47,9 @@ | ||||
| # Debian packaging | ||||
| - ^debian/ | ||||
|  | ||||
| # Haxelib projects often contain a neko bytecode file named run.n | ||||
| - run.n$ | ||||
|  | ||||
| ## Commonly Bundled JavaScript frameworks ## | ||||
|  | ||||
| # jQuery | ||||
| @@ -114,6 +117,13 @@ | ||||
| # Sparkle | ||||
| - (^|/)Sparkle/ | ||||
|  | ||||
| ## Groovy ## | ||||
|  | ||||
| # Gradle | ||||
| - (^|/)gradlew$ | ||||
| - (^|/)gradlew\.bat$ | ||||
| - (^|/)gradle/wrapper/ | ||||
|  | ||||
| ## .NET ## | ||||
|  | ||||
| # Visual Studio IntelliSense | ||||
|   | ||||
							
								
								
									
										110
									
								
								samples/ATS/CoYonedaLemma.dats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										110
									
								
								samples/ATS/CoYonedaLemma.dats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,110 @@ | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2014-01 | ||||
| // CoYoneda Lemma: | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| #include | ||||
| "share/atspre_staload.hats" | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload | ||||
| "libats/ML/SATS/basis.sats" | ||||
| staload | ||||
| "libats/ML/SATS/list0.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload _ = "libats/ML/DATS/list0.dats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| sortdef ftype = type -> type | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| infixr (->) ->> | ||||
| typedef ->> (a:type, b:type) = a -<cloref1> b | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef | ||||
| functor(F:ftype) = | ||||
|   {a,b:type} (a ->> b) ->> F(a) ->> F(b) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef | ||||
| list0 (a:type) = list0 (a) | ||||
| extern | ||||
| val functor_list0 : functor (list0) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| functor_list0{a,b} | ||||
|   (f) = lam xs => list0_map<a><b> (xs, f) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| datatype | ||||
| CoYoneda | ||||
|  (F:ftype, r:type) = {a:type} CoYoneda of (a ->> r, F(a)) | ||||
| // end of [CoYoneda] | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| extern | ||||
| fun CoYoneda_phi | ||||
|   : {F:ftype}functor(F) -> {r:type} (F (r) ->> CoYoneda (F, r)) | ||||
| extern | ||||
| fun CoYoneda_psi | ||||
|   : {F:ftype}functor(F) -> {r:type} (CoYoneda (F, r) ->> F (r)) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| CoYoneda_phi(ftor) = lam (fx) => CoYoneda (lam x => x, fx) | ||||
| implement | ||||
| CoYoneda_psi(ftor) = lam (CoYoneda(f, fx)) => ftor (f) (fx) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| datatype int0 = I of (int) | ||||
| datatype bool = True | False // boxed boolean | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun bool2string | ||||
|   (x:bool): string = | ||||
| ( | ||||
|   case+ x of True() => "True" | False() => "False" | ||||
| ) | ||||
| // | ||||
| implement | ||||
| fprint_val<bool> (out, x) = fprint (out, bool2string(x)) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun int2bool (i: int0): bool = | ||||
|   let val+I(i) = i in if i > 0 then True else False end | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| val myintlist0 = g0ofg1($list{int0}((I)1, (I)0, (I)1, (I)0, (I)0)) | ||||
| val myboolist0 = CoYoneda{list0,bool}{int0}(lam (i) => int2bool(i), myintlist0) | ||||
| val myboolist0 = CoYoneda_psi{list0}(functor_list0){bool}(myboolist0) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| val ((*void*)) = fprintln! (stdout_ref, "myboolist0 = ", myboolist0) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement main0 () = () | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [CoYonedaLemma.dats] *) | ||||
							
								
								
									
										178
									
								
								samples/ATS/DiningPhil2.dats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										178
									
								
								samples/ATS/DiningPhil2.dats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,178 @@ | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2013-11 | ||||
| // | ||||
| // Implementing a variant of | ||||
| // the problem of Dining Philosophers | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| #include | ||||
| "share/atspre_define.hats" | ||||
| #include | ||||
| "share/atspre_staload.hats" | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload | ||||
| UN = "prelude/SATS/unsafe.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "libc/SATS/stdlib.sats" | ||||
| staload "libc/SATS/unistd.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload _ = "libats/DATS/deqarray.dats" | ||||
| staload _ = "{$LIBATSHWXI}/teaching/mythread/DATS/channel.dats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "./DiningPhil2.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement phil_left (n) = n | ||||
| implement phil_right (n) = (n+1) \nmod NPHIL | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| extern | ||||
| fun randsleep (n: intGte(1)): void | ||||
| // | ||||
| implement | ||||
| randsleep (n) = | ||||
|   ignoret (sleep($UN.cast{uInt}(rand() mod n + 1))) | ||||
| // end of [randsleep] | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| phil_think (n) = | ||||
| { | ||||
| val () = println! ("phil_think(", n, ") starts") | ||||
| val () = randsleep (6) | ||||
| val () = println! ("phil_think(", n, ") finishes") | ||||
| } | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| phil_dine (n, lf, rf) = | ||||
| { | ||||
| val () = println! ("phil_dine(", n, ") starts") | ||||
| val () = randsleep (3) | ||||
| val () = println! ("phil_dine(", n, ") finishes") | ||||
| } | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| phil_loop (n) = let | ||||
| // | ||||
| val () = phil_think (n) | ||||
| // | ||||
| val nl = phil_left (n) | ||||
| val nr = phil_right (n) | ||||
| // | ||||
| val ch_lfork = fork_changet (nl) | ||||
| val ch_rfork = fork_changet (nr) | ||||
| // | ||||
| val lf = channel_takeout (ch_lfork) | ||||
| val () = println! ("phil_loop(", n, ") picks left fork") | ||||
| // | ||||
| val () = randsleep (2) // HX: try to actively induce deadlock | ||||
| // | ||||
| val rf = channel_takeout (ch_rfork) | ||||
| val () = println! ("phil_loop(", n, ") picks right fork") | ||||
| // | ||||
| val () = phil_dine (n, lf, rf) | ||||
| // | ||||
| val ch_forktray = forktray_changet () | ||||
| val () = channel_insert (ch_forktray, lf) | ||||
| val () = channel_insert (ch_forktray, rf) | ||||
| // | ||||
| in | ||||
|   phil_loop (n) | ||||
| end // end of [phil_loop] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| cleaner_wash (f) = | ||||
| { | ||||
| val f = fork_get_num (f) | ||||
| val () = println! ("cleaner_wash(", f, ") starts") | ||||
| val () = randsleep (1) | ||||
| val () = println! ("cleaner_wash(", f, ") finishes") | ||||
| } | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| cleaner_return (f) = | ||||
| { | ||||
|   val n = fork_get_num (f) | ||||
|   val ch = fork_changet (n) | ||||
|   val () = channel_insert (ch, f) | ||||
| } | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| cleaner_loop () = let | ||||
| // | ||||
| val ch = forktray_changet () | ||||
| val f0 = channel_takeout (ch) | ||||
| // | ||||
| val () = cleaner_wash (f0) | ||||
| val () = cleaner_return (f0) | ||||
| // | ||||
| in | ||||
|   cleaner_loop () | ||||
| end // end of [cleaner_loop] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| dynload "DiningPhil2.sats" | ||||
| dynload "DiningPhil2_fork.dats" | ||||
| dynload "DiningPhil2_thread.dats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| local | ||||
| // | ||||
| staload | ||||
| "{$LIBATSHWXI}/teaching/mythread/SATS/mythread.sats" | ||||
| // | ||||
| in (* in of [local] *) | ||||
| // | ||||
| val () = mythread_create_cloptr (llam () => phil_loop (0)) | ||||
| val () = mythread_create_cloptr (llam () => phil_loop (1)) | ||||
| val () = mythread_create_cloptr (llam () => phil_loop (2)) | ||||
| val () = mythread_create_cloptr (llam () => phil_loop (3)) | ||||
| val () = mythread_create_cloptr (llam () => phil_loop (4)) | ||||
| // | ||||
| val () = mythread_create_cloptr (llam () => cleaner_loop ()) | ||||
| // | ||||
| end // end of [local] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| main0 () = | ||||
| { | ||||
| // | ||||
| val () = println! ("DiningPhil2: starting") | ||||
| val ((*void*)) = while (true) ignoret (sleep(1)) | ||||
| // | ||||
| } (* end of [main0] *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [DiningPhil2.dats] *) | ||||
							
								
								
									
										71
									
								
								samples/ATS/DiningPhil2.sats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										71
									
								
								samples/ATS/DiningPhil2.sats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,71 @@ | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2013-11 | ||||
| // | ||||
| // Implementing a variant of | ||||
| // the problem of Dining Philosophers | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| #include | ||||
| "share/atspre_define.hats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| %{# | ||||
| #define NPHIL 5 | ||||
| %} // end of [%{#] | ||||
| #define NPHIL 5 | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef nphil = natLt(NPHIL) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun phil_left (n: nphil): nphil | ||||
| fun phil_right (n: nphil): nphil | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun phil_loop (n: nphil): void | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun cleaner_loop ((*void*)): void | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| absvtype fork_vtype = ptr | ||||
| vtypedef fork = fork_vtype | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun fork_get_num (!fork): nphil | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun phil_dine | ||||
|   (n: nphil, lf: !fork, rf: !fork): void | ||||
| // end of [phil_dine] | ||||
|  | ||||
| fun phil_think (n: nphil): void | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun cleaner_wash (f: !fork): void | ||||
| fun cleaner_return (f: fork): void | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun fork_changet (n: nphil): channel(fork) | ||||
| // | ||||
| fun forktray_changet ((*void*)): channel(fork) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [DiningPhil2.sats] *) | ||||
							
								
								
									
										89
									
								
								samples/ATS/DiningPhil2_fork.dats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										89
									
								
								samples/ATS/DiningPhil2_fork.dats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,89 @@ | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2013-11 | ||||
| // | ||||
| // Implementing a variant of | ||||
| // the problem of Dining Philosophers | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| #include | ||||
| "share/atspre_define.hats" | ||||
| #include | ||||
| "share/atspre_staload.hats" | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload | ||||
| UN = "prelude/SATS/unsafe.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload _ = "libats/DATS/deqarray.dats" | ||||
| staload _ = "{$LIBATSHWXI}/teaching/mythread/DATS/channel.dats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "./DiningPhil2.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| datavtype fork = FORK of (nphil) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| assume fork_vtype = fork | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| fork_get_num (f) = let val FORK(n) = f in n end | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| local | ||||
|  | ||||
| val | ||||
| the_forkarray = let | ||||
| // | ||||
| typedef t = channel(fork) | ||||
| // | ||||
| implement | ||||
| array_tabulate$fopr<t> | ||||
|   (n) = ch where | ||||
| { | ||||
|   val n = $UN.cast{nphil}(n) | ||||
|   val ch = channel_create_exn<fork> (i2sz(2)) | ||||
|   val () = channel_insert (ch, FORK (n)) | ||||
| } | ||||
| // | ||||
| in | ||||
|   arrayref_tabulate<t> (i2sz(NPHIL)) | ||||
| end // end of [val] | ||||
|  | ||||
| in (* in of [local] *) | ||||
|  | ||||
| implement fork_changet (n) = the_forkarray[n] | ||||
|  | ||||
| end // end of [local] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| local | ||||
|  | ||||
| val the_forktray = | ||||
|   channel_create_exn<fork> (i2sz(NPHIL+1)) | ||||
|  | ||||
| in (* in of [local] *) | ||||
|  | ||||
| implement forktray_changet () = the_forktray | ||||
|  | ||||
| end // end of [local] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [DiningPhil2_fork.dats] *) | ||||
							
								
								
									
										43
									
								
								samples/ATS/DiningPhil2_thread.dats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										43
									
								
								samples/ATS/DiningPhil2_thread.dats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,43 @@ | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2013-11 | ||||
| // | ||||
| // Implementing a variant of | ||||
| // the problem of Dining Philosophers | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| #include "share/atspre_define.hats" | ||||
| #include "share/atspre_staload.hats" | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "{$LIBATSHWXI}/teaching/mythread/SATS/mythread.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| local | ||||
| // | ||||
| #include "{$LIBATSHWXI}/teaching/mythread/DATS/mythread.dats" | ||||
| // | ||||
| in (* in of [local] *) | ||||
| // | ||||
| // HX: it is intentionally left to be empty | ||||
| // | ||||
| end // end of [local] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| local | ||||
| // | ||||
| #include "{$LIBATSHWXI}/teaching/mythread/DATS/mythread_posix.dats" | ||||
| // | ||||
| in (* in of [local] *) | ||||
| // | ||||
| // HX: it is intentionally left to be empty | ||||
| // | ||||
| end // end of [local] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [DiningPhil2_thread.dats] *) | ||||
							
								
								
									
										178
									
								
								samples/ATS/YonedaLemma.dats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										178
									
								
								samples/ATS/YonedaLemma.dats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,178 @@ | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2014-01 | ||||
| // Yoneda Lemma: | ||||
| // The hardest "trivial" theorem :) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| #include | ||||
| "share/atspre_staload.hats" | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload | ||||
| "libats/ML/SATS/basis.sats" | ||||
| staload | ||||
| "libats/ML/SATS/list0.sats" | ||||
| staload | ||||
| "libats/ML/SATS/option0.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload _ = "libats/ML/DATS/list0.dats" | ||||
| staload _ = "libats/ML/DATS/option0.dats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| sortdef ftype = type -> type | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| infixr (->) ->> | ||||
| typedef ->> (a:type, b:type) = a -<cloref1> b | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef | ||||
| functor(F:ftype) = | ||||
|   {a,b:type} (a ->> b) ->> F(a) ->> F(b) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef | ||||
| list0 (a:type) = list0 (a) | ||||
| extern | ||||
| val functor_list0 : functor (list0) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| functor_list0{a,b} | ||||
|   (f) = lam xs => list0_map<a><b> (xs, f) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef | ||||
| option0 (a:type) = option0 (a)   | ||||
| extern | ||||
| val functor_option0 : functor (option0) | ||||
|    | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| functor_option0{a,b} | ||||
|   (f) = lam opt => option0_map<a><b> (opt, f) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| extern | ||||
| val functor_homres | ||||
|   : {c:type} functor (lam(r:type) => c ->> r) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| functor_homres{c}{a,b} (f) = lam (r) => lam (x) => f (r(x)) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| extern | ||||
| fun Yoneda_phi : {F:ftype}functor(F) -> | ||||
|   {a:type}F(a) ->> ({r:type}(a ->> r) ->> F(r)) | ||||
| extern | ||||
| fun Yoneda_psi : {F:ftype}functor(F) -> | ||||
|   {a:type}({r:type}(a ->> r) ->> F(r)) ->> F(a) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| implement | ||||
| Yoneda_phi | ||||
|   (ftor) = lam(fx) => lam (m) => ftor(m)(fx) | ||||
| // | ||||
| implement | ||||
| Yoneda_psi (ftor) = lam(mf) => mf(lam x => x) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2014-01-05: | ||||
| // Another version based on Natural Transformation | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| typedef | ||||
| natrans(F:ftype, G:ftype) = {x:type} (F(x) ->> G(x)) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| extern | ||||
| fun Yoneda_phi_nat : {F:ftype}functor(F) -> | ||||
|   {a:type} F(a) ->> natrans(lam (r:type) => (a ->> r), F) | ||||
| extern | ||||
| fun Yoneda_psi_nat : {F:ftype}functor(F) -> | ||||
|   {a:type} natrans(lam (r:type) => (a ->> r), F) ->> F(a) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| implement | ||||
| Yoneda_phi_nat | ||||
|   (ftor) = lam(fx) => lam (m) => ftor(m)(fx) | ||||
| // | ||||
| implement | ||||
| Yoneda_psi_nat (ftor) = lam(mf) => mf(lam x => x) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| datatype bool = True | False // boxed boolean | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun bool2string | ||||
|   (x:bool): string = | ||||
| ( | ||||
|   case+ x of True() => "True" | False() => "False" | ||||
| ) | ||||
| // | ||||
| implement | ||||
| fprint_val<bool> (out, x) = fprint (out, bool2string(x)) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| val myboolist0 = | ||||
|   $list_t{bool}(True, False, True, False, False) | ||||
| val myboolist0 = g0ofg1_list (myboolist0) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| extern | ||||
| val Yoneda_bool_list0 : {r:type} (bool ->> r) ->> list0(r) | ||||
| // | ||||
| implement | ||||
| Yoneda_bool_list0 = | ||||
|   Yoneda_phi(functor_list0){bool}(myboolist0) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| val myboolist1 = | ||||
|   Yoneda_psi(functor_list0){bool}(Yoneda_bool_list0) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| val () = fprintln! (stdout_ref, "myboolist0 = ", myboolist0) | ||||
| val () = fprintln! (stdout_ref, "myboolist1 = ", myboolist1) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement main0 () = () | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [YonedaLemma.dats] *) | ||||
							
								
								
									
										187
									
								
								samples/ATS/linset.hats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										187
									
								
								samples/ATS/linset.hats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,187 @@ | ||||
| (***********************************************************************) | ||||
| (*                                                                     *) | ||||
| (*                         Applied Type System                         *) | ||||
| (*                                                                     *) | ||||
| (***********************************************************************) | ||||
|  | ||||
| (* | ||||
| ** ATS/Postiats - Unleashing the Potential of Types! | ||||
| ** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. | ||||
| ** All rights reserved | ||||
| ** | ||||
| ** ATS is free software;  you can  redistribute it and/or modify it under | ||||
| ** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the | ||||
| ** Free Software Foundation; either version 3, or (at  your  option)  any | ||||
| ** later version. | ||||
| **  | ||||
| ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY | ||||
| ** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or | ||||
| ** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License | ||||
| ** for more details. | ||||
| **  | ||||
| ** You  should  have  received  a  copy of the GNU General Public License | ||||
| ** along  with  ATS;  see the  file COPYING.  If not, please write to the | ||||
| ** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA | ||||
| ** 02110-1301, USA. | ||||
| *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* Author: Hongwei Xi *) | ||||
| (* Authoremail: hwxi AT cs DOT bu DOT edu *) | ||||
| (* Start time: December, 2012 *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX: shared by linset_listord (* ordered list *) | ||||
| // HX: shared by linset_avltree (* AVL-tree-based *) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2013-02: | ||||
| // for sets of nonlinear elements | ||||
| // | ||||
| absvtype set_vtype (a:t@ype+) = ptr | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| vtypedef set (a:t0p) = set_vtype (a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| compare_elt_elt (x1: a, x2: a):<> int | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{} linset_nil{a:t0p} ():<> set(a) | ||||
| fun{} linset_make_nil{a:t0p} ():<> set(a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} linset_sing (x: a):<!wrt> set(a) | ||||
| fun{a:t0p} linset_make_sing (x: a):<!wrt> set(a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_make_list (xs: List(INV(a))):<!wrt> set(a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{} | ||||
| linset_is_nil {a:t0p} (xs: !set(INV(a))):<> bool | ||||
| fun{} | ||||
| linset_isnot_nil {a:t0p} (xs: !set(INV(a))):<> bool | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} linset_size (!set(INV(a))): size_t | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_is_member (xs: !set(INV(a)), x0: a):<> bool | ||||
| fun{a:t0p} | ||||
| linset_isnot_member (xs: !set(INV(a)), x0: a):<> bool | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_copy (!set(INV(a))):<!wrt> set(a) | ||||
| fun{a:t0p} | ||||
| linset_free (xs: set(INV(a))):<!wrt> void | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun{a:t0p} | ||||
| linset_insert | ||||
|   (xs: &set(INV(a)) >> _, x0: a):<!wrt> bool | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun{a:t0p} | ||||
| linset_takeout | ||||
| ( | ||||
|   &set(INV(a)) >> _, a, res: &(a?) >> opt(a, b) | ||||
| ) :<!wrt> #[b:bool] bool(b) // endfun | ||||
| fun{a:t0p} | ||||
| linset_takeout_opt (&set(INV(a)) >> _, a):<!wrt> Option_vt(a) | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun{a:t0p} | ||||
| linset_remove | ||||
|   (xs: &set(INV(a)) >> _, x0: a):<!wrt> bool | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX: choosing an element in an unspecified manner | ||||
| // | ||||
| fun{a:t0p} | ||||
| linset_choose | ||||
| ( | ||||
|   xs: !set(INV(a)), x: &a? >> opt (a, b) | ||||
| ) :<!wrt> #[b:bool] bool(b) | ||||
| // | ||||
| fun{a:t0p} | ||||
| linset_choose_opt (xs: !set(INV(a))):<!wrt> Option_vt(a) | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_takeoutmax | ||||
| ( | ||||
|   xs: &set(INV(a)) >> _, res: &a? >> opt(a, b) | ||||
| ) :<!wrt> #[b:bool] bool (b) | ||||
| fun{a:t0p} | ||||
| linset_takeoutmax_opt (xs: &set(INV(a)) >> _):<!wrt> Option_vt(a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_takeoutmin | ||||
| ( | ||||
|   xs: &set(INV(a)) >> _, res: &a? >> opt(a, b) | ||||
| ) :<!wrt> #[b:bool] bool (b) | ||||
| fun{a:t0p} | ||||
| linset_takeoutmin_opt (xs: &set(INV(a)) >> _):<!wrt> Option_vt(a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun{} | ||||
| fprint_linset$sep (FILEref): void // ", " | ||||
| // | ||||
| fun{a:t0p} | ||||
| fprint_linset (out: FILEref, xs: !set(INV(a))): void | ||||
| // | ||||
| overload fprint with fprint_linset | ||||
| // | ||||
| (* ****** ****** *) | ||||
| // | ||||
| fun{ | ||||
| a:t0p}{env:vt0p | ||||
| } linset_foreach$fwork | ||||
|   (x: a, env: &(env) >> _): void | ||||
| // | ||||
| fun{a:t0p} | ||||
| linset_foreach (set: !set(INV(a))): void | ||||
| fun{ | ||||
| a:t0p}{env:vt0p | ||||
| } linset_foreach_env | ||||
|   (set: !set(INV(a)), env: &(env) >> _): void | ||||
| // end of [linset_foreach_env] | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_listize (xs: set(INV(a))): List0_vt (a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| fun{a:t0p} | ||||
| linset_listize1 (xs: !set(INV(a))): List0_vt (a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [linset.hats] *) | ||||
							
								
								
									
										504
									
								
								samples/ATS/linset_listord.dats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										504
									
								
								samples/ATS/linset_listord.dats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,504 @@ | ||||
| (***********************************************************************) | ||||
| (*                                                                     *) | ||||
| (*                         Applied Type System                         *) | ||||
| (*                                                                     *) | ||||
| (***********************************************************************) | ||||
|  | ||||
| (* | ||||
| ** ATS/Postiats - Unleashing the Potential of Types! | ||||
| ** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. | ||||
| ** All rights reserved | ||||
| ** | ||||
| ** ATS is free software;  you can  redistribute it and/or modify it under | ||||
| ** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the | ||||
| ** Free Software Foundation; either version 3, or (at  your  option)  any | ||||
| ** later version. | ||||
| **  | ||||
| ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY | ||||
| ** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or | ||||
| ** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License | ||||
| ** for more details. | ||||
| **  | ||||
| ** You  should  have  received  a  copy of the GNU General Public License | ||||
| ** along  with  ATS;  see the  file COPYING.  If not, please write to the | ||||
| ** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA | ||||
| ** 02110-1301, USA. | ||||
| *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* Author: Hongwei Xi *) | ||||
| (* Authoremail: hwxi AT cs DOT bu DOT edu *) | ||||
| (* Start time: February, 2013 *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX-2013-08: | ||||
| // a set is represented as a sorted list in descending order; | ||||
| // note that descending order is chosen to faciliate set comparison | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload | ||||
| UN = "prelude/SATS/unsafe.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| staload "libats/SATS/linset_listord.sats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| #include "./SHARE/linset.hats" // code reuse | ||||
| #include "./SHARE/linset_node.hats" // code reuse | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| assume | ||||
| set_vtype (elt:t@ype) = List0_vt (elt) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{} | ||||
| linset_nil () = list_vt_nil () | ||||
| implement{} | ||||
| linset_make_nil () = list_vt_nil () | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| linset_sing | ||||
|   (x) = list_vt_cons{a}(x, list_vt_nil) | ||||
| // end of [linset_sing] | ||||
| implement{a} | ||||
| linset_make_sing | ||||
|   (x) = list_vt_cons{a}(x, list_vt_nil) | ||||
| // end of [linset_make_sing] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{} | ||||
| linset_is_nil (xs) = list_vt_is_nil (xs) | ||||
| implement{} | ||||
| linset_isnot_nil (xs) = list_vt_is_cons (xs) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{a} | ||||
| linset_size (xs) = | ||||
|   let val n = list_vt_length(xs) in i2sz(n) end | ||||
| // end of [linset_size] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{a} | ||||
| linset_is_member | ||||
|   (xs, x0) = let | ||||
| // | ||||
| fun aux | ||||
|   {n:nat} .<n>. | ||||
| ( | ||||
|   xs: !list_vt (a, n) | ||||
| ) :<> bool = let | ||||
| in | ||||
| // | ||||
| case+ xs of | ||||
| | list_vt_cons (x, xs) => let | ||||
|     val sgn = compare_elt_elt<a> (x0, x) in | ||||
|     if sgn > 0 then false else (if sgn < 0 then aux (xs) else true) | ||||
|   end // end of [list_vt_cons] | ||||
| | list_vt_nil ((*void*)) => false | ||||
| // | ||||
| end // end of [aux] | ||||
| // | ||||
| in | ||||
|   aux (xs) | ||||
| end // end of [linset_is_member] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{a} | ||||
| linset_copy (xs) = list_vt_copy<a> (xs) | ||||
| implement{a} | ||||
| linset_free (xs) = list_vt_free<a> (xs) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{a} | ||||
| linset_insert | ||||
|   (xs, x0) = let | ||||
| // | ||||
| fun | ||||
| mynode_cons | ||||
|   {n:nat} .<>. | ||||
| ( | ||||
|   nx: mynode1 (a), xs: list_vt (a, n) | ||||
| ) : list_vt (a, n+1) = let | ||||
| // | ||||
| val xs1 = | ||||
| $UN.castvwtp0{List1_vt(a)}(nx) | ||||
| val+@list_vt_cons (_, xs2) = xs1 | ||||
| prval () = $UN.cast2void (xs2); val () = (xs2 := xs) | ||||
| // | ||||
| in | ||||
|   fold@ (xs1); xs1 | ||||
| end // end of [mynode_cons] | ||||
| // | ||||
| fun ins | ||||
|   {n:nat} .<n>. // tail-recursive | ||||
| ( | ||||
|   xs: &list_vt (a, n) >> list_vt (a, n1) | ||||
| ) : #[n1:nat | n <= n1; n1 <= n+1] bool = | ||||
| ( | ||||
| case+ xs of | ||||
| | @list_vt_cons | ||||
|     (x, xs1) => let | ||||
|     val sgn = | ||||
|       compare_elt_elt<a> (x0, x) | ||||
|     // end of [val] | ||||
|   in | ||||
|     if sgn > 0 then let | ||||
|       prval () = fold@ (xs) | ||||
|       val nx = mynode_make_elt<a> (x0) | ||||
|       val ((*void*)) = xs := mynode_cons (nx, xs) | ||||
|     in | ||||
|       false | ||||
|     end else if sgn < 0 then let | ||||
|       val ans = ins (xs1) | ||||
|       prval () = fold@ (xs) | ||||
|     in | ||||
|       ans | ||||
|     end else let // [x0] is found | ||||
|       prval () = fold@ (xs) | ||||
|     in | ||||
|       true (* [x0] in [xs] *) | ||||
|     end (* end of [if] *) | ||||
|   end // end of [list_vt_cons] | ||||
| | list_vt_nil () => let | ||||
|     val nx = mynode_make_elt<a> (x0) | ||||
|     val ((*void*)) = xs := mynode_cons (nx, xs) | ||||
|   in | ||||
|     false | ||||
|   end // end of [list_vt_nil] | ||||
| ) (* end of [ins] *) | ||||
| // | ||||
| in | ||||
|   $effmask_all (ins (xs)) | ||||
| end // end of [linset_insert] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* | ||||
| // | ||||
| HX-2013-08: | ||||
| [linset_remove] moved up | ||||
| // | ||||
| implement{a} | ||||
| linset_remove | ||||
|   (xs, x0) = let | ||||
| // | ||||
| fun rem | ||||
|   {n:nat} .<n>. // tail-recursive | ||||
| ( | ||||
|   xs: &list_vt (a, n) >> list_vt (a, n1) | ||||
| ) : #[n1:nat | n1 <= n; n <= n1+1] bool = | ||||
| ( | ||||
| case+ xs of | ||||
| | @list_vt_cons | ||||
|     (x, xs1) => let | ||||
|     val sgn = | ||||
|       compare_elt_elt<a> (x0, x) | ||||
|     // end of [val] | ||||
|   in | ||||
|     if sgn > 0 then let | ||||
|       prval () = fold@ (xs) | ||||
|     in | ||||
|       false | ||||
|     end else if sgn < 0 then let | ||||
|       val ans = rem (xs1) | ||||
|       prval () = fold@ (xs) | ||||
|     in | ||||
|       ans | ||||
|     end else let // x0 = x | ||||
|       val xs1_ = xs1 | ||||
|       val ((*void*)) = free@{a}{0}(xs) | ||||
|       val () = xs := xs1_ | ||||
|     in | ||||
|       true // [x0] in [xs] | ||||
|     end (* end of [if] *) | ||||
|   end // end of [list_vt_cons] | ||||
| | list_vt_nil () => false | ||||
| ) (* end of [rem] *) | ||||
| // | ||||
| in | ||||
|   $effmask_all (rem (xs)) | ||||
| end // end of [linset_remove] | ||||
| *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| (* | ||||
| ** By Brandon Barker | ||||
| *) | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| linset_choose | ||||
|   (xs, x0) = let | ||||
| in | ||||
| // | ||||
| case+ xs of | ||||
| | list_vt_cons | ||||
|     (x, xs1) => let | ||||
|     val () = x0 := x | ||||
|     prval () = opt_some{a}(x0) | ||||
|   in | ||||
|     true | ||||
|   end // end of [list_vt_cons] | ||||
| | list_vt_nil () => let | ||||
|     prval () = opt_none{a}(x0) | ||||
|   in | ||||
|     false | ||||
|   end // end of [list_vt_nil] | ||||
| // | ||||
| end // end of [linset_choose] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}{env} | ||||
| linset_foreach_env (xs, env) = let | ||||
| // | ||||
| implement | ||||
| list_vt_foreach$fwork<a><env> | ||||
|   (x, env) = linset_foreach$fwork<a><env> (x, env) | ||||
| // | ||||
| in | ||||
|   list_vt_foreach_env<a><env> (xs, env) | ||||
| end // end of [linset_foreach_env] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{a} | ||||
| linset_listize (xs) = xs | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{a} | ||||
| linset_listize1 (xs) = list_vt_copy (xs) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // HX: functions for processing mynodes | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{ | ||||
| } mynode_null{a} () = | ||||
|   $UN.castvwtp0{mynode(a,null)}(the_null_ptr) | ||||
| // end of [mynode_null] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| mynode_make_elt | ||||
|   (x) = let | ||||
| // | ||||
| val nx = list_vt_cons{a}{0}(x, _ ) | ||||
| // | ||||
| in | ||||
|   $UN.castvwtp0{mynode1(a)}(nx) | ||||
| end // end of [mynode_make_elt] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement{ | ||||
| } mynode_free | ||||
|   {a}(nx) = () where { | ||||
| val nx = | ||||
|   $UN.castvwtp0{List1_vt(a)}(nx) | ||||
| // | ||||
| val+~list_vt_cons (_, nx2) = nx | ||||
| // | ||||
| prval ((*void*)) = $UN.cast2void (nx2) | ||||
| // | ||||
| } (* end of [mynode_free] *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| mynode_get_elt | ||||
|   (nx) = (x) where { | ||||
| // | ||||
| val nx1 = | ||||
|   $UN.castvwtp1{List1_vt(a)}(nx) | ||||
| // | ||||
| val+list_vt_cons (x, _) = nx1 | ||||
| // | ||||
| prval ((*void*)) = $UN.cast2void (nx1) | ||||
| // | ||||
| } (* end of [mynode_get_elt] *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| mynode_set_elt | ||||
|   {l} (nx, x0) = | ||||
| { | ||||
| // | ||||
| val nx1 = | ||||
|   $UN.castvwtp1{List1_vt(a)}(nx) | ||||
| // | ||||
| val+@list_vt_cons (x, _) = nx1 | ||||
| // | ||||
| val () = x := x0 | ||||
| // | ||||
| prval () = fold@ (nx1) | ||||
| prval () = $UN.cast2void (nx1) | ||||
| // | ||||
| prval () = __assert (nx) where | ||||
| { | ||||
|   extern praxi __assert (nx: !mynode(a?, l) >> mynode (a, l)): void | ||||
| } (* end of [prval] *) | ||||
| // | ||||
| } (* end of [mynode_set_elt] *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| mynode_getfree_elt | ||||
|   (nx) = (x) where { | ||||
| // | ||||
| val nx = | ||||
|   $UN.castvwtp0{List1_vt(a)}(nx) | ||||
| // | ||||
| val+~list_vt_cons (x, nx2) = nx | ||||
| // | ||||
| prval ((*void*)) = $UN.cast2void (nx2) | ||||
| // | ||||
| } (* end of [mynode_getfree_elt] *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* | ||||
| fun{a:t0p} | ||||
| linset_takeout_ngc | ||||
|   (set: &set(INV(a)) >> _, x0: a):<!wrt> mynode0 (a) | ||||
| // end of [linset_takeout_ngc] | ||||
| *) | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| linset_takeout_ngc | ||||
|   (set, x0) = let | ||||
| // | ||||
| fun takeout | ||||
| ( | ||||
|   xs: &List0_vt (a) >> _ | ||||
| ) : mynode0(a) = let | ||||
| in | ||||
| // | ||||
| case+ xs of | ||||
| | @list_vt_cons | ||||
|     (x, xs1) => let | ||||
|     prval pf_x = view@x | ||||
|     prval pf_xs1 = view@xs1 | ||||
|     val sgn = | ||||
|       compare_elt_elt<a> (x0, x) | ||||
|     // end of [val] | ||||
|   in | ||||
|     if sgn > 0 then let | ||||
|       prval () = fold@ (xs) | ||||
|     in | ||||
|       mynode_null{a}((*void*)) | ||||
|     end else if sgn < 0 then let | ||||
|       val res = takeout (xs1) | ||||
|       prval ((*void*)) = fold@ (xs) | ||||
|     in | ||||
|       res | ||||
|     end else let // x0 = x | ||||
|       val xs1_ = xs1 | ||||
|       val res = $UN.castvwtp0{mynode1(a)}((pf_x, pf_xs1 | xs)) | ||||
|       val () = xs := xs1_ | ||||
|     in | ||||
|       res // [x0] in [xs] | ||||
|     end (* end of [if] *) | ||||
|   end // end of [list_vt_cons] | ||||
| | list_vt_nil () => mynode_null{a}((*void*)) | ||||
| // | ||||
| end (* end of [takeout] *) | ||||
| // | ||||
| in | ||||
|   $effmask_all (takeout (set)) | ||||
| end // end of [linset_takeout_ngc] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| linset_takeoutmax_ngc | ||||
|   (xs) = let | ||||
| in | ||||
| // | ||||
| case+ xs of | ||||
| | @list_vt_cons | ||||
|     (x, xs1) => let | ||||
|     prval pf_x = view@x | ||||
|     prval pf_xs1 = view@xs1 | ||||
|     val xs_ = xs | ||||
|     val () = xs := xs1 | ||||
|   in | ||||
|     $UN.castvwtp0{mynode1(a)}((pf_x, pf_xs1 | xs_)) | ||||
|   end // end of [list_vt_cons] | ||||
| | @list_vt_nil () => let | ||||
|     prval () = fold@ (xs) | ||||
|   in | ||||
|     mynode_null{a}((*void*)) | ||||
|   end // end of [list_vt_nil] | ||||
| // | ||||
| end // end of [linset_takeoutmax_ngc] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| implement | ||||
| {a}(*tmp*) | ||||
| linset_takeoutmin_ngc | ||||
|   (xs) = let | ||||
| // | ||||
| fun unsnoc | ||||
|   {n:pos} .<n>. | ||||
| ( | ||||
|   xs: &list_vt (a, n) >> list_vt (a, n-1) | ||||
| ) :<!wrt> mynode1 (a) = let | ||||
| // | ||||
| val+@list_vt_cons (x, xs1) = xs | ||||
| // | ||||
| prval pf_x = view@x and pf_xs1 = view@xs1 | ||||
| // | ||||
| in | ||||
| // | ||||
| case+ xs1 of | ||||
| | list_vt_cons _ => | ||||
|     let val res = unsnoc(xs1) in fold@xs; res end | ||||
|   // end of [list_vt_cons] | ||||
| | list_vt_nil () => let | ||||
|     val xs_ = xs | ||||
|     val () = xs := list_vt_nil{a}() | ||||
|   in | ||||
|     $UN.castvwtp0{mynode1(a)}((pf_x, pf_xs1 | xs_)) | ||||
|   end // end of [list_vt_nil] | ||||
| // | ||||
| end // end of [unsnoc] | ||||
| // | ||||
| in | ||||
| // | ||||
| case+ xs of | ||||
| | list_vt_cons _ => unsnoc (xs) | ||||
| | list_vt_nil () => mynode_null{a}((*void*)) | ||||
| // | ||||
| end // end of [linset_takeoutmin_ngc] | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [linset_listord.dats] *) | ||||
							
								
								
									
										51
									
								
								samples/ATS/linset_listord.sats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										51
									
								
								samples/ATS/linset_listord.sats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,51 @@ | ||||
| (***********************************************************************) | ||||
| (*                                                                     *) | ||||
| (*                         Applied Type System                         *) | ||||
| (*                                                                     *) | ||||
| (***********************************************************************) | ||||
|  | ||||
| (* | ||||
| ** ATS/Postiats - Unleashing the Potential of Types! | ||||
| ** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. | ||||
| ** All rights reserved | ||||
| ** | ||||
| ** ATS is free software;  you can  redistribute it and/or modify it under | ||||
| ** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the | ||||
| ** Free Software Foundation; either version 3, or (at  your  option)  any | ||||
| ** later version. | ||||
| **  | ||||
| ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY | ||||
| ** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or | ||||
| ** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License | ||||
| ** for more details. | ||||
| **  | ||||
| ** You  should  have  received  a  copy of the GNU General Public License | ||||
| ** along  with  ATS;  see the  file COPYING.  If not, please write to the | ||||
| ** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA | ||||
| ** 02110-1301, USA. | ||||
| *) | ||||
|  | ||||
| (* ****** ****** *) | ||||
| // | ||||
| // Author: Hongwei Xi | ||||
| // Authoremail: hwxiATcsDOTbuDOTedu | ||||
| // Time: October, 2010 | ||||
| // | ||||
| (* ****** ****** *) | ||||
|  | ||||
| #define ATS_PACKNAME "ATSLIB.libats.linset_listord" | ||||
| #define ATS_STALOADFLAG 0 // no static loading at run-time | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| #include "./SHARE/linset.hats" | ||||
| #include "./SHARE/linset_node.hats" | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| castfn | ||||
| linset2list {a:t0p} (xs: set (INV(a))):<> List0_vt (a) | ||||
|  | ||||
| (* ****** ****** *) | ||||
|  | ||||
| (* end of [linset_listord.sats] *) | ||||
							
								
								
									
										215
									
								
								samples/ATS/main.atxt
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										215
									
								
								samples/ATS/main.atxt
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,215 @@ | ||||
| %{ | ||||
| #include "./../ATEXT/atextfun.hats" | ||||
| %} | ||||
|  | ||||
| <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" | ||||
|    "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"> | ||||
| <html xmlns="http://www.w3.org/1999/xhtml"> | ||||
|  | ||||
| <head> | ||||
| <meta http-equiv="content-type" content="text/html; charset=UTF-8" /> | ||||
| <title>EFFECTIVATS-DiningPhil2</title> | ||||
| #patscode_style() | ||||
| </head> | ||||
|  | ||||
| <body> | ||||
|  | ||||
| <h1> | ||||
| Effective ATS: Dining Philosophers | ||||
| </h1> | ||||
|  | ||||
| In this article, I present an implementation of a slight variant of the | ||||
| famous problem of 5-Dining-Philosophers by Dijkstra that makes simple but | ||||
| convincing use of linear types. | ||||
|  | ||||
| <h2> | ||||
| The Original Problem  | ||||
| </h2> | ||||
|  | ||||
| There are five philosophers sitting around a table and there are also 5 | ||||
| forks placed on the table such that each fork is located between the left | ||||
| hand of a philosopher and the right hand of another philosopher. Each | ||||
| philosopher does the following routine repeatedly: thinking and dining.  In | ||||
| order to dine, a philosopher needs to first acquire two forks: one located | ||||
| on his left-hand side and the other on his right-hand side. After | ||||
| finishing dining, a philosopher puts the two acquired forks onto the table: | ||||
| one on his left-hand side and the other on his right-hand side. | ||||
|  | ||||
| <h2> | ||||
| A Variant of the Original Problem  | ||||
| </h2> | ||||
|  | ||||
| The following twist is added to the original version: | ||||
|  | ||||
| <p> | ||||
|  | ||||
| After a fork is used, it becomes a "dirty" fork and needs to be put in a | ||||
| tray for dirty forks. There is a cleaner who cleans dirty forks and then | ||||
| puts them back on the table. | ||||
|  | ||||
| <h2> | ||||
| Channels for Communication | ||||
| </h2> | ||||
|  | ||||
| A channel is just a shared queue of fixed capacity. The following two | ||||
| functions are for inserting an element into and taking an element out of a | ||||
| given channel: | ||||
|  | ||||
| <pre | ||||
| class="patsyntax"> | ||||
| #pats2xhtml_sats("\ | ||||
| fun{a:vt0p} channel_insert (channel (a), a): void | ||||
| fun{a:vt0p} channel_takeout (chan: channel (a)): (a)  | ||||
| ")</pre> | ||||
|  | ||||
| If [channel_insert] is called on a channel that is full, then the caller is | ||||
| blocked until an element is taken out of the channel.  If [channel_takeout] | ||||
| is called on a channel that is empty, then the caller is blocked until an | ||||
| element is inserted into the channel. | ||||
|  | ||||
| <h2> | ||||
| A Channel for Each Fork | ||||
| </h2> | ||||
|  | ||||
| Forks are resources given a linear type. Each fork is initially stored in a | ||||
| channel, which can be obtained by calling the following function: | ||||
|  | ||||
| <pre | ||||
| class="patsyntax"> | ||||
| #pats2xhtml_sats("\ | ||||
| fun fork_changet (n: nphil): channel(fork) | ||||
| ")</pre> | ||||
|  | ||||
| where the type [nphil] is defined to be [natLt(5)] (for natural numbers | ||||
| less than 5). The channels for storing forks are chosen to be of capacity | ||||
| 2. The reason that channels of capacity 2 are chosen to store at most one | ||||
| element (in each of them) is to guarantee that these channels can never be | ||||
| full (so that there is no attempt made to send signals to awake callers | ||||
| supposedly being blocked due to channels being full). | ||||
|  | ||||
|  | ||||
| <h2> | ||||
| A Channel for the Fork Tray | ||||
| </h2> | ||||
|  | ||||
| A tray for storing "dirty" forks is also a channel, which can be obtained | ||||
| by calling the following function: | ||||
|  | ||||
| <pre | ||||
| class="patsyntax"> | ||||
| #pats2xhtml_sats("\ | ||||
| fun forktray_changet ((*void*)): channel(fork) | ||||
| ")</pre> | ||||
|  | ||||
| The capacity chosen for the channel is 6 (instead of 5) so that it can | ||||
| never become full (as there are only 5 forks in total). | ||||
|  | ||||
| <h2> | ||||
| Philosopher Loop | ||||
| </h2> | ||||
|  | ||||
| Each philosopher is implemented as a loop: | ||||
|  | ||||
| <pre | ||||
| class="patsyntax"> | ||||
| #pats2xhtml_dats('\ | ||||
| implement | ||||
| phil_loop (n) = let | ||||
| // | ||||
| val () = phil_think (n) | ||||
| // | ||||
| val nl = phil_left (n) // = n | ||||
| val nr = phil_right (n) // = (n+1) % 5 | ||||
| // | ||||
| val ch_lfork = fork_changet (nl) | ||||
| val ch_rfork = fork_changet (nr) | ||||
| // | ||||
| val lf = channel_takeout (ch_lfork) | ||||
| val () = println! ("phil_loop(", n, ") picks left fork") | ||||
| // | ||||
| val () = randsleep (2) // sleep up to 2 seconds | ||||
| // | ||||
| val rf = channel_takeout (ch_rfork) | ||||
| val () = println! ("phil_loop(", n, ") picks right fork") | ||||
| // | ||||
| val () = phil_dine (n, lf, rf) | ||||
| // | ||||
| val ch_forktray = forktray_changet () | ||||
| val () = channel_insert (ch_forktray, lf) // left fork to dirty tray | ||||
| val () = channel_insert (ch_forktray, rf) // right fork to dirty tray | ||||
| // | ||||
| in | ||||
|   phil_loop (n) | ||||
| end // end of [phil_loop] | ||||
| ')</pre> | ||||
|  | ||||
| It should be straighforward to follow the code for [phil_loop]. | ||||
|  | ||||
| <h2> | ||||
| Fork Cleaner Loop | ||||
| </h2> | ||||
|  | ||||
| A cleaner is implemented as a loop: | ||||
|  | ||||
| <pre | ||||
| class="patsyntax"> | ||||
| #pats2xhtml_dats('\ | ||||
| implement | ||||
| cleaner_loop () = let | ||||
| // | ||||
| val ch = forktray_changet () | ||||
| val f0 = channel_takeout (ch) // [f0] is dirty | ||||
| // | ||||
| val () = cleaner_wash (f0) // washes dirty [f0] | ||||
| val () = cleaner_return (f0) // puts back cleaned [f0] | ||||
| // | ||||
| in | ||||
|   cleaner_loop () | ||||
| end // end of [cleaner_loop] | ||||
| ')</pre> | ||||
|  | ||||
| The function [cleaner_return] first finds out the number of a given fork | ||||
| and then uses the number to locate the channel for storing the fork. Its | ||||
| actual implementation is given as follows: | ||||
|  | ||||
| <pre | ||||
| class="patsyntax"> | ||||
| #pats2xhtml_dats('\ | ||||
| implement | ||||
| cleaner_return (f) = | ||||
| { | ||||
|   val n = fork_get_num (f) | ||||
|   val ch = fork_changet (n) | ||||
|   val () = channel_insert (ch, f) | ||||
| } | ||||
| ')</pre> | ||||
|  | ||||
| It should now be straighforward to follow the code for [cleaner_loop]. | ||||
|  | ||||
| <h2> | ||||
| Testing | ||||
| </h2> | ||||
|  | ||||
| The entire code of this implementation is stored in the following files: | ||||
|  | ||||
| <pre> | ||||
| DiningPhil2.sats | ||||
| DiningPhil2.dats | ||||
| DiningPhil2_fork.dats | ||||
| DiningPhil2_thread.dats | ||||
| </pre> | ||||
|  | ||||
| There is also a Makefile available for compiling the ATS source code into | ||||
| an excutable for testing. One should be able to encounter a deadlock after | ||||
| running the simulation for a while. | ||||
|  | ||||
| <hr size="2"> | ||||
|  | ||||
| This article is written by <a href="http://www.cs.bu.edu/~hwxi/">Hongwei Xi</a>. | ||||
|  | ||||
| </body> | ||||
| </html> | ||||
|  | ||||
| %{ | ||||
| implement main () = fprint_filsub (stdout_ref, "main_atxt.txt") | ||||
| %} | ||||
							
								
								
									
										41
									
								
								samples/AspectJ/CacheAspect.aj
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										41
									
								
								samples/AspectJ/CacheAspect.aj
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,41 @@ | ||||
| package com.blogspot.miguelinlas3.aspectj.cache; | ||||
|  | ||||
| import java.util.Map; | ||||
| import java.util.WeakHashMap; | ||||
|  | ||||
| import org.aspectj.lang.JoinPoint; | ||||
|  | ||||
| import com.blogspot.miguelinlas3.aspectj.cache.marker.Cachable; | ||||
|  | ||||
| /** | ||||
|  * This simple aspect simulates the behaviour of a very simple cache | ||||
|  *   | ||||
|  * @author migue | ||||
|  * | ||||
|  */ | ||||
| public aspect CacheAspect { | ||||
|  | ||||
| 	public pointcut cache(Cachable cachable): execution(@Cachable * * (..)) && @annotation(cachable); | ||||
| 	 | ||||
| 	Object around(Cachable cachable): cache(cachable){ | ||||
| 	 | ||||
| 		String evaluatedKey = this.evaluateKey(cachable.scriptKey(), thisJoinPoint); | ||||
| 		 | ||||
| 		if(cache.containsKey(evaluatedKey)){ | ||||
| 			System.out.println("Cache hit for key " + evaluatedKey); | ||||
| 			return this.cache.get(evaluatedKey); | ||||
| 		} | ||||
| 		 | ||||
| 		System.out.println("Cache miss for key " + evaluatedKey); | ||||
| 		Object value = proceed(cachable); | ||||
| 		cache.put(evaluatedKey, value); | ||||
| 		return value; | ||||
| 	} | ||||
| 	 | ||||
| 	protected String evaluateKey(String key, JoinPoint joinPoint) { | ||||
| 		// TODO add some smart staff to allow simple scripting in @Cachable annotation | ||||
| 		return key; | ||||
| 	} | ||||
| 	 | ||||
| 	protected Map<String, Object> cache = new WeakHashMap<String, Object>(); | ||||
| } | ||||
							
								
								
									
										50
									
								
								samples/AspectJ/OptimizeRecursionCache.aj
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										50
									
								
								samples/AspectJ/OptimizeRecursionCache.aj
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,50 @@ | ||||
| package aspects.caching; | ||||
|  | ||||
| import java.util.Map; | ||||
|  | ||||
| /** | ||||
|  * Cache aspect for optimize recursive functions. | ||||
|  *  | ||||
|  * @author Migueli | ||||
|  * @date 05/11/2013 | ||||
|  * @version 1.0 | ||||
|  * | ||||
|  */ | ||||
| public abstract aspect OptimizeRecursionCache { | ||||
| 		 | ||||
| 	@SuppressWarnings("rawtypes") | ||||
| 	private Map _cache; | ||||
| 	 | ||||
| 	public OptimizeRecursionCache() { | ||||
| 		_cache = getCache(); | ||||
| 	} | ||||
| 	 | ||||
| 	@SuppressWarnings("rawtypes") | ||||
| 	abstract public Map getCache(); | ||||
| 	 | ||||
| 	abstract public pointcut operation(Object o); | ||||
|  | ||||
| 	pointcut topLevelOperation(Object o): operation(o) && !cflowbelow(operation(Object)); | ||||
|  | ||||
| 	before(Object o) : topLevelOperation(o) { | ||||
| 		System.out.println("Seeking value for " + o); | ||||
| 	} | ||||
|  | ||||
| 	Object around(Object o) : operation(o) { | ||||
| 		Object cachedValue = _cache.get(o); | ||||
| 		if (cachedValue != null) { | ||||
| 			System.out.println("Found cached value for " + o + ": " + cachedValue); | ||||
| 			return cachedValue; | ||||
| 		} | ||||
| 		return proceed(o); | ||||
| 	} | ||||
|  | ||||
| 	@SuppressWarnings("unchecked") | ||||
| 	after(Object o) returning(Object result) : topLevelOperation(o) { | ||||
| 		_cache.put(o, result); | ||||
| 	} | ||||
| 	 | ||||
| 	after(Object o) returning(Object result) : topLevelOperation(o) { | ||||
| 		System.out.println("cache size: " + _cache.size()); | ||||
| 	} | ||||
| } | ||||
							
								
								
									
										56
									
								
								samples/C/dynarray.cats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										56
									
								
								samples/C/dynarray.cats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,56 @@ | ||||
| /* ******************************************************************* */ | ||||
| /*                                                                     */ | ||||
| /*                         Applied Type System                         */ | ||||
| /*                                                                     */ | ||||
| /* ******************************************************************* */ | ||||
|  | ||||
| /* | ||||
| ** ATS/Postiats - Unleashing the Potential of Types! | ||||
| ** Copyright (C) 2011-20?? Hongwei Xi, ATS Trustful Software, Inc. | ||||
| ** All rights reserved | ||||
| ** | ||||
| ** ATS is free software;  you can  redistribute it and/or modify it under | ||||
| ** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the | ||||
| ** Free Software Foundation; either version 3, or (at  your  option)  any | ||||
| ** later version. | ||||
| **  | ||||
| ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY | ||||
| ** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or | ||||
| ** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License | ||||
| ** for more details. | ||||
| **  | ||||
| ** You  should  have  received  a  copy of the GNU General Public License | ||||
| ** along  with  ATS;  see the  file COPYING.  If not, please write to the | ||||
| ** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA | ||||
| ** 02110-1301, USA. | ||||
| */ | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| /* | ||||
| (* Author: Hongwei Xi *) | ||||
| (* Authoremail: hwxi AT cs DOT bu DOT edu *) | ||||
| (* Start time: March, 2013 *) | ||||
| */ | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #ifndef ATSHOME_LIBATS_DYNARRAY_CATS | ||||
| #define ATSHOME_LIBATS_DYNARRAY_CATS | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #include <string.h> | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #define atslib_dynarray_memcpy memcpy | ||||
| #define atslib_dynarray_memmove memmove | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #endif // ifndef ATSHOME_LIBATS_DYNARRAY_CATS | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| /* end of [dynarray.cats] */ | ||||
							
								
								
									
										47
									
								
								samples/C/readline.cats
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										47
									
								
								samples/C/readline.cats
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,47 @@ | ||||
| /* | ||||
| ** API in ATS for GNU-readline | ||||
| */ | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| /* | ||||
| ** Permission to use, copy, modify, and distribute this software for any | ||||
| ** purpose with or without fee is hereby granted, provided that the above | ||||
| ** copyright notice and this permission notice appear in all copies. | ||||
| **  | ||||
| ** THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES | ||||
| ** WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF | ||||
| ** MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR | ||||
| ** ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES | ||||
| ** WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN | ||||
| ** ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF | ||||
| ** OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. | ||||
| */ | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #ifndef READLINE_READLINE_CATS | ||||
| #define READLINE_READLINE_CATS | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #include <readline/readline.h> | ||||
|  | ||||
| /* ****** ****** */ | ||||
| // | ||||
| #define \ | ||||
| atscntrb_readline_rl_library_version() ((char*)rl_library_version) | ||||
| // | ||||
| #define atscntrb_readline_rl_readline_version() (rl_readline_version) | ||||
| // | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #define atscntrb_readline_readline readline | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| #endif // ifndef READLINE_READLINE_CATS | ||||
|  | ||||
| /* ****** ****** */ | ||||
|  | ||||
| /* end of [readline.cats] */ | ||||
							
								
								
									
										30
									
								
								samples/JSONLD/sample.jsonld
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										30
									
								
								samples/JSONLD/sample.jsonld
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,30 @@ | ||||
| { | ||||
|   "@context": { | ||||
|     "property": "http://example.com/vocab#property" | ||||
|   }, | ||||
|   "@id": "../document-relative", | ||||
|   "@type": "#document-relative", | ||||
|   "property": { | ||||
|     "@context": { | ||||
|       "@base": "http://example.org/test/" | ||||
|     }, | ||||
|     "@id": "../document-base-overwritten", | ||||
|     "@type": "#document-base-overwritten", | ||||
|     "property": [ | ||||
|       { | ||||
|         "@context": null, | ||||
|         "@id": "../document-relative", | ||||
|         "@type": "#document-relative", | ||||
|         "property": "context completely reset, drops property" | ||||
|       }, | ||||
|       { | ||||
|         "@context": { | ||||
|           "@base": null | ||||
|         }, | ||||
|         "@id": "../document-relative", | ||||
|         "@type": "#document-relative", | ||||
|         "property": "only @base is cleared" | ||||
|       } | ||||
|     ] | ||||
|   } | ||||
| } | ||||
							
								
								
									
										36
									
								
								samples/M/Comment.m
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										36
									
								
								samples/M/Comment.m
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,36 @@ | ||||
| Comment ; | ||||
|   ; this is a comment block | ||||
|   ; comments always start with a semicolon | ||||
|   ; the next line, while not a comment, is a legal blank line | ||||
|    | ||||
|   ;whitespace alone is a valid line in a routine | ||||
|   ;** Comments can have any graphic character, but no "control" | ||||
|   ;** characters | ||||
|    | ||||
|   ;graphic characters such as: !@#$%^&*()_+=-{}[]|\:"?/>.<, | ||||
|   ;the space character is considered a graphic character, even  | ||||
|   ;though you can't see it. | ||||
|   ; ASCII characters whose numeric code is above 128 and below 32 | ||||
|   ; are NOT allowed on a line in a routine. | ||||
|   ;; multiple semicolons are okay | ||||
|   ; a line that has a tag must have whitespace after the tag, bug | ||||
|   ; does not have to have a comment or a command on it | ||||
| Tag1   | ||||
|   ; | ||||
|   ;Tags can start with % or an uppercase or lowercase alphabetic | ||||
|   ; or can be a series of numeric characters | ||||
| %HELO ; | ||||
|  ; | ||||
| 0123 ; | ||||
|   ; | ||||
| %987  ; | ||||
|   ; the most common label is uppercase alphabetic | ||||
| LABEL ; | ||||
|   ;  | ||||
|   ; Tags can be followed directly by an open parenthesis and a | ||||
|   ; formal list of variables, and a close parenthesis | ||||
| ANOTHER(X) ; | ||||
|   ; | ||||
|   ;Normally, a subroutine would be ended by a QUIT command, but we | ||||
|   ; are taking advantage of the rule that the END of routine is an | ||||
|   ; implicit QUIT | ||||
							
								
								
									
										61
									
								
								samples/Mask/view.mask
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										61
									
								
								samples/Mask/view.mask
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,61 @@ | ||||
|  | ||||
| // HTML Elements | ||||
| header { | ||||
|      | ||||
|     img .logo src='/images/~[currentLogo].png' alt=logo; | ||||
|      | ||||
|     h4 > 'Bar View' | ||||
|      | ||||
|     if (currentUser) { | ||||
|          | ||||
|         .account > | ||||
|             a href='/acount' > | ||||
|                 'Hello, ~[currentUser.username]' | ||||
|     } | ||||
| } | ||||
|  | ||||
| .view { | ||||
|     ul { | ||||
|         | ||||
|         // Iteration | ||||
|         for ((user, index) of users) { | ||||
|              | ||||
|             li.user data-id='~[user.id]' { | ||||
|                  | ||||
|                 // interpolation | ||||
|                 .name > '~[ user.username ]' | ||||
|                  | ||||
|                 // expression | ||||
|                 .count > '~[: user.level.toFixed(2) ]' | ||||
|                  | ||||
|                 // util | ||||
|                 /* Localization sample | ||||
|                  * lastActivity: "Am {0:dd. MM} war der letzte Eintrag" | ||||
|                  */ | ||||
|                 .date > '~[ L: "lastActivity",  user.date]' | ||||
|             } | ||||
|         } | ||||
|     } | ||||
|      | ||||
|     // Component | ||||
|     :countdownComponent { | ||||
|         input type = text > | ||||
|             :dualbind value='number'; | ||||
|              | ||||
|         button x-signal='click: countdownStart' > 'Start'; | ||||
|          | ||||
|         h5 { | ||||
|             '~[bind: number]' | ||||
|              | ||||
|             :animation x-slot='countdownStart' { | ||||
|                 @model > 'transition | scale(0) > scale(1) | 500ms' | ||||
|                 @next  > 'background-color | red > blue | 2s linear' | ||||
|             } | ||||
|         } | ||||
|     } | ||||
| } | ||||
|  | ||||
| footer > :bazCompo { | ||||
|      | ||||
|     'Component generated at ~[: $u.format($c.date, "HH-mm") ]' | ||||
| } | ||||
							
								
								
									
										90
									
								
								samples/Prolog/or-constraint.ecl
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										90
									
								
								samples/Prolog/or-constraint.ecl
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,90 @@ | ||||
| :- lib(ic). | ||||
|  | ||||
| /** | ||||
|  * Question 1.11 | ||||
|  * vabs(?Val, ?AbsVal) | ||||
|  */ | ||||
| vabs(Val, AbsVal):- | ||||
| 	AbsVal #> 0, | ||||
| 	( | ||||
| 		Val #= AbsVal | ||||
| 	; | ||||
| 		Val #= -AbsVal | ||||
| 	), | ||||
| 	labeling([Val, AbsVal]). | ||||
|  | ||||
| /** | ||||
|  * vabsIC(?Val, ?AbsVal) | ||||
|  */ | ||||
| vabsIC(Val, AbsVal):- | ||||
| 	AbsVal #> 0, | ||||
| 	Val #= AbsVal or Val #= -AbsVal, | ||||
| 	labeling([Val, AbsVal]). | ||||
|  | ||||
| /** | ||||
|  * Question 1.12 | ||||
|  */ | ||||
| % X #:: -10..10, vabs(X, Y). | ||||
| % X #:: -10..10, vabsIC(X, Y). | ||||
|  | ||||
| /** | ||||
|  * Question 1.13 | ||||
|  * faitListe(?ListVar, ?Taille, +Min, +Max) | ||||
|  */ | ||||
| faitListe([], 0, _, _):-!. | ||||
| faitListe([First|Rest], Taille, Min, Max):- | ||||
| 	First #:: Min..Max, | ||||
| 	Taille1 #= Taille - 1, | ||||
| 	faitListe(Rest, Taille1, Min, Max). | ||||
|  | ||||
| /** | ||||
|  * Question 1.14 | ||||
|  * suite(?ListVar) | ||||
|  */ | ||||
| suite([Xi, Xi1, Xi2]):- | ||||
| 	checkRelation(Xi, Xi1, Xi2). | ||||
| suite([Xi, Xi1, Xi2|Rest]):- | ||||
| 	checkRelation(Xi, Xi1, Xi2), | ||||
| 	suite([Xi1, Xi2|Rest]). | ||||
|  | ||||
| /** | ||||
|  * checkRelation(?Xi, ?Xi1, ?Xi2) | ||||
|  */ | ||||
| checkRelation(Xi, Xi1, Xi2):- | ||||
| 	vabs(Xi1, VabsXi1), | ||||
| 	Xi2 #= VabsXi1 - Xi. | ||||
|  | ||||
| /** | ||||
|  * Question 1.15 | ||||
|  * checkPeriode(+ListVar). | ||||
|  */ | ||||
| % TODO Any better solution? | ||||
| checkPeriode(ListVar):- | ||||
| 	length(ListVar, Length), | ||||
| 	Length < 10. | ||||
| checkPeriode([X1, X2, X3, X4, X5, X6, X7, X8, X9, X10|Rest]):- | ||||
| 	X1 =:= X10, | ||||
| 	checkPeriode([X2, X3, X4, X5, X6, X7, X8, X9, X10|Rest]). | ||||
| % faitListe(ListVar, 18, -9, 9), suite(ListVar), checkPeriode(ListVar). => 99 solutions | ||||
|  | ||||
|  | ||||
| /** | ||||
|  * Tests | ||||
|  */ | ||||
| /* | ||||
| vabs(5, 5). => Yes | ||||
| vabs(5, -5). => No | ||||
| vabs(-5, 5). => Yes | ||||
| vabs(X, 5). | ||||
| vabs(X, AbsX).  | ||||
| vabsIC(5, 5). => Yes | ||||
| vabsIC(5, -5). => No | ||||
| vabsIC(-5, 5). => Yes | ||||
| vabsIC(X, 5). | ||||
| vabsIC(X, AbsX). | ||||
|  | ||||
| faitListe(ListVar, 5, 1, 3). => 243 solutions | ||||
| faitListe([_, _, _, _, _], Taille, 1, 3). => Taille = 5 !!!!!!!!!!!!!!!! | ||||
|  | ||||
| faitListe(ListVar, 18, -9, 9), suite(ListVar). => 99 solutions | ||||
| */ | ||||
							
								
								
									
										5
									
								
								samples/R/R-qgis-extension.rsx
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										5
									
								
								samples/R/R-qgis-extension.rsx
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,5 @@ | ||||
| ##polyg=vector | ||||
| ##numpoints=number 10 | ||||
| ##output=output vector | ||||
| ##[Example scripts]=group | ||||
| pts=spsample(polyg,numpoints,type="regular") | ||||
							
								
								
									
										7
									
								
								samples/Scheme/basic.sld
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										7
									
								
								samples/Scheme/basic.sld
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,7 @@ | ||||
| (define-library (libs basic) | ||||
|     (export list2 x) | ||||
|     (begin | ||||
|         (define (list2 . objs)  objs) | ||||
|         (define x 'libs-basic) | ||||
|         (define not-exported 'should-not-be-exported) | ||||
|         )) | ||||
							
								
								
									
										321
									
								
								samples/Shen/graph.shen
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										321
									
								
								samples/Shen/graph.shen
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,321 @@ | ||||
| \* graph.shen --- a library for graph definition and manipulation | ||||
|  | ||||
| Copyright (C) 2011,  Eric Schulte | ||||
|  | ||||
| *** License: | ||||
|  | ||||
| Redistribution and use in source and binary forms, with or without | ||||
| modification, are permitted provided that the following conditions are | ||||
| met: | ||||
|  | ||||
|  - Redistributions of source code must retain the above copyright | ||||
|    notice, this list of conditions and the following disclaimer. | ||||
|  | ||||
|  - Redistributions in binary form must reproduce the above copyright | ||||
|    notice, this list of conditions and the following disclaimer in the | ||||
|    documentation and/or other materials provided with the distribution. | ||||
|  | ||||
| THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS | ||||
| "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT | ||||
| LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR | ||||
| A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT | ||||
| HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, | ||||
| SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT | ||||
| LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, | ||||
| DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY | ||||
| THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT | ||||
| (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE | ||||
| OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. | ||||
|  | ||||
| *** Commentary: | ||||
|  | ||||
| Graphs are represented as two dictionaries one for vertices and one | ||||
| for edges.  It is important to note that the dictionary implementation | ||||
| used is able to accept arbitrary data structures as keys.  This | ||||
| structure technically encodes hypergraphs (a generalization of graphs | ||||
| in which each edge may contain any number of vertices).  Examples of a | ||||
| regular graph G and a hypergraph H with the corresponding data | ||||
| structure are given below. | ||||
|  | ||||
|  | ||||
| --G=<graph Vertices Edges>------------------------------------------------ | ||||
|                             Vertices                  Edges | ||||
|                            ----------                ------- | ||||
|  +----Graph G-----+      hash | key -> value      hash |  key  -> value | ||||
|  |                |      -----+------>--------    -----+-------->--------- | ||||
|  | a---b---c   g  |         1 |  a  -> [1]           1 | [a b] -> [1 2] | ||||
|  |     |   |      |         2 |  b  -> [1 2 3]       2 | [b c] -> [2 3] | ||||
|  |     d---e---f  |         3 |  c  -> [2 4]         3 | [b d] -> [2 4] | ||||
|  |                |         4 |  d  -> [3 5]         4 | [c e] -> [3 5] | ||||
|  +----------------+         5 |  e  -> [4 5 6]       5 | [d e] -> [4 5] | ||||
|                             6 |  f  -> [6]           6 | [e f] -> [5 6] | ||||
|                             7 |  g  -> [] | ||||
|  | ||||
|  | ||||
| --H=<graph Vertices Edges>------------------------------------------------ | ||||
|                             Vertices                  Edges | ||||
|                            ----------                ------- | ||||
|                          hash | key -> value      hash |  key  -> value | ||||
|  +-- Hypergraph H----+   -----+------>--------    -----+-------->--------- | ||||
|  |                   |      1 |  a  -> [1]           1 | [a b     [1 2 | ||||
|  |        +------+   |      2 |  b  -> [1]             |  c d  ->  3 4 | ||||
|  | +------+------+   |      3 |  c  -> [1]             |  e f]     5 6] | ||||
|  | |a b c |d e f |   |      4 |  d  -> [1 2]           | | ||||
|  | +------+------+   |      5 |  e  -> [1 2]         2 | [d e     [4 5 | ||||
|  |        |g h i | j |      6 |  f  -> [1 2]           |  f g  ->  6 7 | ||||
|  |        +------+   |      7 |  g  -> [2]             |  h i]     8 9] | ||||
|  |                   |      8 |  h  -> [2] | ||||
|  +-------------------+      9 |  i  -> [2] | ||||
|                            10 |  j  -> [] | ||||
|  | ||||
|  | ||||
| --G=<graph Vertices Edges>-------Graph with associated edge/vertex data--------- | ||||
|                             Vertices                    Edges | ||||
|                            ----------                  ------- | ||||
|  +----Graph G-----+      hash | key -> value        hash |  key  -> value | ||||
|  |   4   6     7  |      -----+------>--------      -----+-------->--------- | ||||
|  |0a---b---c   g  |         1 |  a  -> (@p 0 [1])      1 | [a b] -> (@p 4 [1 2]) | ||||
|  |    1|  3|      |         2 |  b  -> [1 2 3]         2 | [b c] -> (@p 6 [2 3]) | ||||
|  |     d---e---f  |         3 |  c  -> [2 4]           3 | [b d] -> (@p 1 [2 4]) | ||||
|  |       2   5    |         4 |  d  -> [3 5]           4 | [c e] -> (@p 3 [3 5]) | ||||
|  +----------------+         5 |  e  -> [4 5 6]         5 | [d e] -> (@p 2 [4 5]) | ||||
|                             6 |  f  -> [6]             6 | [e f] -> (@p 5 [5 6]) | ||||
|                             7 |  g  -> (@p 7 []) | ||||
|  | ||||
| V = # of vertices | ||||
| E = # of edges | ||||
| M = # of vertex edge associations | ||||
|  | ||||
| size = size of all vertices +            all vertices stored in Vertices dict | ||||
|        M * sizeof(int) * 4 +             indices into Vertices & Edge dicts | ||||
|        V * sizeof(dict entry) +          storage in the Vertex dict | ||||
|        E * sizeof(dict entry) +          storage in the Edge dict | ||||
|        2 * sizeof(dict)                  the Vertices and Edge dicts | ||||
|  | ||||
| *** Code: *\ | ||||
| (require dict) | ||||
| (require sequence) | ||||
|  | ||||
| (datatype graph | ||||
|   Vertices : dictionary; | ||||
|      Edges : dictoinary; | ||||
|   =================== | ||||
|   (vector symbol Vertices Edges);) | ||||
|  | ||||
| (package graph- [graph graph? vertices edges add-vertex | ||||
|                  add-edge has-edge? has-vertex? edges-for | ||||
|                  neighbors connected-to connected? connected-components | ||||
|                  vertex-partition bipartite? | ||||
|                  \* included from the sequence library\ *\ | ||||
|                  take drop take-while drop-while range flatten | ||||
|                  filter complement seperate zip indexed reduce | ||||
|                  mapcon partition partition-with unique frequencies | ||||
|                  shuffle pick remove-first interpose subset? | ||||
|                  cartesian-product | ||||
|                  \* included from the dict library\ *\ | ||||
|                  dict? dict dict-> <-dict contents key? keys vals | ||||
|                  dictionary make-dict] | ||||
|  | ||||
| (define graph? | ||||
|   X -> (= graph (<-address X 0))) | ||||
|  | ||||
| (define make-graph | ||||
|   \* create a graph with specified sizes for the vertex dict and edge dict *\ | ||||
|   {number --> number --> graph} | ||||
|   Vertsize Edgesize -> | ||||
|     (let Graph (absvector 3) | ||||
|       (do (address-> Graph 0 graph) | ||||
|           (address-> Graph 1 (make-dict Vertsize)) | ||||
|           (address-> Graph 2 (make-dict Edgesize)) | ||||
|           Graph))) | ||||
|  | ||||
| (defmacro graph-macro | ||||
|   \* return a graph taking optional sizes for the vertex and edge dicts *\ | ||||
|   [graph] -> [make-graph 1024 1024] | ||||
|   [graph N] -> [make-graph N 1024] | ||||
|   [graph N M] -> [make-graph N M]) | ||||
|  | ||||
| (define vert-dict Graph -> (<-address Graph 1)) | ||||
|  | ||||
| (define edge-dict Graph -> (<-address Graph 2)) | ||||
|  | ||||
| (define vertices | ||||
|   {graph --> (list A)} | ||||
|   Graph -> (keys (vert-dict Graph))) | ||||
|  | ||||
| (define edges | ||||
|   {graph --> (list (list A))} | ||||
|   Graph -> (keys (edge-dict Graph))) | ||||
|  | ||||
| (define get-data | ||||
|   Value V -> (if (tuple? Value) | ||||
|                  (fst Value) | ||||
|                  (error (make-string "no data for ~S~%" V)))) | ||||
|  | ||||
| (define vertex-data | ||||
|   Graph V -> (get-data (<-dict (vert-dict Graph) V) V)) | ||||
|  | ||||
| (define edge-data | ||||
|   Graph V -> (get-data (<-dict (edge-dict Graph) V) V)) | ||||
|  | ||||
| (define resolve | ||||
|   {(vector (list A)) --> (@p number number) --> A} | ||||
|   Vector (@p Index Place) -> (nth (+ 1 Place) (<-vector Vector Index))) | ||||
|  | ||||
| (define resolve-vert | ||||
|   {graph --> (@p number number) --> A} | ||||
|   Graph Place -> (resolve (<-address (vert-dict Graph) 2) Place)) | ||||
|  | ||||
| (define resolve-edge | ||||
|   {graph --> (@p number number) --> A} | ||||
|   Graph Place -> (resolve (<-address (edge-dict Graph) 2) Place)) | ||||
|  | ||||
| (define edges-for | ||||
|   {graph --> A --> (list (list A))} | ||||
|   Graph Vert -> (let Val (trap-error (<-dict (vert-dict Graph) Vert) (/. E [])) | ||||
|                      Edges (if (tuple? Val) (snd Val) Val) | ||||
|                   (map (lambda X (fst (resolve-edge Graph X))) Val))) | ||||
|  | ||||
| (define add-vertex-w-data | ||||
|   \* add a vertex to a graph *\ | ||||
|   {graph --> A --> B --> A} | ||||
|   G V Data -> (do (dict-> (vert-dict G) V (@p Data (edges-for G V))) V)) | ||||
|  | ||||
| (define add-vertex-w/o-data | ||||
|   \* add a vertex to a graph *\ | ||||
|   {graph --> A --> B --> A} | ||||
|   G V -> (do (dict-> (vert-dict G) V (edges-for G V)) V)) | ||||
|  | ||||
| (defmacro add-vertex-macro | ||||
|   [add-vertex G V]   -> [add-vertex-w/o-data G V] | ||||
|   [add-vertex G V D] -> [add-vertex-w-data G V D]) | ||||
|  | ||||
| (define update-vert | ||||
|   \* in a dict, add an edge to a vertex's edge list *\ | ||||
|   {vector --> (@p number number) --> A --> number} | ||||
|   Vs Edge V -> (let Store (<-address Vs 2) | ||||
|                     N (hash V (limit Store)) | ||||
|                     VertLst (trap-error (<-vector Store N) (/. E [])) | ||||
|                     Contents (trap-error (<-dict Vs V) (/. E [])) | ||||
|                  (do (dict-> Vs V (if (tuple? Contents) | ||||
|                                       (@p (fst Contents) | ||||
|                                           (adjoin Edge (snd Contents))) | ||||
|                                       (adjoin Edge Contents))) | ||||
|                      (@p N (length VertLst))))) | ||||
|  | ||||
| (define update-edges-vertices | ||||
|   \* add an edge to a graph *\ | ||||
|   {graph --> (list A) --> (list A)} | ||||
|   Graph Edge -> | ||||
|   (let Store (<-address (edge-dict Graph) 2) | ||||
|        EdgeID (hash Edge (limit Store)) | ||||
|        EdgeLst (trap-error (<-vector Store EdgeID) (/. E [])) | ||||
|     (map (update-vert (vert-dict Graph) (@p EdgeID (length EdgeLst))) Edge))) | ||||
|  | ||||
| (define add-edge-w-data | ||||
|   G E D -> (do (dict-> (edge-dict G) E (@p D (update-edges-vertices G E))) E)) | ||||
|  | ||||
| (define add-edge-w/o-data | ||||
|   G E -> (do (dict-> (edge-dict G) E (update-edges-vertices G E)) E)) | ||||
|  | ||||
| (defmacro add-edge-macro | ||||
|   [add-edge G E]   -> [add-edge-w/o-data G E] | ||||
|   [add-edge G E V] -> [add-edge-w-data G E V]) | ||||
|  | ||||
| (define has-edge? | ||||
|   {graph --> (list A) --> boolean} | ||||
|   Graph Edge -> (key? (edge-dict Graph) Edge)) | ||||
|  | ||||
| (define has-vertex? | ||||
|   {graph --> A --> boolean} | ||||
|   Graph Vertex -> (key? (vert-dict Graph) Vertex)) | ||||
|  | ||||
| (define neighbors | ||||
|   \* Return the neighbors of a vertex *\ | ||||
|   {graph --> A --> (list A)} | ||||
|   Graph Vert -> (unique (mapcon (remove-first Vert) (edges-for Graph Vert)))) | ||||
|  | ||||
| (define connected-to- | ||||
|   {graph --> (list A) --> (list A) --> (list A)} | ||||
|   Graph [] Already -> Already | ||||
|   Graph New Already -> | ||||
|   (let Reachable (unique (mapcon (neighbors Graph) New)) | ||||
|        New (difference Reachable Already) | ||||
|     (connected-to- Graph New (append New Already)))) | ||||
|  | ||||
| (define connected-to | ||||
|   \* return all vertices connected to the given vertex, including itself *\ | ||||
|   {graph --> A --> (list A)} | ||||
|   Graph V -> (connected-to- Graph [V] [V])) | ||||
|  | ||||
| (define connected? | ||||
|   \* return if a graph is fully connected *\ | ||||
|   {graph --> boolean} | ||||
|   Graph -> (reduce (/. V Acc | ||||
|                        (and Acc | ||||
|                             (subset? (vertices Graph) (connected-to Graph V)))) | ||||
|                    true (vertices Graph))) | ||||
|  | ||||
| (define connected-components- | ||||
|   \* given a graph return a list of connected components *\ | ||||
|   {graph --> (list A) --> (list (list A)) --> (list graph)} | ||||
|   Graph [] _ -> [] | ||||
|   Graph VS [] -> (map (/. V (let Component (graph 1 0) | ||||
|                               (do (add-vertex Component V) Component))) | ||||
|                       VS) | ||||
|   Graph [V|VS] ES -> | ||||
|     (let Con-verts (connected-to Graph V) | ||||
|          Con-edges (filter (/. E (subset? E Con-verts)) ES) | ||||
|          Component (graph (length Con-verts) (length Con-edges)) | ||||
|       (do (map (add-edge-w/o-data Component) Con-edges) | ||||
|           (cons Component (connected-components- Graph | ||||
|                                                  (difference VS Con-verts) | ||||
|                                                  (difference ES Con-edges)))))) | ||||
|  | ||||
| (define connected-components | ||||
|   {graph --> (list graph)} | ||||
|   Graph -> (connected-components- Graph (vertices Graph) (edges Graph))) | ||||
|  | ||||
| (define place-vertex | ||||
|   \* given a graph, vertex and list of partitions, partition the vertex *\ | ||||
|   {graph --> A --> (list (list A)) --> (list (list A))} | ||||
|   Graph V [] -> (if (element? V (neighbors Graph V)) | ||||
|                     (simple-error | ||||
|                      (make-string "self-loop ~S, no vertex partition" V)) | ||||
|                     [[V]]) | ||||
|   Graph V [C|CS] -> (let Neighbors (neighbors Graph V) | ||||
|                       (if (element? V Neighbors) | ||||
|                           (simple-error | ||||
|                            (make-string "self-loop ~S, no vertex partition" V)) | ||||
|                           (if (empty? (intersection C Neighbors)) | ||||
|                               [[V|C]|CS] | ||||
|                               [C|(place-vertex Graph V CS)])))) | ||||
|  | ||||
| (define vertex-partition | ||||
|   \* partition the vertices of a graph *\ | ||||
|   {graph --> (list (list A))} | ||||
|   Graph -> (reduce (place-vertex Graph) [] (vertices Graph))) | ||||
|  | ||||
| (define bipartite? | ||||
|   \* check if a graph is bipartite *\ | ||||
|   {graph --> boolean} | ||||
|   Graph -> (= 2 (length (vertex-partition Graph)))) | ||||
|  | ||||
| ) | ||||
|  | ||||
| \* simple tests | ||||
|  | ||||
| (set g (graph)) | ||||
| (add-edge (value g) [chris patton]) | ||||
| (add-edge (value g) [eric chris]) | ||||
| (add-vertex (value g) nobody) | ||||
| (has-edge? (value g) [patton chris]) | ||||
| (edges-for (value g) chris) | ||||
| (neighbors (value g) chris) | ||||
| (neighbors (value g) nobody) | ||||
| (connected-to (value g) chris) | ||||
| (connected? (value g)) | ||||
| (connected-components (value g)) <- fail when package wrapper is used | ||||
| (map (function vertices) (connected-components (value g))) | ||||
|  | ||||
| *\ | ||||
							
								
								
									
										102
									
								
								samples/Shen/html.shen
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										102
									
								
								samples/Shen/html.shen
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,102 @@ | ||||
| \* html.shen --- html generation functions for shen | ||||
|  | ||||
| Copyright (C) 2011,  Eric Schulte | ||||
|  | ||||
| *** License: | ||||
|  | ||||
| Redistribution and use in source and binary forms, with or without | ||||
| modification, are permitted provided that the following conditions are | ||||
| met: | ||||
|  | ||||
|  - Redistributions of source code must retain the above copyright | ||||
|    notice, this list of conditions and the following disclaimer. | ||||
|  | ||||
|  - Redistributions in binary form must reproduce the above copyright | ||||
|    notice, this list of conditions and the following disclaimer in the | ||||
|    documentation and/or other materials provided with the distribution. | ||||
|  | ||||
| THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS | ||||
| "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT | ||||
| LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR | ||||
| A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT | ||||
| HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, | ||||
| SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT | ||||
| LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, | ||||
| DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY | ||||
| THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT | ||||
| (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE | ||||
| OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. | ||||
|  | ||||
| *** Commentary: | ||||
|  | ||||
| The standard lisp-to-html conversion tool suite.  Follows some of | ||||
| the convertions of Clojure's hiccup. | ||||
|  | ||||
|   an example... | ||||
|  | ||||
| (8-) (html [ul#todo1.tasks.stuff [: [title "today"]] | ||||
|           (map (lambda Str [li Str]) ["get milk" "dishes"])]) | ||||
| "<ul class='tasks stuff' id='todo1' title='today'> | ||||
|  <li>get milk</li><li>dishes</li></ul>" | ||||
|  | ||||
| *** Code: *\ | ||||
| (trap-error | ||||
|  (require string) | ||||
|  (/. E (load "../string/string.shen"))) | ||||
|  | ||||
| (package string- [html | ||||
|                   \* symbols included from string *\ | ||||
|                   takestr dropstr substr length-str index-str | ||||
|                   reverse-str starts-with substr? replace-str | ||||
|                   join split trim-left trim-right chomp trim] | ||||
|  | ||||
| (define to-str | ||||
|   \* return argument as a string, if already a string do not change *\ | ||||
|   X -> X where (string? X) | ||||
|   X -> (str X)) | ||||
|  | ||||
| (define gassoc | ||||
|   X Y -> (hd (tl (assoc X Y)))) | ||||
|  | ||||
| (define dassoc | ||||
|   X Y -> (remove (assoc X Y) Y)) | ||||
|  | ||||
| (define passoc | ||||
|   [] Y -> Y | ||||
|   [X XV] Y -> (let Orig (gassoc X Y) | ||||
|                    New (if (cons? Orig) [XV|Orig] XV) | ||||
|                 [[X New]|(dassoc X Y)])) | ||||
|  | ||||
| (define html | ||||
|   X -> X where (string? X) | ||||
|   [Tag [: |Attrs] |Body] -> | ||||
|     (let Tag-comps (css-parse-symbol Tag) | ||||
|          Tag (gassoc tag Tag-comps) | ||||
|          New-attrs (passoc (assoc class Tag-comps) | ||||
|                            (passoc (assoc id Tag-comps) Attrs)) | ||||
|       (@s (make-string "<~S" Tag) (attributes New-attrs) ">" | ||||
|           (html Body) | ||||
|           (make-string "</~S>" Tag))) where (symbol? Tag) | ||||
|   [Tag|Body] -> (html [Tag [:] Body]) where (symbol? Tag) | ||||
|   [H|HS] -> (@s (html H) (html HS)) | ||||
|   [] -> "") | ||||
|  | ||||
| (define css-parse-symbol | ||||
|   {symbol --> [[symbol A]]} | ||||
|   Symbol -> (let String (str Symbol) | ||||
|                  Class-split (split (str .) String) | ||||
|                  Class (map (function intern) (tl Class-split)) | ||||
|                  Id-split (split (str #) (hd Class-split)) | ||||
|                  Tag (hd Id-split) | ||||
|                  Id (tl Id-split) | ||||
|               ((if (= [] Id) (/. X X) (cons [id (intern (hd Id))])) | ||||
|                ((if (= [] Class) (/. X X) (cons [class Class]))  | ||||
|                 [[tag (intern Tag)]])))) | ||||
|  | ||||
| (define attributes | ||||
|   [] -> "" | ||||
|   [[K V]|AS] -> (@s " " (to-str K) "='" | ||||
|                     (if (cons? V) (join " " (map (function str) V)) (to-str V)) | ||||
|                     "'" (attributes AS))) | ||||
|  | ||||
| ) | ||||
							
								
								
									
										39
									
								
								samples/Shen/json.shen
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										39
									
								
								samples/Shen/json.shen
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,39 @@ | ||||
| (load "grammar.shen") | ||||
|  | ||||
| \* | ||||
|  | ||||
| JSON Lexer | ||||
|  | ||||
| 1. Read a stream of characters | ||||
| 2. Whitespace characters not in strings should be discarded. | ||||
| 3. Whitespace characters in strings should be preserved | ||||
| 4. Strings can contain escaped double quotes. e.g. "\"" | ||||
|  | ||||
| *\ | ||||
|  | ||||
| (define whitespacep | ||||
|   \* e.g. ASCII 32 == #\Space. *\ | ||||
|   \* All the others are whitespace characters from an ASCII table. *\ | ||||
|   Char -> (member Char ["c#9;" "c#10;" "c#11;" "c#12;" "c#13;" "c#32;"])) | ||||
|  | ||||
| (define replace-whitespace | ||||
|   "" -> "" | ||||
|   (@s Whitespace Suffix) -> (@s "" (replace-whitespace Suffix)) where (whitespacep Whitespace) | ||||
|   (@s Prefix Suffix) -> (@s Prefix (replace-whitespace Suffix))) | ||||
|  | ||||
| (define fetch-until-unescaped-doublequote | ||||
|   [] -> [] | ||||
|   ["\" "c#34;" | Chars] -> ["\" "c#34;" | (fetch-until-unescaped-doublequote Chars)] | ||||
|   ["c#34;" | Chars] -> [] | ||||
|   [Char | Chars] -> [Char | (fetch-until-unescaped-doublequote Chars)]) | ||||
|  | ||||
| \* (define strip-whitespace-chars *\ | ||||
| \*   [] -> [] *\ | ||||
| \*   ["c#34;" | Chars] -> ["c#34;" | ( *\ | ||||
| \*   [WhitespaceChar | Chars] -> (strip-whitespace-chars Chars) where (whitespace? WhitespaceChar) *\ | ||||
| \*   [Char | Chars] -> [Char | (strip-whitespace-chars Chars)]) *\ | ||||
|  | ||||
| (define tokenise | ||||
|   JSONString -> | ||||
|   (let CharList (explode JSONString) | ||||
|        CharList)) | ||||
							
								
								
									
										216
									
								
								samples/SystemVerilog/endpoint_phy_wrapper.svh
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										216
									
								
								samples/SystemVerilog/endpoint_phy_wrapper.svh
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,216 @@ | ||||
| module endpoint_phy_wrapper | ||||
|   ( | ||||
|    input clk_sys_i, | ||||
|    input clk_ref_i, | ||||
|    input clk_rx_i, | ||||
|    input rst_n_i, | ||||
|  | ||||
|    IWishboneMaster.master src, | ||||
|    IWishboneSlave.slave snk, | ||||
|    IWishboneMaster.master sys, | ||||
|     | ||||
|    output [9:0] td_o, | ||||
|    input [9:0] rd_i, | ||||
|  | ||||
|    output txn_o, | ||||
|    output txp_o, | ||||
|  | ||||
|    input rxn_i, | ||||
|    input rxp_i | ||||
|    ); | ||||
|  | ||||
|    wire rx_clock; | ||||
|     | ||||
|    parameter g_phy_type   = "GTP";    | ||||
|  | ||||
|    wire[15:0] gtx_data; | ||||
|    wire [1:0]gtx_k; | ||||
|    wire gtx_disparity; | ||||
|    wire gtx_enc_error; | ||||
|    wire [15:0] grx_data; | ||||
|    wire grx_clk; | ||||
|    wire [1:0]grx_k; | ||||
|    wire grx_enc_error; | ||||
|    wire [3:0] grx_bitslide; | ||||
|    wire gtp_rst; | ||||
|    wire tx_clock; | ||||
|     | ||||
|    generate | ||||
|       if(g_phy_type == "TBI") begin | ||||
|  | ||||
|          assign rx_clock  = clk_ref_i; | ||||
|          assign tx_clock  = clk_rx_i; | ||||
|           | ||||
|           | ||||
|          wr_tbi_phy U_Phy  | ||||
|            ( | ||||
|             .serdes_rst_i (gtp_rst), | ||||
|             .serdes_loopen_i(1'b0), | ||||
|             .serdes_prbsen_i(1'b0), | ||||
|             .serdes_enable_i(1'b1),  | ||||
|             .serdes_syncen_i(1'b1), | ||||
|  | ||||
|             .serdes_tx_data_i  (gtx_data[7:0]), | ||||
|             .serdes_tx_k_i     (gtx_k[0]), | ||||
|             .serdes_tx_disparity_o (gtx_disparity), | ||||
|             .serdes_tx_enc_err_o   (gtx_enc_error), | ||||
|  | ||||
|             .serdes_rx_data_o      (grx_data[7:0]), | ||||
|             .serdes_rx_k_o        (grx_k[0]), | ||||
|             .serdes_rx_enc_err_o  (grx_enc_error), | ||||
|             .serdes_rx_bitslide_o (grx_bitslide), | ||||
|  | ||||
|  | ||||
|             .tbi_refclk_i (clk_ref_i), | ||||
|             .tbi_rbclk_i  (clk_rx_i), | ||||
|  | ||||
|             .tbi_td_o     (td_o), | ||||
|             .tbi_rd_i     (rd_i), | ||||
|             .tbi_syncen_o (), | ||||
|             .tbi_loopen_o (), | ||||
|             .tbi_prbsen_o (), | ||||
|             .tbi_enable_o () | ||||
|             ); | ||||
|  | ||||
|       end else if (g_phy_type == "GTX") begin // if (g_phy_type == "TBI") | ||||
|          wr_gtx_phy_virtex6 | ||||
|            #( | ||||
|              .g_simulation(1) | ||||
|              ) U_PHY  | ||||
|              ( | ||||
|               .clk_ref_i(clk_ref_i), | ||||
|                | ||||
|               .tx_clk_o   (tx_clock), | ||||
|               .tx_data_i (gtx_data), | ||||
|               .tx_k_i (gtx_k), | ||||
|               .tx_disparity_o (gtx_disparity), | ||||
|               .tx_enc_err_o(gtx_enc_error), | ||||
|               .rx_rbclk_o (rx_clock), | ||||
|               .rx_data_o (grx_data), | ||||
|               .rx_k_o  (grx_k), | ||||
|               .rx_enc_err_o (grx_enc_error), | ||||
|               .rx_bitslide_o  (), | ||||
|  | ||||
|               .rst_i    (!rst_n_i), | ||||
|               .loopen_i (1'b0), | ||||
|  | ||||
|               .pad_txn_o (txn_o), | ||||
|               .pad_txp_o (txp_o), | ||||
|  | ||||
|               .pad_rxn_i (rxn_i), | ||||
|               .pad_rxp_i (rxp_i) | ||||
|     ); | ||||
|                     | ||||
|       end  else if (g_phy_type == "GTP") begin // if (g_phy_type == "TBI") | ||||
|          assign #1 tx_clock  = clk_ref_i; | ||||
|           | ||||
|          wr_gtp_phy_spartan6 | ||||
|            #( | ||||
|              .g_simulation(1) | ||||
|              ) U_PHY  | ||||
|              ( | ||||
|               .gtp_clk_i(clk_ref_i), | ||||
|               .ch0_ref_clk_i(clk_ref_i), | ||||
|                | ||||
|               .ch0_tx_data_i (gtx_data[7:0]), | ||||
|               .ch0_tx_k_i (gtx_k[0]), | ||||
|               .ch0_tx_disparity_o (gtx_disparity), | ||||
|               .ch0_tx_enc_err_o(gtx_enc_error), | ||||
|               .ch0_rx_rbclk_o (rx_clock), | ||||
|               .ch0_rx_data_o (grx_data[7:0]), | ||||
|               .ch0_rx_k_o  (grx_k[0]), | ||||
|               .ch0_rx_enc_err_o (grx_enc_error), | ||||
|               .ch0_rx_bitslide_o  (), | ||||
|  | ||||
|               .ch0_rst_i    (!rst_n_i), | ||||
|               .ch0_loopen_i (1'b0), | ||||
|  | ||||
|               .pad_txn0_o (txn_o), | ||||
|               .pad_txp0_o (txp_o), | ||||
|  | ||||
|               .pad_rxn0_i (rxn_i), | ||||
|               .pad_rxp0_i (rxp_i) | ||||
|               ); | ||||
|           | ||||
|       end // else: !if(g_phy_type == "TBI") | ||||
|    endgenerate | ||||
|     | ||||
|    wr_endpoint | ||||
|      #( | ||||
|        .g_simulation          (1), | ||||
|        .g_pcs_16bit(g_phy_type == "GTX" ? 1: 0), | ||||
|        .g_rx_buffer_size (1024), | ||||
|        .g_with_rx_buffer(0), | ||||
|        .g_with_timestamper    (1), | ||||
|        .g_with_dmtd           (0), | ||||
|        .g_with_dpi_classifier (1), | ||||
|        .g_with_vlans          (0), | ||||
|        .g_with_rtu            (0) | ||||
|        ) DUT ( | ||||
|               .clk_ref_i (clk_ref_i), | ||||
|               .clk_sys_i (clk_sys_i), | ||||
|               .clk_dmtd_i (clk_ref_i), | ||||
|               .rst_n_i  (rst_n_i), | ||||
|               .pps_csync_p1_i (1'b0), | ||||
|  | ||||
|               .phy_rst_o   (), | ||||
|               .phy_loopen_o (), | ||||
|               .phy_enable_o (), | ||||
|               .phy_syncen_o (), | ||||
|  | ||||
|               .phy_ref_clk_i      (tx_clock), | ||||
|               .phy_tx_data_o      (gtx_data), | ||||
|               .phy_tx_k_o         (gtx_k), | ||||
|               .phy_tx_disparity_i (gtx_disparity), | ||||
|               .phy_tx_enc_err_i   (gtx_enc_error), | ||||
|  | ||||
|               .phy_rx_data_i     (grx_data), | ||||
|               .phy_rx_clk_i      (rx_clock), | ||||
|               .phy_rx_k_i        (grx_k), | ||||
|               .phy_rx_enc_err_i  (grx_enc_error), | ||||
|               .phy_rx_bitslide_i (5'b0), | ||||
|  | ||||
|               .src_dat_o   (snk.dat_i), | ||||
|               .src_adr_o   (snk.adr), | ||||
|               .src_sel_o   (snk.sel), | ||||
|               .src_cyc_o   (snk.cyc), | ||||
|               .src_stb_o   (snk.stb), | ||||
|               .src_we_o    (snk.we), | ||||
|               .src_stall_i (snk.stall), | ||||
|               .src_ack_i   (snk.ack), | ||||
|               .src_err_i(1'b0), | ||||
|  | ||||
|               .snk_dat_i   (src.dat_o[15:0]), | ||||
|               .snk_adr_i   (src.adr[1:0]), | ||||
|               .snk_sel_i   (src.sel[1:0]), | ||||
|               .snk_cyc_i   (src.cyc), | ||||
|               .snk_stb_i   (src.stb), | ||||
|               .snk_we_i    (src.we), | ||||
|               .snk_stall_o (src.stall), | ||||
|               .snk_ack_o   (src.ack), | ||||
|               .snk_err_o   (src.err), | ||||
|               .snk_rty_o   (src.rty), | ||||
|  | ||||
|               .txtsu_ack_i (1'b1), | ||||
|  | ||||
|               .rtu_full_i (1'b0), | ||||
|               .rtu_almost_full_i (1'b0), | ||||
|               .rtu_rq_strobe_p1_o  (), | ||||
|               .rtu_rq_smac_o  (), | ||||
|               .rtu_rq_dmac_o (), | ||||
|               .rtu_rq_vid_o  (), | ||||
|               .rtu_rq_has_vid_o (), | ||||
|               .rtu_rq_prio_o (), | ||||
|               .rtu_rq_has_prio_o (), | ||||
|  | ||||
|               .wb_cyc_i(sys.cyc), | ||||
|               .wb_stb_i (sys.stb), | ||||
|               .wb_we_i (sys.we), | ||||
|               .wb_sel_i(sys.sel), | ||||
|               .wb_adr_i(sys.adr[7:0]), | ||||
|               .wb_dat_i(sys.dat_o), | ||||
|               .wb_dat_o(sys.dat_i), | ||||
|               .wb_ack_o (sys.ack) | ||||
|     ); | ||||
|  | ||||
| endmodule // endpoint_phy_wrapper | ||||
							
								
								
									
										7
									
								
								samples/SystemVerilog/fifo.sv
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										7
									
								
								samples/SystemVerilog/fifo.sv
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,7 @@ | ||||
| module fifo ( | ||||
|     input           clk_50, | ||||
|     input           clk_2, | ||||
|     input           reset_n, | ||||
|     output [7:0]    data_out, | ||||
|     output          empty | ||||
| ); | ||||
							
								
								
									
										18
									
								
								samples/SystemVerilog/priority_encoder.sv
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										18
									
								
								samples/SystemVerilog/priority_encoder.sv
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,18 @@ | ||||
| // http://hdlsnippets.com/parameterized_priority_encoder | ||||
| module priority_encoder #(parameter INPUT_WIDTH=8,OUTPUT_WIDTH=3) | ||||
| ( | ||||
|  input  logic [INPUT_WIDTH-1:0]  input_data, | ||||
|  output logic [OUTPUT_WIDTH-1:0] output_data | ||||
| ); | ||||
|   | ||||
| int ii; | ||||
|   | ||||
| always_comb | ||||
| begin | ||||
|   output_data = 'b0; | ||||
| 	for(ii=0;ii<INPUT_WIDTH;ii++) | ||||
| 		if (input_data[ii]) | ||||
| 			output_data = ii[OUTPUT_WIDTH-1:0]; | ||||
| end | ||||
|  | ||||
| endmodule | ||||
							
								
								
									
										8
									
								
								samples/SystemVerilog/util.vh
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										8
									
								
								samples/SystemVerilog/util.vh
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,8 @@ | ||||
| function integer log2; | ||||
|   input integer x; | ||||
|   begin | ||||
|     x = x-1; | ||||
|     for (log2 = 0; x > 0; log2 = log2 + 1) | ||||
|       x = x >> 1; | ||||
|   end | ||||
| endfunction | ||||
							
								
								
									
										20
									
								
								samples/YAML/vcr_cassette.yml
									
									
									
									
									
										Normal file
									
								
							
							
						
						
									
										20
									
								
								samples/YAML/vcr_cassette.yml
									
									
									
									
									
										Normal file
									
								
							| @@ -0,0 +1,20 @@ | ||||
| --- | ||||
| http_interactions: | ||||
| - request: | ||||
|     method: get | ||||
|     uri: http://example.com/ | ||||
|     body: '' | ||||
|     headers: {} | ||||
|   response: | ||||
|     status: | ||||
|       code: 200 | ||||
|       message: OK | ||||
|     headers: | ||||
|       Content-Type: | ||||
|       - text/html;charset=utf-8 | ||||
|       Content-Length: | ||||
|       - '26' | ||||
|     body: This is the response body | ||||
|     http_version: '1.1' | ||||
|   recorded_at: Tue, 01 Nov 2011 04:58:44 GMT | ||||
| recorded_with: VCR 2.0.0 | ||||
| @@ -211,6 +211,9 @@ class TestBlob < Test::Unit::TestCase | ||||
|     assert !blob("CSS/bootstrap.css").generated? | ||||
|     assert blob("CSS/bootstrap.min.css").generated? | ||||
|  | ||||
|     # Generated VCR | ||||
|     assert blob("YAML/vcr_cassette.yml").generated? | ||||
|  | ||||
|     assert Linguist::Generated.generated?("node_modules/grunt/lib/grunt.js", nil) | ||||
|   end | ||||
|  | ||||
| @@ -343,6 +346,14 @@ class TestBlob < Test::Unit::TestCase | ||||
|  | ||||
|     # Vagrant | ||||
|     assert blob("Vagrantfile").vendored? | ||||
|  | ||||
|     # Gradle | ||||
|     assert blob("gradlew").vendored? | ||||
|     assert blob("gradlew.bat").vendored? | ||||
|     assert blob("gradle/wrapper/gradle-wrapper.properties").vendored? | ||||
|     assert blob("subproject/gradlew").vendored? | ||||
|     assert blob("subproject/gradlew.bat").vendored? | ||||
|     assert blob("subproject/gradle/wrapper/gradle-wrapper.properties").vendored? | ||||
|   end | ||||
|  | ||||
|   def test_language | ||||
|   | ||||
| @@ -50,6 +50,18 @@ class TestHeuristcs < Test::Unit::TestCase | ||||
|     results = Heuristics.disambiguate_pl(fixture("Perl/perl-test.t"), languages) | ||||
|     assert_equal Language["Perl"], results.first | ||||
|   end | ||||
|    | ||||
|   def test_ecl_prolog_by_heuristics | ||||
|     languages = ["ECL", "Prolog"] | ||||
|     results = Heuristics.disambiguate_ecl(fixture("Prolog/or-constraint.ecl"), languages) | ||||
|     assert_equal Language["Prolog"], results.first | ||||
|   end | ||||
|    | ||||
|   def test_ecl_ecl_by_heuristics | ||||
|     languages = ["ECL", "Prolog"] | ||||
|     results = Heuristics.disambiguate_ecl(fixture("ECL/sample.ecl"), languages) | ||||
|     assert_equal Language["ECL"], results.first | ||||
|   end | ||||
|  | ||||
|   def test_ts_typescript_by_heuristics | ||||
|     languages = ["TypeScript", "XML"] | ||||
|   | ||||
| @@ -10,6 +10,7 @@ class TestLanguage < Test::Unit::TestCase | ||||
|  | ||||
|   def test_lexer | ||||
|     assert_equal Lexer['ActionScript 3'], Language['ActionScript'].lexer | ||||
|     assert_equal Lexer['AspectJ'], Language['AspectJ'].lexer | ||||
|     assert_equal Lexer['Bash'], Language['Gentoo Ebuild'].lexer | ||||
|     assert_equal Lexer['Bash'], Language['Gentoo Eclass'].lexer | ||||
|     assert_equal Lexer['Bash'], Language['Shell'].lexer | ||||
| @@ -322,7 +323,7 @@ class TestLanguage < Test::Unit::TestCase | ||||
|   def test_color | ||||
|     assert_equal '#701516', Language['Ruby'].color | ||||
|     assert_equal '#3581ba', Language['Python'].color | ||||
|     assert_equal '#f15501', Language['JavaScript'].color | ||||
|     assert_equal '#f7df1e', Language['JavaScript'].color | ||||
|     assert_equal '#31859c', Language['TypeScript'].color | ||||
|   end | ||||
|  | ||||
|   | ||||
		Reference in New Issue
	
	Block a user