language-ats 0.1.0.0 → 0.1.0.1
raw patch · 29 files changed
+5397/−1 lines, 29 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- language-ats.cabal +4/−1
- test/data/combinatorics.dats +40/−0
- test/data/combinatorics.out +43/−0
- test/data/concurrency.dats +257/−0
- test/data/concurrency.out +287/−0
- test/data/fact.dats +32/−0
- test/data/fact.out +39/−0
- test/data/factorial.dats +4/−0
- test/data/factorial.out +4/−0
- test/data/fast-combinatorics.dats +93/−0
- test/data/fast-combinatorics.out +94/−0
- test/data/fib.dats +6/−0
- test/data/fib.out +6/−0
- test/data/filecount.dats +31/−0
- test/data/filecount.out +41/−0
- test/data/filetype.out +180/−0
- test/data/filetype.sats +180/−0
- test/data/left-pad.dats +98/−0
- test/data/left-pad.out +76/−0
- test/data/number-theory.dats +167/−0
- test/data/number-theory.out +186/−0
- test/data/numerics.dats +61/−0
- test/data/numerics.out +63/−0
- test/data/polyglot.dats +1235/−0
- test/data/polyglot.out +1619/−0
- test/data/toml-parse.dats +244/−0
- test/data/toml-parse.out +260/−0
- test/data/types.out +24/−0
- test/data/types.sats +23/−0
language-ats.cabal view
@@ -1,5 +1,5 @@ name: language-ats-version: 0.1.0.0+version: 0.1.0.1 synopsis: Parser and pretty-printer for ATS. description: Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. homepage: https://github.com/vmchale/language-ats#readme@@ -13,6 +13,9 @@ extra-doc-files: README.md extra-source-files: stack.yaml , cabal.project.local+data-files: test/data/*.dats+ , test/data/*.sats+ , test/data/*.out cabal-version: 1.18 Flag development {
+ test/data/combinatorics.dats view
@@ -0,0 +1,40 @@+#define ATS_MAINATSFLAG 1++#include "share/atspre_staload.hats"++staload "contrib/atscntrb-hx-intinf/SATS/intinf_t.sats"+staload "libats/libc/SATS/math.sats"+staload "contrib/atscntrb-hx-intinf/SATS/intinf.sats"+staload UN = "prelude/SATS/unsafe.sats"++fnx fact {n : nat} .<n>. (k : int(n)) : [ n : nat | n > 0 ] intinf(n) =+ case+ k of+ | 0 => int2intinf(1)+ | 1 => int2intinf(1)+ | k =>> $UN.cast(fact(k - 1) * k)++// double factorial http://mathworld.wolfram.com/DoubleFactorial.html+fnx dfact {n : nat} .<n>. (k : int(n)) : Intinf =+ case+ k of+ | 0 => int2intinf(1)+ | 1 => int2intinf(1)+ | k =>> k * dfact(k - 2)++// Number of permutations on n objects using k at a time.+fn permutatsions {n : nat}{ k : nat | k <= n } (n : int(n), k : int(k)) : Intinf =+ ndiv(fact(n), fact(n - k))++// Number of permutations on n objects using k at a time.+fn choose {n : nat}{ m : nat | m <= n } (n : int(n), k : int(m)) : Intinf =+ let+ fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) : [ n : nat | n > 0 ] intinf(n) =+ case+ i of+ | 1 => int2intinf(n)+ | 2 => $UN.cast(int2intinf(n - 1) * n)+ | i =>> $UN.cast((n + 1 - i) * numerator_loop(i - 1))+ in+ case+ k of+ | 0 => int2intinf(1)+ | 1 => int2intinf(n)+ | k =>> ndiv(numerator_loop(k), fact(k))+ end
+ test/data/combinatorics.out view
@@ -0,0 +1,43 @@+#define ATS_MAINATSFLAG 1++#include "share/atspre_staload.hats"++staload "contrib/atscntrb-hx-intinf/SATS/intinf_t.sats"+staload "libats/libc/SATS/math.sats"+staload "contrib/atscntrb-hx-intinf/SATS/intinf.sats"+staload UN = "prelude/SATS/unsafe.sats"++fnx fact {n:nat} .<n>. (k : int(n)) : [ n : nat | n > 0 ] intinf(n) =+ case+ k of+ | 0 => int2intinf(1)+ | 1 => int2intinf(1)+ | k =>> $UN.cast(fact(k - 1) * k)++// double factorial http://mathworld.wolfram.com/DoubleFactorial.html+fnx dfact {n:nat} .<n>. (k : int(n)) : Intinf =+ case+ k of+ | 0 => int2intinf(1)+ | 1 => int2intinf(1)+ | k =>> k * dfact(k - 2)++// Number of permutations on n objects using k at a time.+fn permutatsions {n:nat}{ k : nat | k <= n } (n : int(n), k : int(k)) :+ Intinf =+ ndiv(fact(n), fact(n - k))++// Number of permutations on n objects using k at a time.+fn choose {n:nat}{ m : nat | m <= n } (n : int(n), k : int(m)) :+ Intinf =+ let+ fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) :+ [ n : nat | n > 0 ] intinf(n) =+ case+ i of+ | 1 => int2intinf(n)+ | 2 => $UN.cast(int2intinf(n - 1) * n)+ | i =>> $UN.cast((n + 1 - i) * numerator_loop(i - 1))+ in+ case+ k of+ | 0 => int2intinf(1)+ | 1 => int2intinf(n)+ | k =>> ndiv(numerator_loop(k), fact(k))+ end
+ test/data/concurrency.dats view
@@ -0,0 +1,257 @@+// This is mostly taken from the example in the book.++#include "share/atspre_staload.hats"+#include "share/atspre_staload_libats_ML.hats"+#include "libats/DATS/athread_posix.dats"++staload "libats/SATS/athread.sats"+staload "src/filetype.sats"+staload "libats/SATS/funarray.sats"+staload "libats/SATS/deqarray.sats"+staload _ = "libats/DATS/deqarray.dats"++absvtype queue_vtype(a: vt@ype+, int) = ptr++vtypedef queue(a: vt0p, id: int) = queue_vtype(a, id)+vtypedef queue(a: vt0p) = [id:int] queue(a, id)++absprop ISNIL(id: int, b: bool)++extern fun {a:vt0p} queue_is_nil {id:int} (!queue(a, id)) : [b:bool] (ISNIL(id, b) | bool(b))++absprop ISFULL(id: int, b: bool)++extern fun {a:vt0p} queue_is_full {id:int} (!queue(a, id)) : [b:bool] (ISFULL(id, b) | bool(b))++extern fun {a:vt0p} queue_insert {id:int} (ISFULL(id, false) | xs: !queue(a, id) >> queue(a, id2), x: a) : #[id2:int] void++extern fun {a:vt0p} queue_remove {id:int} (ISNIL(id, false) | xs: !queue(a, id) >> queue(a, id2)) : #[id2:int] a++extern fun {a:vt0p} queue_make (cap: intGt(0)) : queue(a)++extern fun {a:t@ype} queue_free(que: queue(a)) : void++assume queue_vtype(a: vt0p, id: int) = deqarray(a)+assume ISNIL(id: int, b: bool) = unit_p+assume ISFULL(id: int, b: bool) = unit_p++absvtype channel_vtype(a: vt@ype+) = ptr++vtypedef channel(a: vt0p) = channel_vtype(a)++extern fun {a:vt0p} channel_insert (!channel(a), a) : void++extern fun {a:vt0p} channel_remove (chan: !channel(a)) : a++extern fun {a:vt0p} channel_remove_helper (chan: !channel(a), !queue(a) >> _) : a++extern fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) : void++datavtype channel_ = {l0,l1,l2,l3:agz} CHANNEL of+ @{ cap = intGt(0)+ , spin = spin_vt(l0)+ , refcount = intGt(0)+ , mutex = mutex_vt(l1)+ , CVisNil = condvar_vt(l2)+ , CVisFull = condvar_vt(l3)+ , queue = ptr+ }++extern fun {a:vt0p} channel_make(cap: intGt(0)) : channel(a)++extern fun {a:vt0p} channel_ref(ch: !channel(a)) : channel(a)++extern fun {a:vt0p} channel_unref(ch: channel(a)) : Option_vt(queue(a))++extern fun channel_refcount{a:vt0p}(ch: !channel(a)) : intGt(0)++assume channel_vtype(a:vt0p) = channel_++implement {a} queue_is_nil(xs) = (unit_p() | deqarray_is_nil(xs))++implement {a} queue_is_full(xs) = (unit_p() | deqarray_is_full(xs))++implement {a} queue_remove(prf | xs) = + let+ prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISNIL(id, false)) : [false] void }+ in+ deqarray_takeout_atbeg<a> (xs)+ end++implement {a} queue_insert(prf | xs, x) = + { + prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISFULL(id, false)) : [false] void }+ val () = deqarray_insert_atend<a>(xs, x)+ }++implement {a} queue_make(cap) = deqarray_make_cap(i2sz(cap))++implement {a} queue_free(que) = deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))++implement {a} channel_ref(chan) =+ let+ val@ CHANNEL(ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = ch.refcount := ch.refcount + 1+ val () = spin_unlock (prf | spin)+ prval () = fold@(chan)+ in+ $UN.castvwtp1{channel(a)}(chan)+ end++implement {a} channel_unref(chan) = + let+ val@ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = spin_unlock(prf | spin)+ val refcount = ch.refcount // needed to make the theorem prover work+ in+ if refcount <= 1 then+ let+ val que = $UN.castvwtp0{queue(a)}(ch.queue)+ val () = spin_vt_destroy(ch.spin)+ val () = mutex_vt_destroy(ch.mutex)+ val () = condvar_vt_destroy(ch.CVisNil)+ val () = condvar_vt_destroy(ch.CVisFull)+ val () = free@{l0,l1,l2,l3}(chan)+ in+ Some_vt(que)+ end+ else+ let+ val () = ch.refcount := refcount - 1+ prval () = fold@chan+ prval () = $UN.cast2void(chan)+ in+ None_vt()+ end+ end++implement channel_refcount{a}(chan) =+ let+ val@ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val refcount = ch.refcount+ in+ fold@(chan) ; refcount+ end++implement {a} channel_make(cap) = + let+ extern praxi __assert() : [l:agz] void++ prval [l0:addr] () = __assert()+ prval [l1:addr] () = __assert()+ prval [l2:addr] () = __assert()+ prval [l3:addr] () = __assert()++ val chan = CHANNEL{l0,l1,l2,l3}(_)+ val+ CHANNEL(ch) = chan++ val () = ch.cap := cap+ val () = ch.refcount := 1+ + local + val x = spin_create_exn()+ in+ val () = ch.spin := unsafe_spin_t2vt(x)+ end++ local+ val x = mutex_create_exn()+ in+ val () = ch.mutex := unsafe_mutex_t2vt(x)+ end++ local+ val x = condvar_create_exn()+ in+ val () = ch.CVisNil := unsafe_condvar_t2vt(x)+ end++ local+ val x = condvar_create_exn()+ in+ val () = ch.CVisFull := unsafe_condvar_t2vt(x)+ end++ val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))++ in+ fold@(chan) ; chan+ end++implement {a} channel_insert(chan, x) = + let+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val () = channel_insert_helper<a>(chan, xs, x)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex)+ in+ end++implement {a} channel_remove(chan) = x where+ {+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val x = channel_remove_helper<a> (chan, xs)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex)+ }++implement {a} channel_remove_helper(chan, xs) =+ let+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val (prf | is_nil) = queue_is_nil(xs)+ in+ if is_nil then+ let+ prval (pfmut, fpf) = __assert() where { extern praxi __assert(): vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisNil = unsafe_condvar_vt2t(ch.CVisNil)+ val () = condvar_wait(pfmut | CVisNil, mutex)+ prval () = fpf(pfmut)+ in+ channel_remove_helper(chan, xs)+ end+ else+ let+ val is_full = queue_is_full(xs)+ val x_out = queue_remove(prf | xs)+ val () = if is_full.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull))+ in+ x_out+ end+ end++implement {a} channel_insert_helper(chan, xs, x) = + let+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val (prf | is_full) = queue_is_full(xs)+ in+ if is_full then+ let+ prval (pfmut, fpf) = __assert() where { extern praxi __assert() : vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisFull = unsafe_condvar_vt2t(ch.CVisFull)+ val () = condvar_wait(pfmut | CVisFull, mutex)+ prval () = fpf(pfmut)+ in+ channel_insert_helper(chan, xs, x)+ end+ else+ let+ val is_nil = queue_is_nil(xs)+ val () = queue_insert(prf | xs, x)+ val () = if is_nil.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil))+ in+ end+ end
+ test/data/concurrency.out view
@@ -0,0 +1,287 @@+// This is mostly taken from the example in the book.+#include "share/atspre_staload.hats"+#include "share/atspre_staload_libats_ML.hats"+#include "libats/DATS/athread_posix.dats"++staload "libats/SATS/athread.sats"+staload "src/filetype.sats"+staload "libats/SATS/funarray.sats"+staload "libats/SATS/deqarray.sats"+staload _ = "libats/DATS/deqarray.dats"++absvtype queue_vtype(a : vt@ype+, int) = ptr++vtypedef queue(a : vt0p, id : int) = queue_vtype(a, id)+vtypedef queue(a : vt0p) = [id:int] queue(a, id)++absprop ISNIL (id : int, b : bool)++extern+fun {a:vt0p} queue_is_nil {id:int} (!queue(a, id)) :+ [b:bool] (ISNIL(id, b) | bool(b))++absprop ISFULL (id : int, b : bool)++extern+fun {a:vt0p} queue_is_full {id:int} (!queue(a, id)) :+ [b:bool] (ISFULL(id, b) | bool(b))++extern+fun {a:vt0p} queue_insert {id:int}+(ISFULL(id,false) | xs : !queue(a, id) >> queue(a, id2), x : a) :+ #[id2:int] void++extern+fun {a:vt0p} queue_remove {id:int}+(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a++extern+fun {a:vt0p} queue_make (cap : intGt(0)) : queue(a)++extern+fun {a:t@ype} queue_free (que : queue(a)) : void++assume queue_vtype(a : vt0p, id : int) = deqarray(a)++assume ISNIL(id : int, b : bool) = unit_p++assume ISFULL(id : int, b : bool) = unit_p++absvtype channel_vtype(a : vt@ype+) = ptr++vtypedef channel(a : vt0p) = channel_vtype(a)++extern+fun {a:vt0p} channel_insert (!channel(a), a) : void++extern+fun {a:vt0p} channel_remove (chan : !channel(a)) : a++extern+fun {a:vt0p} channel_remove_helper ( chan : !channel(a)+ , !queue(a) >> _+ ) : a++extern+fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) :+ void++datavtype channel_ =+ | { l0, l1, l2, l3 : agz } CHANNEL of @{ cap = intGt(0)+ , spin = spin_vt(l0)+ , refcount = intGt(0)+ , mutex = mutex_vt(l1)+ , CVisNil = condvar_vt(l2)+ , CVisFull = condvar_vt(l3)+ , queue = ptr+ }++extern+fun {a:vt0p} channel_make (cap : intGt(0)) : channel(a)++extern+fun {a:vt0p} channel_ref (ch : !channel(a)) : channel(a)++extern+fun {a:vt0p} channel_unref (ch : channel(a)) : Option_vt(queue(a))++extern+fun channel_refcount {a:vt0p} (ch : !channel(a)) : intGt(0)++assume channel_vtype(a : vt0p) = channel_++implement {a} queue_is_nil (xs) =+ (unit_p() | deqarray_is_nil(xs))++implement {a} queue_is_full (xs) =+ (unit_p() | deqarray_is_full(xs))++implement {a} queue_remove (prf | xs) =+ let+ prval () = __assert(prf) where+ { extern+ praxi __assert {id:int} (p : ISNIL(id, false)) : [ false ] void }+ in+ deqarray_takeout_atbeg<a>(xs)+ end++implement {a} queue_insert (prf | xs, x) =+ {+ prval () = __assert(prf) where+ { extern+ praxi __assert {id:int} (p : ISFULL(id, false)) : [ false ] void }+ val () = deqarray_insert_atend<a>(xs, x)+ }++implement {a} queue_make (cap) =+ deqarray_make_cap(i2sz(cap))++implement {a} queue_free (que) =+ deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))++implement {a} channel_ref (chan) =+ let+ val @CHANNEL (ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = ch.refcount := ch.refcount + 1+ val () = spin_unlock(prf | spin)+ prval () = fold@(chan)+ in+ $UN.castvwtp1{channel(a)}(chan)+ end++implement {a} channel_unref (chan) =+ let+ val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = spin_unlock(prf | spin)+ val refcount = ch.refcount+ in+ if refcount <= 1 then+ let+ val que = $UN.castvwtp0{queue(a)}(ch.queue)+ val () = spin_vt_destroy(ch.spin)+ val () = mutex_vt_destroy(ch.mutex)+ val () = condvar_vt_destroy(ch.CVisNil)+ val () = condvar_vt_destroy(ch.CVisFull)+ val () = free@{l0,l1,l2,l3}(chan)+ in+ Some_vt(que)+ end+ else+ let+ val () = ch.refcount := refcount - 1+ prval () = fold@(chan)+ prval () = $UN.cast2void(chan)+ in+ None_vt()+ end+ end++implement channel_refcount {a} (chan) =+ let+ val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val refcount = ch.refcount+ in+ (fold@(chan) ; refcount)+ end++implement {a} channel_make (cap) =+ let+ extern+ praxi __assert() : [l:agz] void+ + prval [l0:addr]() = __assert()+ prval [l1:addr]() = __assert()+ prval [l2:addr]() = __assert()+ prval [l3:addr]() = __assert()+ val chan = CHANNEL{l0,l1,l2,l3}(_)+ val+ CHANNEL (ch) = chan+ val () = ch.cap := cap+ val () = ch.refcount := 1+ + local+ val x = spin_create_exn()+ in+ val () = ch.spin := unsafe_spin_t2vt(x)+ end+ + local+ val x = mutex_create_exn()+ in+ val () = ch.mutex := unsafe_mutex_t2vt(x)+ end+ + local+ val x = condvar_create_exn()+ in+ val () = ch.CVisNil := unsafe_condvar_t2vt(x)+ end+ + local+ val x = condvar_create_exn()+ in+ val () = ch.CVisFull := unsafe_condvar_t2vt(x)+ end+ + val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))+ in+ (fold@(chan) ; chan)+ end++implement {a} channel_insert (chan, x) =+ let+ val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val () = channel_insert_helper<a>(chan, xs, x)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex)+ in end++implement {a} channel_remove (chan) =+ x where+ { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val x = channel_remove_helper<a>(chan, xs)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex) }++implement {a} channel_remove_helper (chan, xs) =+ let+ val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val (prf | is_nil) = queue_is_nil(xs)+ in+ if is_nil then+ let+ prval (pfmut, fpf) = __assert() where+ { extern+ praxi __assert() : vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisNil = unsafe_condvar_vt2t(ch.CVisNil)+ val () = condvar_wait(pfmut | CVisNil, mutex)+ prval () = fpf(pfmut)+ in+ channel_remove_helper(chan, xs)+ end+ else+ let+ val is_full = queue_is_full(xs)+ val x_out = queue_remove(prf | xs)+ val () = if is_full.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull))+ in+ x_out+ end+ end++implement {a} channel_insert_helper (chan, xs, x) =+ let+ val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val (prf | is_full) = queue_is_full(xs)+ in+ if is_full then+ let+ prval (pfmut, fpf) = __assert() where+ { extern+ praxi __assert() : vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisFull = unsafe_condvar_vt2t(ch.CVisFull)+ val () = condvar_wait(pfmut | CVisFull, mutex)+ prval () = fpf(pfmut)+ in+ channel_insert_helper(chan, xs, x)+ end+ else+ let+ val is_nil = queue_is_nil(xs)+ val () = queue_insert(prf | xs, x)+ val () = if is_nil.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil))+ in end+ end
+ test/data/fact.dats view
@@ -0,0 +1,32 @@+#include "share/atspre_staload.hats"+#include "share/HATS/atslib_staload_libats_libc.hats"++fnx fact_boring(n: int) : int =+ case+ n of+ | 0 => 1+ | n => n * fact_boring(n-1)++(* fnx collatz{n:nat} *)+(* (n: int(n)) : int = let *)+(* fun loop{n:nat}{l:addr} .<n>. *)+(* (pf: !int @ l | n: int n, res: ptr l) : void = *)+(* if n > 1 *)++// TODO rewrite this for collatz?+fnx fact{n:nat}+(n: int (n)): int = let+fun loop{n:nat}{l:addr} .<n>.+(pf: !int @ l | n: int n, res: ptr l): void =+if n > 0 then let+val () = !res := n * !res in loop (pf | n-1, res)+end // end of [if]+// end of [loop]+var res: int with pf = 1+val () = loop (pf | n, addr@res) // addr@res: the pointer to res+in+res+end // end of [fact]++implement main0 () =+ let val x = fact(30) in+ println!(tostring_int(x)) end
+ test/data/fact.out view
@@ -0,0 +1,39 @@+#include "share/atspre_staload.hats"+#include "share/HATS/atslib_staload_libats_libc.hats"++fnx fact_boring(n : int) : int =+ case+ n of+ | 0 => 1+ | n => n * fact_boring(n - 1)++(* fnx collatz{n:nat} *)+(* (n: int(n)) : int = let *)+(* fun loop{n:nat}{l:addr} .<n>. *)+(* (pf: !int @ l | n: int n, res: ptr l) : void = *)+(* if n > 1 *)+// TODO rewrite this for collatz?+fnx fact {n:nat} (n : int(n)) : int =+ let+ fun loop {n:nat}{l:addr} .<n>. ( pf : !int @ l | n : int(n)+ , res : ptr(l)+ ) : void =+ if n > 0 then+ let+ val () = !res := n * !res+ in+ loop(pf | n - 1, res)+ end+ + // end of [loop]+ var res: int with pf = 1+ val () = loop(pf | n, addr@res)+ in+ res+ end++implement main0 () =+ let+ val x = fact(30)+ in+ println!(tostring_int(x))+ end
+ test/data/factorial.dats view
@@ -0,0 +1,4 @@+fun factorial_recursion {n:nat} .<n>. (n: int(n)) : int =+case+ n of+| 0 => 1+| n =>> factorial_recursion(n-1) * n
+ test/data/factorial.out view
@@ -0,0 +1,4 @@+fun factorial_recursion {n:nat} .<n>. (n : int(n)) : int =+ case+ n of+ | 0 => 1+ | n =>> factorial_recursion(n - 1) * n
+ test/data/fast-combinatorics.dats view
@@ -0,0 +1,93 @@+#define ATS_MAINATSFLAG 1++#include "share/atspre_staload.hats"++staload "libats/libc/SATS/math.sats"++fnx fact {n : nat} .<n>. (k : int(n)) :<> int =+ case+ k of+ | 0 => 1+ | k =>> fact(k - 1) * k++fnx dfact {n : nat} .<n>. (k : int(n)) :<> int =+ case+ k of+ | 0 => 1+ | 1 => 1+ | k =>> k * dfact(k - 2)++// TODO make this more versatile?+fn choose {n : nat}{ m : nat | m <= n } (n : int(n), k : int(m)) : int =+ let+ fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) : int =+ case+ i of+ | 1 => n+ | 2 => (n - 1) * n+ | i =>> (n + 1 - i) * numerator_loop(i - 1)+ in+ case+ k of+ | 0 => 1+ | 1 => n+ | k =>> numerator_loop(k) / fact(k)+ end++// FIXME+fun bad(n : int) : [ m : nat ] int(m) =+ case+ n of+ | 0 => 0+ | n => 1 + bad(n - 1)++fun is_prime(k : intGt(0)) : bool =+ case+ k of+ | 1 => false+ | k => + begin+ let+ var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))+ var bound: [ m : nat ] int(m) = bad(pre_bound)+ + fun loop {n : nat}{m : nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<> bool =+ if i < bound then+ if k mod i = 0 then+ false+ else+ true && loop(i + 1, bound)+ else+ if i = bound then+ if k mod i = 0 then+ false+ else+ true+ else+ true+ in+ loop(2, bound)+ end+ end++extern+fun choose_ats {n : nat}{ m : nat | m <= n } : (int(n), int(m)) -> int =+ "mac#"++extern+fun double_factorial {n : nat} : int(n) -> int =+ "mac#"++extern+fun factorial_ats {n : nat} : int(n) -> int =+ "mac#"++extern+fun is_prime_ats { n : nat | n > 0 } : int(n) -> bool =+ "mac#"++implement choose_ats (n, k) =+ choose(n, k)++implement double_factorial (m) =+ dfact(m)++implement is_prime_ats (n) =+ is_prime(n)++implement factorial_ats (m) =+ fact(m)
+ test/data/fast-combinatorics.out view
@@ -0,0 +1,94 @@+#define ATS_MAINATSFLAG 1++#include "share/atspre_staload.hats"++staload "libats/libc/SATS/math.sats"++fnx fact {n:nat} .<n>. (k : int(n)) :<> int =+ case+ k of+ | 0 => 1+ | k =>> fact(k - 1) * k++fnx dfact {n:nat} .<n>. (k : int(n)) :<> int =+ case+ k of+ | 0 => 1+ | 1 => 1+ | k =>> k * dfact(k - 2)++// TODO make this more versatile?+fn choose {n:nat}{ m : nat | m <= n } (n : int(n), k : int(m)) : int =+ let+ fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) : int =+ case+ i of+ | 1 => n+ | 2 => (n - 1) * n+ | i =>> (n + 1 - i) * numerator_loop(i - 1)+ in+ case+ k of+ | 0 => 1+ | 1 => n+ | k =>> numerator_loop(k) / fact(k)+ end++// FIXME+fun bad(n : int) : [m:nat] int(m) =+ case+ n of+ | 0 => 0+ | n => 1 + bad(n - 1)++fun is_prime(k : intGt(0)) : bool =+ case+ k of+ | 1 => false+ | k => + begin+ let+ var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))+ var bound: [m:nat] int(m) = bad(pre_bound)+ + fun loop {n:nat}{m:nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<>+ bool =+ if i < bound then+ if k % i = 0 then+ false+ else+ true && loop(i + 1, bound)+ else+ if i = bound then+ if k % i = 0 then+ false+ else+ true+ else+ true+ in+ loop(2, bound)+ end+ end++extern+fun choose_ats {n:nat}{ m : nat | m <= n } : (int(n), int(m)) -> int =+ "mac#"++extern+fun double_factorial {n:nat} : int(n) -> int =+ "mac#"++extern+fun factorial_ats {n:nat} : int(n) -> int =+ "mac#"++extern+fun is_prime_ats { n : nat | n > 0 } : int(n) -> bool =+ "mac#"++implement choose_ats (n, k) =+ choose(n, k)++implement double_factorial (m) =+ dfact(m)++implement is_prime_ats (n) =+ is_prime(n)++implement factorial_ats (m) =+ fact(m)
+ test/data/fib.dats view
@@ -0,0 +1,6 @@+#include "prelude/DATS/integer.dats"++fnx fib { n : int | n >= 0 } .<n>. (i : int(n)) : int =+case+ i of+| _ when i - 2 >= 0 => ( fib(i-1) + fib(i-2) )+| _ => 1
+ test/data/fib.out view
@@ -0,0 +1,6 @@+#include "prelude/DATS/integer.dats"++fnx fib { n : int | n >= 0 } .<n>. (i : int(n)) : int =+ case+ i of+ | _ when i - 2 >= 0 => (fib(i - 1) + fib(i - 2))+ | _ => 1
+ test/data/filecount.dats view
@@ -0,0 +1,31 @@+#include "share/atspre_staload.hats"+#include "libats/ML/DATS/filebas_dirent.dats"+#include "libats/libc/DATS/dirent.dats"++staload "libats/ML/DATS/string.dats"++fun good_dir(next: string) : bool = case next of | "." => false | ".." => false | _ => true+fnx step_stream(acc: int, s: string) : int =+if test_file_isdir(s) != 0 then+flow_stream(s, acc + 1)+else+acc + 1+and flow_stream(s: string, init: int) : int =+let+var files = streamize_dirname_fname(s)+var ffiles = stream_vt_filter_cloptr(files, lam x => good_dir(x))+in+stream_vt_foldleft_cloptr(ffiles, init, lam (acc, next) => step_stream(acc, s + "/" + next))+end+fun count_files(s: string) : void =+let+var n: int = step_stream(0, g1ofg0(s))+in+println!(tostring_int(n))+end++implement main0 (argc, argv) =+if argc > 1 then+count_files(argv[1])+else+count_files(".")
+ test/data/filecount.out view
@@ -0,0 +1,41 @@+#include "share/atspre_staload.hats"+#include "libats/ML/DATS/filebas_dirent.dats"+#include "libats/libc/DATS/dirent.dats"++staload "libats/ML/DATS/string.dats"++fun good_dir(next : string) : bool =+ case next of+ | "." => false+ | ".." => false+ | _ => true++fnx step_stream(acc : int, s : string) : int =+ if test_file_isdir(s) != 0 then+ flow_stream(s, acc + 1)+ else+ acc + 1+and flow_stream(s : string, init : int) : int =+ let+ var files = streamize_dirname_fname(s)+ var ffiles = stream_vt_filter_cloptr(files, lam x => good_dir(x))+ in+ stream_vt_foldleft_cloptr( ffiles+ , init+ , lam (acc, next) =>+ step_stream(acc, s + "/" + next)+ )+ end++fun count_files(s : string) : void =+ let+ var n: int = step_stream(0, g1ofg0(s))+ in+ println!(tostring_int(n))+ end++implement main0 (argc, argv) =+ if argc > 1 then+ count_files(argv[1])+ else+ count_files(".")
+ test/data/filetype.out view
@@ -0,0 +1,180 @@+// Type for a collection of files (monoidal)+typedef file = @{ lines = int, files = int }++// Type for the parsed command-line arguments. +typedef command_line = @{ version = bool+ , help = bool+ , table = bool+ , excludes = [m:nat] list(string, m)+ , includes = [m:nat] list(string, m)+ }++// Program state, tracking *all* supported file types in an unboxed structure.+typedef source_contents = @{ rust = file+ , haskell = file+ , ats = file+ , python = file+ , vimscript = file+ , elm = file+ , idris = file+ , madlang = file+ , tex = file+ , markdown = file+ , yaml = file+ , toml = file+ , cabal = file+ , happy = file+ , alex = file+ , go = file+ , html = file+ , css = file+ , verilog = file+ , vhdl = file+ , c = file+ , purescript = file+ , futhark = file+ , brainfuck = file+ , ruby = file+ , julia = file+ , perl = file+ , ocaml = file+ , agda = file+ , cobol = file+ , tcl = file+ , r = file+ , lua = file+ , cpp = file+ , lalrpop = file+ , header = file+ , sixten = file+ , dhall = file+ , ipkg = file+ , makefile = file+ , justfile = file+ , ion = file+ , bash = file+ , hamlet = file+ , cassius = file+ , lucius = file+ , julius = file+ , mercury = file+ , yacc = file+ , lex = file+ , coq = file+ , jupyter = file+ , java = file+ , scala = file+ , erlang = file+ , elixir = file+ , pony = file+ , clojure = file+ , cabal_project = file+ , assembly = file+ , nix = file+ , php = file+ , javascript = file+ , kotlin = file+ , fsharp = file+ , fortran = file+ , swift = file+ , csharp = file+ , nim = file+ , cpp_header = file+ , elisp = file+ , plaintext = file+ , rakefile = file+ , llvm = file+ , autoconf = file+ , batch = file+ , powershell = file+ , m4 = file+ , objective_c = file+ , automake = file+ }++// Reference to source_contents; used to update the structure.+vtypedef source_contents_r = ref(source_contents)++// Sum type representing all supported data types.+datavtype pl_type =+ | unknown+ | rust of int+ | haskell of int+ | perl of int+ | verilog of int+ | vhdl of int+ | agda of int+ | futhark of int+ | ats of int+ | idris of int+ | python of int+ | elm of int+ | purescript of int+ | vimscript of int+ | ocaml of int+ | madlang of int+ | tex of int+ | markdown of int+ | yaml of int+ | toml of int+ | cabal of int+ | happy of int+ | alex of int+ | go of int+ | html of int+ | css of int+ | c of int+ | brainfuck of int+ | ruby of int+ | julia of int+ | cobol of int+ | tcl of int+ | r of int+ | lua of int+ | cpp of int+ | lalrpop of int+ | header of int+ | sixten of int+ | dhall of int+ | ipkg of int+ | makefile of int+ | justfile of int+ | ion of int+ | bash of int+ | hamlet of int+ | cassius of int+ | lucius of int+ | julius of int+ | mercury of int+ | yacc of int+ | lex of int+ | coq of int+ | jupyter of int+ | java of int+ | scala of int+ | erlang of int+ | elixir of int+ | pony of int+ | clojure of int+ | cabal_project of int+ | assembly of int+ | nix of int+ | php of int+ | javascript of int+ | kotlin of int+ | fsharp of int+ | fortran of int+ | swift of int+ | csharp of int+ | nim of int+ | cpp_header of int+ | elisp of int+ | rakefile of int+ | plaintext of int+ | llvm of int+ | autoconf of int+ | batch of int+ | powershell of int+ | m4 of int+ | objective_c of int+ | automake of int
+ test/data/filetype.sats view
@@ -0,0 +1,180 @@+// Type for a collection of files (monoidal)+typedef file = @{ lines = int, files = int }++// Type for the parsed command-line arguments. +typedef command_line = @{ version = bool+, help = bool+, table = bool+, excludes = [ m : nat ] list(string, m)+, includes = [ m : nat ] list(string, m)+}++// Program state, tracking *all* supported file types in an unboxed structure.+typedef source_contents = @{ rust = file+, haskell = file+, ats = file+, python = file+, vimscript = file+, elm = file+, idris = file+, madlang = file+, tex = file+, markdown = file+, yaml = file+, toml = file+, cabal = file+, happy = file+, alex = file+, go = file+, html = file+, css = file+, verilog = file+, vhdl = file+, c = file+, purescript = file+, futhark = file+, brainfuck = file+, ruby = file+, julia = file+, perl = file+, ocaml = file+, agda = file+, cobol = file+, tcl = file+, r = file+, lua = file+, cpp = file+, lalrpop = file+, header = file+, sixten = file+, dhall = file+, ipkg = file+, makefile = file+, justfile = file+, ion = file+, bash = file+, hamlet = file+, cassius = file+, lucius = file+, julius = file+, mercury = file+, yacc = file+, lex = file+, coq = file+, jupyter = file+, java = file+, scala = file+, erlang = file+, elixir = file+, pony = file+, clojure = file+, cabal_project = file+, assembly = file+, nix = file+, php = file+, javascript = file+, kotlin = file+, fsharp = file+, fortran = file+, swift = file+, csharp = file+, nim = file+, cpp_header = file+, elisp = file+, plaintext = file+, rakefile = file+, llvm = file+, autoconf = file+, batch = file+, powershell = file+, m4 = file+, objective_c = file+, automake = file+}++// Reference to source_contents; used to update the structure.+vtypedef source_contents_r = ref(source_contents)++// Sum type representing all supported data types.+datavtype pl_type =+| unknown+| rust of int+| haskell of int+| perl of int+| verilog of int+| vhdl of int+| agda of int+| futhark of int+| ats of int+| idris of int+| python of int+| elm of int+| purescript of int+| vimscript of int+| ocaml of int+| madlang of int+| tex of int+| markdown of int+| yaml of int+| toml of int+| cabal of int+| happy of int+| alex of int+| go of int+| html of int+| css of int+| c of int+| brainfuck of int+| ruby of int+| julia of int+| cobol of int+| tcl of int+| r of int+| lua of int+| cpp of int+| lalrpop of int+| header of int+| sixten of int+| dhall of int+| ipkg of int+| makefile of int+| justfile of int+| ion of int+| bash of int+| hamlet of int+| cassius of int+| lucius of int+| julius of int+| mercury of int+| yacc of int+| lex of int+| coq of int+| jupyter of int+| java of int+| scala of int+| erlang of int+| elixir of int+| pony of int+| clojure of int+| cabal_project of int+| assembly of int+| nix of int+| php of int+| javascript of int+| kotlin of int+| fsharp of int+| fortran of int+| swift of int+| csharp of int+| nim of int+| cpp_header of int+| elisp of int+| rakefile of int+| plaintext of int+| llvm of int+| autoconf of int+| batch of int+| powershell of int+| m4 of int+| objective_c of int+| automake of int
+ test/data/left-pad.dats view
@@ -0,0 +1,98 @@+#include "share/atspre_staload.hats"++dataprop PAD(int,int,int) =+ | {p,l:nat} Yep(p,l,p-l)+ | {p,l:nat} Nope(p,l,0)++extern fun left_pad+ {p,l:nat | p>0 && l>0}+ (+ pad: ssize_t p,+ c: charNZ,+ s: strnptr l+ ): [cushion:nat] (PAD(p,l,cushion) | strnptr (cushion+l))++extern fun {t:t@ype} fill_list+ {n:nat}+ (+ size:ssize_t n,+ c: t+ ): list_vt(t,n)++implement {t}fill_list{n}(size,c) =+ let+ fun loop+ {i:nat | i <= n}+ .<i>.+ (+ size : ssize_t i,+ c: t,+ res: list_vt(t, n-i)+ ): list_vt(t,n) =+ if (size = i2ssz(0))+ then res+ else loop(pred size, c, list_vt_cons(c,res))+ in+ loop(size,c,list_vt_nil())+ end++implement left_pad{p,l}(pad,c,s) =+ let+ val size = strnptr_length(s)+ in+ if (pad > size)+ then+ let+ val padding = pad-size+ val char_list = fill_list(padding,c)+ val pad_string = string_make_list_vt(char_list)+ val res = strnptr_append(pad_string, s)+ in+ begin+ strnptr_free(pad_string);+ strnptr_free(s);+ (Yep{p,l} | res)+ end+ end+ else+ (Nope{p,l} | s)+ end++implement main0(argc, argv) =+ let+ val args = listize_argc_argv(argc,argv)+ val _ =+ if list_vt_length(args) = 3+ then (+ let+ val c = '0'+ val s = g1ofg0(args[1]) : [n:nat] string n+ val pad = g1ofg0(g0string2int(args[2]))+ in+ if length(s) > 0 && pad > 0+ then (+ let+ prval _ = lemma_not_empty(s) where {+ extern praxi+ lemma_not_empty{n:int}(x:string(n)):[n > 0] void+ }+ prval _ = lemma_not_zero(pad) where {+ extern praxi+ lemma_not_zero{n:int}(x:int(n)):[n > 0] void+ }+ val (pf | res) = left_pad(i2ssz(pad),c, string1_copy(s))+ in+ begin+ println! ("padding: ", res);+ strnptr_free(res);+ end+ end+ )+ else+ print "Usage: left-pad <string-to-pad> <pad-length>\n"+ end+ )+ else print "Usage: left-pad <string-to-pad> <pad-length>\n"+ in+ list_vt_free(args)+ end
+ test/data/left-pad.out view
@@ -0,0 +1,76 @@+#include "share/atspre_staload.hats"++dataprop PAD(int, int, int) =+ | { p, l : nat } Yep(p, l, p - l)+ | { p, l : nat } Nope(p, l, 0)++extern+fun left_pad { p, l : nat | p > 0 && l > 0 } ( pad : ssize_t(p)+ , c : charNZ+ , s : strnptr(l)+ ) : [cushion:nat] (PAD(p, l, cushion) | strnptr(cushion+l))++extern+fun {t:t@ype} fill_list {n:nat} (size : ssize_t(n), c : t) :+ list_vt(t, n)++implement {t} fill_list {n} (size, c) =+ let+ fun loop { i : nat | i <= n } .<i>. ( size : ssize_t(i)+ , c : t+ , res : list_vt(t, n-i)+ ) : list_vt(t, n) =+ if (size = i2ssz(0)) then+ res+ else+ loop(pred(size), c, list_vt_cons(c, res))+ in+ loop(size, c, list_vt_nil())+ end++implement left_pad { p, l } (pad, c, s) =+ let+ val size = strnptr_length(s)+ in+ if (pad > size) then+ let+ val padding = pad - size+ val char_list = fill_list(padding, c)+ val pad_string = string_make_list_vt(char_list)+ val res = strnptr_append(pad_string, s)+ in+ (strnptr_free(pad_string) ; strnptr_free(s) ; (Yep{p,l} | res))+ end+ else+ (Nope{p,l} | s)+ end++implement main0 (argc, argv) =+ let+ val args = listize_argc_argv(argc, argv)+ val _ = if list_vt_length(args) = 3 then+ (let+ val c = '0'+ val s = g1ofg0(args[1]) : [n:nat] string(n)+ val pad = g1ofg0(g0string2int(args[2]))+ in+ if length(s) > 0 && pad > 0 then+ (let+ prval _ = lemma_not_empty(s) where+ { extern+ praxi lemma_not_empty {n:int} (x : string(n)) : [ n > 0 ] void }+ prval _ = lemma_not_zero(pad) where+ { extern+ praxi lemma_not_zero {n:int} (x : int(n)) : [ n > 0 ] void }+ val (pf | res) = left_pad(i2ssz(pad), c, string1_copy(s))+ in+ (println!("padding: ", res) ; strnptr_free(res))+ end)+ else+ print("Usage: left-pad <string-to-pad> <pad-length>\n")+ end)+ else+ print("Usage: left-pad <string-to-pad> <pad-length>\n")+ in+ list_vt_free(args)+ end
+ test/data/number-theory.dats view
@@ -0,0 +1,167 @@+#include "share/atspre_staload.hats"+#include "ats-src/numerics.dats"+#include "contrib/atscntrb-hx-intinf/mylibies.hats"++staload UN = "prelude/SATS/unsafe.sats"+staload "contrib/atscntrb-hx-intinf/SATS/intinf_vt.sats"++#define ATS_MAINATSFLAG 1++// Existential types for even and odd numbers. These are only usable with the+// ATS library.+typedef Even = [ n : nat ] int(2 * n)++typedef Odd = [ n : nat ] int(2 * n+1)++// TODO jacobi symbol+// fn legendre(a: int, p: int) : int =+// a ^ (p - 1 / 2) % p+// m | n+fn divides(m : int, n : int) :<> bool =+ n % m = 0++fnx gcd {k : nat}{l : nat} (m : int(l), n : int(k)) : int =+ if n > 0 then+ gcd(n, witness(m % n))+ else+ m++fn lcm {k : nat}{l : nat} (m : int(l), n : int(k)) : int =+ (m / gcd(m, n)) * n++// stream all divisors of an integer.+fn divisors(n : intGte(1)) :<> stream_vt(int) =+ let+ fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> stream_vt(int) =+ if acc >= n then+ $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))+ else+ if n % acc = 0 then+ $ldelay(stream_vt_cons(n, loop(n, acc + 1)))+ else+ $ldelay(stream_vt_nil)+ in+ loop(n, 1)+ end++// stream all prime divisors of an integer (without multiplicity)+fn prime_divisors(n : intGte(1)) :<> stream_vt(int) =+ let+ fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> stream_vt(int) =+ if acc >= n then+ $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))+ else+ if n % acc = 0 && is_prime(n) then+ $ldelay(stream_vt_cons(n, loop(n, acc + 1)))+ else+ $ldelay(stream_vt_nil)+ in+ loop(n, 1)+ end++fn witness(n : int) : intGte(0) =+ $UN.cast(n)++propdef PRIME (p : int) = { x, y : nat | x <= y } MUL(x, y, p) -<> [ x == 1 ] void++dataprop FACT(int, int) =+ | FACTbas(0, 1)+ | {n : nat}{ r, r1 : int } FACTind(n + 1, r) of (FACT(n, r1), MUL(n + 1, r1, r))++fun get_multiplicity { p : nat | p > 1 } (n : intGte(0), p : int(p)) : int =+ case+ n % p of+ | 0 => 1 + get_multiplicity(witness(n / p), p)+ | _ => 0++fn count_divisors(n : intGte(1)) :<> int =+ let+ fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> int =+ if acc >= n then+ 1+ else+ if n % acc = 0 then+ 1 + loop(n, acc + 1)+ else+ loop(n, acc + 1)+ in+ loop(n, 1)+ end++fn sum_divisors(n : intGte(1)) :<> int =+ let+ fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> int =+ if acc >= n then+ 0+ else+ if n % acc = 0 then+ acc + loop(n, acc + 1)+ else+ loop(n, acc + 1)+ in+ loop(n, 1)+ end++fn is_perfect(n : intGte(1)) :<> bool =+ sum_divisors(n) = n++// distinct prime divisors+fn little_omega(n : intGte(1)) :<> int =+ let+ fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> int =+ if acc >= n then+ if is_prime(n) then+ 1+ else+ 0+ else+ if n % acc = 0 && is_prime(acc) then+ 1 + loop(n, acc + 1)+ else+ loop(n, acc + 1)+ in+ loop(n, 1)+ end++// Euler's totient function.+fn totient(n : intGte(1)) : int =+ case+ n of+ | 1 => 1+ | n =>> + begin+ let+ fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m } .<k-m>. (i : int(m), n : int(k)) : int =+ if i >= n then+ if is_prime(n) then+ n - 1+ else+ n+ else+ if n % i = 0 && is_prime(i) && i != n then+ (loop(i + 1, n) / i) * (i - 1)+ else+ loop(i + 1, n)+ in+ loop(1, n)+ end+ end++// TODO modular exponentiation+// The sum of all φ(m) for m between 1 and n +fun totient_sum(n : intGte(1)) : Intinf =+ let+ fnx loop { n : nat | n >= 1 }{ m : nat | m >= n } .<m-n>. (i : int(n), bound : int(m)) : Intinf =+ if i < bound then+ let+ val x = loop(i + 1, bound)+ val y = add_intinf0_int(x, witness(totient(i)))+ in+ y+ end+ else+ int2intinf(witness(totient(i)))+ in+ loop(1, n)+ end++extern+fun chinese_remainder {n : nat} (residues : list_vt(int, n), moduli : list_vt(int, n)) : Option_vt(int)
+ test/data/number-theory.out view
@@ -0,0 +1,186 @@+#include "share/atspre_staload.hats"+#include "ats-src/numerics.dats"+#include "contrib/atscntrb-hx-intinf/mylibies.hats"++staload UN = "prelude/SATS/unsafe.sats"+staload "contrib/atscntrb-hx-intinf/SATS/intinf_vt.sats"++#define ATS_MAINATSFLAG 1++// Existential types for even and odd numbers. These are only usable with the+// ATS library.+typedef Even = [n:nat] int(2*n)+typedef Odd = [n:nat] int(2*n+1)++// TODO jacobi symbol+// fn legendre(a: int, p: int) : int =+// a ^ (p - 1 / 2) % p+// m | n+fn divides(m : int, n : int) :<> bool =+ n % m = 0++fnx gcd {k:nat}{l:nat} (m : int(l), n : int(k)) : int =+ if n > 0 then+ gcd(n, witness(m % n))+ else+ m++fn lcm {k:nat}{l:nat} (m : int(l), n : int(k)) : int =+ (m / gcd(m, n)) * n++// stream all divisors of an integer.+fn divisors(n : intGte(1)) :<> stream_vt(int) =+ let+ fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)+ , acc : int(m)+ ) :<> stream_vt(int) =+ if acc >= n then+ $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))+ else+ if n % acc = 0 then+ $ldelay(stream_vt_cons(n, loop(n, acc + 1)))+ else+ $ldelay(stream_vt_nil)+ in+ loop(n, 1)+ end++// stream all prime divisors of an integer (without multiplicity)+fn prime_divisors(n : intGte(1)) :<> stream_vt(int) =+ let+ fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)+ , acc : int(m)+ ) :<> stream_vt(int) =+ if acc >= n then+ $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))+ else+ if n % acc = 0 && is_prime(n) then+ $ldelay(stream_vt_cons(n, loop(n, acc + 1)))+ else+ $ldelay(stream_vt_nil)+ in+ loop(n, 1)+ end++fn witness(n : int) : intGte(0) =+ $UN.cast(n)++propdef PRIME (p : int) =+{ x, y : nat | x <= y } MUL(x, y, p) -<> [ x == 1 ] void++dataprop FACT(int, int) =+ | FACTbas(0, 1)+ | { r, r1 : int }{n:nat} FACTind(n + 1, r) of (FACT(n, r1), MUL( n + 1+ , r1+ , r+ ))++fun get_multiplicity { p : nat | p > 1 } (n : intGte(0), p : int(p)) :+ int =+ case+ n % p of+ | 0 => 1 + get_multiplicity(witness(n / p), p)+ | _ => 0++fn count_divisors(n : intGte(1)) :<> int =+ let+ fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)+ , acc : int(m)+ ) :<> int =+ if acc >= n then+ 1+ else+ if n % acc = 0 then+ 1 + loop(n, acc + 1)+ else+ loop(n, acc + 1)+ in+ loop(n, 1)+ end++fn sum_divisors(n : intGte(1)) :<> int =+ let+ fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)+ , acc : int(m)+ ) :<> int =+ if acc >= n then+ 0+ else+ if n % acc = 0 then+ acc + loop(n, acc + 1)+ else+ loop(n, acc + 1)+ in+ loop(n, 1)+ end++fn is_perfect(n : intGte(1)) :<> bool =+ sum_divisors(n) = n++// distinct prime divisors+fn little_omega(n : intGte(1)) :<> int =+ let+ fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)+ , acc : int(m)+ ) :<> int =+ if acc >= n then+ if is_prime(n) then+ 1+ else+ 0+ else+ if n % acc = 0 && is_prime(acc) then+ 1 + loop(n, acc + 1)+ else+ loop(n, acc + 1)+ in+ loop(n, 1)+ end++// Euler's totient function.+fn totient(n : intGte(1)) : int =+ case+ n of+ | 1 => 1+ | n =>> + begin+ let+ fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m } .<k-m>.+ (i : int(m), n : int(k)) : int =+ if i >= n then+ if is_prime(n) then+ n - 1+ else+ n+ else+ if n % i = 0 && is_prime(i) && i != n then+ (loop(i + 1, n) / i) * (i - 1)+ else+ loop(i + 1, n)+ in+ loop(1, n)+ end+ end++// TODO modular exponentiation+// The sum of all φ(m) for m between 1 and n +fun totient_sum(n : intGte(1)) : Intinf =+ let+ fnx loop { n : nat | n >= 1 }{ m : nat | m >= n } .<m-n>. ( i : int(n)+ , bound : int(m)+ ) : Intinf =+ if i < bound then+ let+ val x = loop(i + 1, bound)+ val y = add_intinf0_int(x, witness(totient(i)))+ in+ y+ end+ else+ int2intinf(witness(totient(i)))+ in+ loop(1, n)+ end++extern+fun chinese_remainder {n:nat} ( residues : list_vt(int, n)+ , moduli : list_vt(int, n)+ ) : Option_vt(int)
+ test/data/numerics.dats view
@@ -0,0 +1,61 @@+#define ATS_MAINATSFLAG 1++#include "share/atspre_staload.hats"++staload "libats/libc/SATS/math.sats"+staload UN = "prelude/SATS/unsafe.sats"++fun exp {n : nat} .<n>. (x : int, n : int(n)) :<> int =+ case+ x of+ | 0 => 0+ | x => + begin+ if n > 0 then+ let+ val n2 = half(n)+ val i2 = n % 2+ in+ if i2 = 0 then+ exp(x * x, n2)+ else+ x * exp(x * x, n2)+ end+ else+ 1+ end++castfn lemma_bounded(i: int) : [n:nat] int(n)+ = $UN.cast(i)++fun sqrt_bad(k : intGt(0)) : [ m : nat ] int(m) =+ let+ var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))+ var bound: [m:nat] int(m) = lemma_bounded(pre_bound)+ in+ bound+ end++fn is_prime(k : intGt(0)) : bool =+ case+ k of+ | 1 => false+ | k => + begin+ let+ fun loop {n : nat}{m : nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<> bool =+ if i < bound then+ if k % i = 0 then+ false+ else+ loop(i + 1, bound)+ else+ if i = bound then+ if k % i = 0 then+ false+ else+ true+ else+ true+ in+ loop(2, sqrt_bad(k))+ end+ end
+ test/data/numerics.out view
@@ -0,0 +1,63 @@+#define ATS_MAINATSFLAG 1++#include "share/atspre_staload.hats"++staload "libats/libc/SATS/math.sats"+staload UN = "prelude/SATS/unsafe.sats"++fun exp {n:nat} .<n>. (x : int, n : int(n)) :<> int =+ case+ x of+ | 0 => 0+ | x => + begin+ if n > 0 then+ let+ val n2 = half(n)+ val i2 = n % 2+ in+ if i2 = 0 then+ exp(x * x, n2)+ else+ x * exp(x * x, n2)+ end+ else+ 1+ end++castfn lemma_bounded(i : int) : [n:nat] int(n) =+ $UN.cast(i)++fun sqrt_bad(k : intGt(0)) : [m:nat] int(m) =+ let+ var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))+ var bound: [m:nat] int(m) = lemma_bounded(pre_bound)+ in+ bound+ end++fn is_prime(k : intGt(0)) : bool =+ case+ k of+ | 1 => false+ | k => + begin+ let+ fun loop {n:nat}{m:nat} .<max(0,m-n)>. ( i : int(n)+ , bound : int(m)+ ) :<> bool =+ if i < bound then+ if k % i = 0 then+ false+ else+ loop(i + 1, bound)+ else+ if i = bound then+ if k % i = 0 then+ false+ else+ true+ else+ true+ in+ loop(2, sqrt_bad(k))+ end+ end
+ test/data/polyglot.dats view
@@ -0,0 +1,1235 @@+#include "share/atspre_staload.hats"+#include "share/HATS/atslib_staload_libats_libc.hats"+#include "prelude/DATS/filebas.dats"+#include "libats/ML/DATS/filebas_dirent.dats"+#include "libats/libc/DATS/dirent.dats"+#include "src/concurrency.dats"+#include "libats/DATS/athread_posix.dats"+#include "prelude/DATS/stream_vt.dats"++%{^+#include "libats/libc/CATS/string.cats"+#include "prelude/CATS/filebas.cats"+%}++staload "prelude/SATS/stream_vt.sats"+staload "libats/ML/DATS/list0.dats"+staload "libats/SATS/athread.sats"+staload "libats/ML/DATS/string.dats"+staload "libats/libc/SATS/stdio.sats"+staload "prelude/SATS/filebas.sats"+staload "src/filetype.sats"+staload "libats/ML/DATS/filebas.dats"+staload EXTRA = "libats/ML/SATS/filebas.sats"+staload "libats/libc/SATS/unistd.sats"+staload "libats/DATS/athread.dats"++fun to_file(s : string, pre : Option(string)) : file =+ let+ val is_comment = case+ pre of+ | Some (x) => string_is_prefix(x, s)+ | None => false+ in+ if s = "" then+ @{ lines = 1, blanks = 1, comments = 0, files = 0 }+ else+ if is_comment then+ @{ lines = 1, blanks = 0, comments = 1, files = 0 }+ else+ @{ lines = 1, blanks = 0, comments = 0, files = 0 }+ end++fun empty_file() : file =+ let+ var f = @{ files = 0, blanks = 0, comments = 0, lines = 0 } : file+ in+ f+ end++fun acc_file() : file =+ let+ var f = @{ files = 1, blanks = 0, comments = 0, lines = ~1 } : file+ in+ f+ end++// monoidal addition for 'file' type+fun add_results(x : file, y : file) : file =+ let+ var next = @{ lines = x.lines + y.lines, blanks = x.blanks + y.blanks, comments = x.comments+ + y.comments, files = x.files + y.files }+ in+ next+ end++overload + with add_results++// Given a string representing a filepath, return an integer.+fun line_count(s : string, pre : Option(string)) : file =+ let+ var ref = fileref_open_opt(s, file_mode_r)+ in+ case ref of+ | ~Some_vt (x) => + begin+ let+ var viewstream: stream_vt(string) = $EXTRA.streamize_fileref_line(x)+ val n: file = stream_vt_foldleft_cloptr( viewstream+ , acc_file()+ , lam (acc, f) =<cloptr1> acc + to_file(f, pre)+ )+ val _ = fileref_close(x)+ in+ n+ end+ end+ | ~None_vt() => (println!("\33[33mWarning:\33[0m could not open file at " + s) ; to_file( s+ , None+ ))+ end++// Pad a string of bounded length on the right by adding spaces.+fnx right_pad { k : int | k >= 0 }{ m : int | m <= k } .<k>. (s : string(m), n : int(k)) :+string =+ case+ length(s) < n of+ | true when n > 0 => right_pad(s, n - 1) + " "+ | _ => s++// Pad a string on the left by adding spaces.+fnx left_pad { k : int | k >= 0 } .<k>. (s : string, n : int(k)) : string =+ case+ length(s) < n of+ | true when n > 0 => " " + left_pad(s, n - 1)+ | _ => s++// helper function for make_output+fun maybe_string(s : string, n : int) : string =+ if n > 0 then+ s + ": " + tostring_int(n) + "\n"+ else+ ""++// helper function for make_table+fun maybe_table { k : int | k >= 0 && k < 20 } (s : string(k), f : file) : string =+ let+ var code = f.lines - f.comments - f.blanks+ in+ if f.files > 0 then+ " " + right_pad(s, 21) + left_pad(tostring_int(f.files), 5) + left_pad(tostring_int(f.lines+ ), 12)+ + left_pad(tostring_int(code), 13) + left_pad(tostring_int(f.comments), 13)+ + left_pad(tostring_int(f.blanks), 13) + "\n"+ else+ ""+ end++// helper function for make_output+fun with_nonempty(s1 : string, s2 : string) : string =+ if s2 != "" then+ s1 + s2+ else+ ""++// helper function to make totals for tabular output.+fun sum_fields(sc : source_contents) : file =+ let+ var f = @{ lines = sc.rust.lines + sc.haskell.lines + sc.ats.lines + sc.python.lines+ + sc.vimscript.lines + sc.elm.lines + sc.idris.lines + sc.madlang.lines + sc.tex.lines+ + sc.markdown.lines + sc.yaml.lines + sc.toml.lines + sc.cabal.lines + sc.happy.lines+ + sc.alex.lines + sc.go.lines + sc.html.lines + sc.css.lines + sc.verilog.lines + sc.vhdl.lines+ + sc.c.lines + sc.purescript.lines + sc.futhark.lines + sc.brainfuck.lines + sc.ruby.lines+ + sc.julia.lines + sc.perl.lines + sc.ocaml.lines + sc.agda.lines + sc.cobol.lines+ + sc.tcl.lines + sc.r.lines + sc.lua.lines + sc.cpp.lines + sc.lalrpop.lines + sc.header.lines+ + sc.sixten.lines + sc.dhall.lines + sc.ipkg.lines + sc.makefile.lines + sc.justfile.lines+ + sc.ion.lines + sc.bash.lines + sc.hamlet.lines + sc.cassius.lines + sc.lucius.lines+ + sc.julius.lines + sc.mercury.lines + sc.yacc.lines + sc.lex.lines + sc.coq.lines+ + sc.jupyter.lines + sc.java.lines + sc.scala.lines + sc.erlang.lines + sc.elixir.lines+ + sc.pony.lines + sc.clojure.lines + sc.cabal_project.lines + sc.assembly.lines + sc.nix.lines+ + sc.php.lines + sc.javascript.lines + sc.kotlin.lines + sc.fsharp.lines + sc.fortran.lines+ + sc.swift.lines + sc.csharp.lines + sc.nim.lines + sc.cpp_header.lines + sc.elisp.lines+ + sc.plaintext.lines + sc.rakefile.lines + sc.llvm.lines + sc.autoconf.lines + sc.batch.lines+ + sc.powershell.lines + sc.m4.lines + sc.objective_c.lines+ + sc.automake.lines, blanks = sc.rust.blanks + sc.haskell.blanks + sc.ats.blanks+ + sc.python.blanks + sc.vimscript.blanks + sc.elm.blanks + sc.idris.blanks + sc.madlang.blanks+ + sc.tex.blanks + sc.markdown.blanks + sc.yaml.blanks + sc.toml.blanks + sc.cabal.blanks+ + sc.happy.blanks + sc.alex.blanks + sc.go.blanks + sc.html.blanks + sc.css.blanks+ + sc.verilog.blanks + sc.vhdl.blanks + sc.c.blanks + sc.purescript.blanks + sc.futhark.blanks+ + sc.brainfuck.blanks + sc.ruby.blanks + sc.julia.blanks + sc.perl.blanks + sc.ocaml.blanks+ + sc.agda.blanks + sc.cobol.blanks + sc.tcl.blanks + sc.r.blanks + sc.lua.blanks + sc.cpp.blanks+ + sc.lalrpop.blanks + sc.header.blanks + sc.sixten.blanks + sc.dhall.blanks + sc.ipkg.blanks+ + sc.makefile.blanks + sc.justfile.blanks + sc.ion.blanks + sc.bash.blanks + sc.hamlet.blanks+ + sc.cassius.blanks + sc.lucius.blanks + sc.julius.blanks + sc.mercury.blanks + sc.yacc.blanks+ + sc.lex.blanks + sc.coq.blanks + sc.jupyter.blanks + sc.java.blanks + sc.scala.blanks+ + sc.erlang.blanks + sc.elixir.blanks + sc.pony.blanks + sc.clojure.blanks+ + sc.cabal_project.blanks + sc.assembly.blanks + sc.nix.blanks + sc.php.blanks+ + sc.javascript.blanks + sc.kotlin.blanks + sc.fsharp.blanks + sc.fortran.blanks+ + sc.swift.blanks + sc.csharp.blanks + sc.nim.blanks + sc.cpp_header.blanks + sc.elisp.blanks+ + sc.plaintext.blanks + sc.rakefile.blanks + sc.llvm.blanks + sc.autoconf.blanks+ + sc.batch.blanks + sc.powershell.blanks + sc.m4.blanks + sc.objective_c.blanks+ + sc.automake.blanks, comments = sc.rust.comments + sc.haskell.comments + sc.ats.comments+ + sc.python.comments + sc.vimscript.comments + sc.elm.comments + sc.idris.comments+ + sc.madlang.comments + sc.tex.comments + sc.markdown.comments + sc.yaml.comments+ + sc.toml.comments + sc.cabal.comments + sc.happy.comments + sc.alex.comments + sc.go.comments+ + sc.html.comments + sc.css.comments + sc.verilog.comments + sc.vhdl.comments + sc.c.comments+ + sc.purescript.comments + sc.futhark.comments + sc.brainfuck.comments + sc.ruby.comments+ + sc.julia.comments + sc.perl.comments + sc.ocaml.comments + sc.agda.comments+ + sc.cobol.comments + sc.tcl.comments + sc.r.comments + sc.lua.comments + sc.cpp.comments+ + sc.lalrpop.comments + sc.header.comments + sc.sixten.comments + sc.dhall.comments+ + sc.ipkg.comments + sc.makefile.comments + sc.justfile.comments + sc.ion.comments+ + sc.bash.comments + sc.hamlet.comments + sc.cassius.comments + sc.lucius.comments+ + sc.julius.comments + sc.mercury.comments + sc.yacc.comments + sc.lex.comments+ + sc.coq.comments + sc.jupyter.comments + sc.java.comments + sc.scala.comments+ + sc.erlang.comments + sc.elixir.comments + sc.pony.comments + sc.clojure.comments+ + sc.cabal_project.comments + sc.assembly.comments + sc.nix.comments + sc.php.comments+ + sc.javascript.comments + sc.kotlin.comments + sc.fsharp.comments + sc.fortran.comments+ + sc.swift.comments + sc.csharp.comments + sc.nim.comments + sc.cpp_header.comments+ + sc.elisp.comments + sc.plaintext.comments + sc.rakefile.comments + sc.llvm.comments+ + sc.autoconf.comments + sc.batch.comments + sc.powershell.comments + sc.m4.comments+ + sc.objective_c.comments + sc.automake.comments, files = sc.rust.files + sc.haskell.files+ + sc.ats.files + sc.python.files + sc.vimscript.files + sc.elm.files + sc.idris.files+ + sc.madlang.files + sc.tex.files + sc.markdown.files + sc.yaml.files + sc.toml.files+ + sc.cabal.files + sc.happy.files + sc.alex.files + sc.go.files + sc.html.files + sc.css.files+ + sc.verilog.files + sc.vhdl.files + sc.c.files + sc.purescript.files + sc.futhark.files+ + sc.brainfuck.files + sc.ruby.files + sc.julia.files + sc.perl.files + sc.ocaml.files+ + sc.agda.files + sc.cobol.files + sc.tcl.files + sc.r.files + sc.lua.files + sc.cpp.files+ + sc.lalrpop.files + sc.header.files + sc.sixten.files + sc.dhall.files + sc.ipkg.files+ + sc.makefile.files + sc.justfile.files + sc.ion.files + sc.bash.files + sc.hamlet.files+ + sc.cassius.files + sc.lucius.files + sc.julius.files + sc.mercury.files + sc.yacc.files+ + sc.lex.files + sc.coq.files + sc.jupyter.files + sc.java.files + sc.scala.files+ + sc.erlang.files + sc.elixir.files + sc.pony.files + sc.clojure.files + sc.cabal_project.files+ + sc.assembly.files + sc.nix.files + sc.php.files + sc.javascript.files + sc.kotlin.files+ + sc.fsharp.files + sc.fortran.files + sc.swift.files + sc.csharp.files + sc.nim.files+ + sc.cpp_header.files + sc.elisp.files + sc.plaintext.files + sc.rakefile.files + sc.llvm.files+ + sc.autoconf.files + sc.batch.files + sc.powershell.files + sc.m4.files + sc.objective_c.files+ + sc.automake.files }+ in+ f+ end++// function to print tabular output at the end+fun make_table(isc : source_contents) : string =+ "-------------------------------------------------------------------------------\n \33[35mLanguage\33[0m \33[35mFiles\33[0m \33[35mLines\33[0m \33[35mCode\33[0m \33[35mComments\33[0m \33[35mBlanks\33[0m\n-------------------------------------------------------------------------------\n"+ + maybe_table("Alex", isc.alex) + maybe_table("Agda", isc.agda) + maybe_table( "Assembly"+ , isc.assembly+ ) + maybe_table("ATS", isc.ats)+ + maybe_table("Autoconf", isc.autoconf) + maybe_table("Automake", isc.automake)+ + maybe_table("Bash", isc.bash) + maybe_table("Batch", isc.batch) + maybe_table( "Brainfuck"+ , isc.brainfuck+ ) + maybe_table("C", isc.c)+ + maybe_table("C Header", isc.header) + maybe_table("C++ cpp_header", isc.cpp_header)+ + maybe_table("C++", isc.cpp) + maybe_table("C#", isc.csharp) + maybe_table("Cabal", isc.cabal)+ + maybe_table("Cabal Project", isc.cabal_project) + maybe_table("Cassius", isc.cassius)+ + maybe_table("COBOL", isc.cobol) + maybe_table("Coq", isc.coq) + maybe_table("CSS", isc.css)+ + maybe_table("Dhall", isc.dhall) + maybe_table("Elixir", isc.elixir) + maybe_table( "Elm"+ , isc.elm+ ) + maybe_table( "Emacs Lisp"+ , isc.elisp+ )+ + maybe_table("Erlang", isc.erlang) + maybe_table("F#", isc.fsharp) + maybe_table( "Fortran"+ , isc.fortran+ ) + maybe_table("Go", isc.go)+ + maybe_table("Hamlet", isc.hamlet) + maybe_table("Happy", isc.happy) + maybe_table( "Haskell"+ , isc.haskell+ ) + maybe_table("HTML", isc.html)+ + maybe_table("Idris", isc.idris) + maybe_table("iPKG", isc.ipkg) + maybe_table("Ion", isc.ion)+ + maybe_table("Java", isc.java) + maybe_table("JavaScript", isc.javascript)+ + maybe_table("Julius", isc.julius) + maybe_table("Julia", isc.julia) + maybe_table( "Jupyter"+ , isc.jupyter+ ) + maybe_table( "Justfile"+ , isc.justfile+ )+ + maybe_table("Kotlin", isc.kotlin) + maybe_table("LALRPOP", isc.lalrpop) + maybe_table( "Lex"+ , isc.lex+ ) + maybe_table( "LLVM"+ , isc.llvm+ )+ + maybe_table("Lua", isc.lua) + maybe_table("Lucius", isc.lucius) + maybe_table("M4", isc.m4)+ + maybe_table("Madlang", isc.madlang) + maybe_table("Makefile", isc.makefile)+ + maybe_table("Margaret", isc.margaret) + maybe_table("Markdown", isc.markdown)+ + maybe_table("Mercury", isc.mercury) + maybe_table("Nim", isc.nim) + maybe_table( "Nix"+ , isc.nix+ ) + maybe_table( "Objective C"+ , isc.objective_c+ )+ + maybe_table("OCaml", isc.ocaml) + maybe_table("Perl", isc.perl) + maybe_table("PHP", isc.php)+ + maybe_table("Plaintext", isc.plaintext) + maybe_table("PowerShell", isc.powershell)+ + maybe_table("Pony", isc.pony) + maybe_table("Python", isc.python) + maybe_table( "PureScript"+ , isc.purescript+ ) + maybe_table("R", isc.r)+ + maybe_table("Rakefile", isc.rakefile) + maybe_table("Ruby", isc.ruby) + maybe_table( "Rust"+ , isc.rust+ ) + maybe_table( "Scala"+ , isc.scala+ )+ + maybe_table("Sixten", isc.sixten) + maybe_table("Swift", isc.swift) + maybe_table( "TCL"+ , isc.tcl+ ) + maybe_table("TeX", isc.tex)+ + maybe_table("TOML", isc.toml) + maybe_table("Verilog", isc.verilog) + maybe_table( "VHDL"+ , isc.vhdl+ ) + maybe_table( "Vimscript"+ , isc.vimscript+ )+ + maybe_table("Yacc", isc.yacc) + maybe_table("YAML", isc.yaml)+ + "-------------------------------------------------------------------------------\n"+ + maybe_table("Total", sum_fields(isc))+ + "-------------------------------------------------------------------------------\n"++// Function to print output sorted by type of language.+fun make_output(isc : source_contents) : string =+ with_nonempty( "\33[33mProgramming Languages:\33[0m\n"+ , maybe_string("Agda", isc.agda.lines) + maybe_string("Assembly", isc.assembly.lines)+ + maybe_string("ATS", isc.ats.lines) + maybe_string("Brainfuck", isc.brainfuck.lines)+ + maybe_string("C", isc.c.lines) + maybe_string("C Header", isc.header.lines)+ + maybe_string("C++", isc.cpp.lines) + maybe_string("C++ Header", isc.cpp_header.lines)+ + maybe_string("C#", isc.csharp.lines) + maybe_string("COBOL", isc.cobol.lines)+ + maybe_string("Coq", isc.coq.lines) + maybe_string("Elixir", isc.elixir.lines)+ + maybe_string("Elm", isc.elm.lines) + maybe_string("Erlang", isc.erlang.lines)+ + maybe_string("F#", isc.fsharp.lines) + maybe_string("Fortran", isc.fortran.lines)+ + maybe_string("Go", isc.go.lines) + maybe_string("Haskell", isc.haskell.lines)+ + maybe_string("Idris", isc.idris.lines) + maybe_string("Kotline", isc.kotlin.lines)+ + maybe_string("Java", isc.java.lines) + maybe_string("Julia", isc.julia.lines)+ + maybe_string("Lua", isc.lua.lines) + maybe_string("Margaret", isc.margaret.lines)+ + maybe_string("Mercury", isc.mercury.lines) + maybe_string("Nim", isc.nim.lines)+ + maybe_string("Objective C", isc.objective_c.lines) + maybe_string("OCaml", isc.ocaml.lines)+ + maybe_string("Perl", isc.perl.lines) + maybe_string("Pony", isc.pony.lines)+ + maybe_string("PureScript", isc.purescript.lines) + maybe_string("Python", isc.python.lines)+ + maybe_string("R", isc.r.lines) + maybe_string("Ruby", isc.ruby.lines) + maybe_string( "Rust"+ , isc.rust.lines+ )+ + maybe_string("Scala", isc.scala.lines) + maybe_string("Sixten", isc.sixten.lines)+ + maybe_string("Swift", isc.swift.lines) + maybe_string("TCL", isc.tcl.lines)+ ) + with_nonempty( "\n\33[33mEditor Plugins:\33[0m\n"+ , maybe_string("Emacs Lisp", isc.elisp.lines) + maybe_string( "Vimscript"+ , isc.vimscript.lines+ )+ ) + with_nonempty( "\n\33[33mDocumentation:\33[0m\n"+ , maybe_string("Markdown", isc.markdown.lines)+ + maybe_string("Plaintext", isc.plaintext.lines) + maybe_string( "TeX"+ , isc.tex.lines+ )+ ) + with_nonempty( "\n\33[33mConfiguration:\33[0m\n"+ , maybe_string("Cabal", isc.cabal.lines)+ + maybe_string( "Cabal Project"+ , isc.cabal_project.lines+ ) + maybe_string( "Dhall"+ , isc.dhall.lines+ ) + maybe_string( "iPKG"+ , isc.ipkg.lines+ )+ + maybe_string("TOML", isc.toml.lines)+ + maybe_string("YAML", isc.yaml.lines)+ ) + with_nonempty( "\n\33[33mShell:\33[0m\n"+ , maybe_string( "Bash"+ , isc.bash.lines+ )+ + maybe_string( "Batch"+ , isc.batch.lines+ ) + maybe_string( "Ion"+ , isc.ion.lines+ )+ + maybe_string( "PowerShell"+ , isc.powershell.lines+ )+ )+ + with_nonempty( "\n\33[33mParser Generators:\33[0m\n"+ , maybe_string("Alex", isc.alex.lines) + maybe_string("Happy", isc.happy.lines)+ + maybe_string("LALRPOP", isc.lalrpop.lines) + maybe_string("Lex", isc.lex.lines)+ + maybe_string("Yacc", isc.yacc.lines)+ ) + with_nonempty( "\n\33[33mWeb:\33[0m\n"+ , maybe_string("Cassius", isc.cassius.lines) + maybe_string("CSS", isc.css.lines)+ + maybe_string("Hamlet", isc.hamlet.lines) + maybe_string("HTML", isc.html.lines)+ + maybe_string("JavaScript", isc.javascript.lines) + maybe_string( "Julius"+ , isc.julius.lines+ )+ + maybe_string("Lucius", isc.lucius.lines)+ ) + with_nonempty( "\n\33[33mHardware:\33[0m\n"+ , maybe_string("Verilog", isc.verilog.lines) + maybe_string( "VHDL"+ , isc.vhdl.lines+ )+ ) + with_nonempty( "\n\33[33mNotebooks:\33[0m\n"+ , maybe_string("Jupyter", isc.jupyter.lines)+ ) + with_nonempty( "\n\33[33mOther:\33[0m\n"+ , maybe_string( "Autoconf"+ , isc.autoconf.lines+ )+ + maybe_string( "Automake"+ , isc.automake.lines+ )+ + maybe_string( "Justfile"+ , isc.justfile.lines+ )+ + maybe_string( "LLVM"+ , isc.llvm.lines+ )+ + maybe_string("M4", isc.m4.lines)+ + maybe_string( "Madlang"+ , isc.madlang.lines+ )+ + maybe_string( "Makefile"+ , isc.makefile.lines+ )+ + maybe_string( "Rakefile"+ , isc.rakefile.lines+ )+ )++fun add_contents(x : source_contents, y : source_contents) : source_contents =+ let+ var next = @{ rust = x.rust + y.rust, haskell = x.haskell + y.haskell, ats = x.ats+ + y.ats, python = x.python + y.python, vimscript = x.vimscript + y.vimscript, elm = x.elm+ + y.elm, idris = x.idris + y.idris, madlang = x.madlang + y.madlang, tex = x.tex+ + y.tex, markdown = x.markdown + y.markdown, yaml = x.yaml + y.yaml, toml = x.toml+ + y.toml, cabal = x.cabal + y.cabal, happy = x.happy + y.happy, alex = x.alex+ + y.alex, go = x.go + y.go, html = x.html + y.html, css = x.css + y.css, verilog = x.verilog+ + y.verilog, vhdl = x.vhdl + y.vhdl, c = x.c + y.c, purescript = x.purescript+ + y.purescript, futhark = x.futhark + y.futhark, brainfuck = x.brainfuck+ + y.brainfuck, ruby = x.ruby + y.ruby, julia = x.julia + y.julia, perl = x.perl+ + y.perl, ocaml = x.ocaml + y.ocaml, agda = x.agda + y.agda, cobol = x.cobol+ + y.cobol, tcl = x.tcl + y.tcl, r = x.r + y.r, lua = x.lua + y.lua, cpp = x.cpp+ + y.cpp, lalrpop = x.lalrpop + y.lalrpop, header = x.header + y.header, sixten = x.sixten+ + y.sixten, dhall = x.dhall + y.dhall, ipkg = x.ipkg + y.ipkg, makefile = x.makefile+ + y.makefile, justfile = x.justfile + y.justfile, ion = x.ion + y.ion, bash = x.bash+ + y.bash, hamlet = x.hamlet + y.hamlet, cassius = x.cassius + y.cassius, lucius = x.lucius+ + y.lucius, julius = x.julius + y.julius, mercury = x.mercury + y.mercury, yacc = x.yacc+ + y.yacc, lex = x.lex + y.lex, coq = x.coq + y.coq, jupyter = x.jupyter+ + y.jupyter, java = x.java + y.java, scala = x.scala + y.scala, erlang = x.erlang+ + y.erlang, elixir = x.elixir + y.elixir, pony = x.pony + y.pony, clojure = x.clojure+ + y.clojure, cabal_project = x.cabal_project + y.cabal_project, assembly = x.assembly+ + y.assembly, nix = x.nix + y.nix, php = x.php + y.php, javascript = x.javascript+ + y.javascript, kotlin = x.kotlin + y.kotlin, fsharp = x.fsharp + y.fsharp, fortran = x.fortran+ + y.fortran, swift = x.swift + y.swift, csharp = x.csharp + y.csharp, nim = x.nim+ + y.nim, cpp_header = x.cpp_header + y.cpp_header, elisp = x.elisp+ + y.elisp, plaintext = x.plaintext + y.plaintext, rakefile = x.rakefile+ + y.rakefile, llvm = x.llvm + y.llvm, autoconf = x.autoconf + y.autoconf, batch = x.batch+ + y.batch, powershell = x.powershell + y.powershell, m4 = x.m4+ + y.m4, objective_c = x.objective_c + y.objective_c, automake = x.automake+ + y.automake, margaret = x.margaret + y.margaret } : source_contents+ in+ next+ end++// This is the step function used when streaming directory contents. +fun adjust_contents(prev : source_contents, scf : pl_type) : source_contents =+ let+ val sc_r = ref<source_contents>(prev)+ val _ = case+ scf of+ | ~haskell n => sc_r->haskell := prev.haskell + n+ | ~ats n => sc_r->ats := prev.ats + n+ | ~rust n => sc_r->rust := prev.rust + n+ | ~markdown n => sc_r->markdown := prev.markdown + n+ | ~python n => sc_r->python := prev.python + n+ | ~vimscript n => sc_r->vimscript := prev.vimscript + n+ | ~yaml n => sc_r->yaml := prev.yaml + n+ | ~toml n => sc_r->toml := prev.toml + n+ | ~happy n => sc_r->happy := prev.happy + n+ | ~alex n => sc_r->alex := prev.alex + n+ | ~idris n => sc_r->idris := prev.idris + n+ | ~madlang n => sc_r->madlang := prev.madlang + n+ | ~elm n => sc_r->elm := prev.elm + n+ | ~c n => sc_r->c := prev.c + n+ | ~go n => sc_r->go := prev.go + n+ | ~cabal n => sc_r->cabal := prev.cabal + n+ | ~verilog n => sc_r->verilog := prev.verilog + n+ | ~vhdl n => sc_r->vhdl := prev.vhdl + n+ | ~html n => sc_r->html := prev.html + n+ | ~css n => sc_r->css := prev.css + n+ | ~purescript n => sc_r->purescript := prev.purescript + n+ | ~futhark n => sc_r->futhark := prev.futhark + n+ | ~brainfuck n => sc_r->brainfuck := prev.brainfuck + n+ | ~ruby n => sc_r->ruby := prev.ruby + n+ | ~julia n => sc_r->julia := prev.julia + n+ | ~tex n => sc_r->tex := prev.tex + n+ | ~perl n => sc_r->perl := prev.perl + n+ | ~ocaml n => sc_r->ocaml := prev.ocaml + n+ | ~agda n => sc_r->agda := prev.agda + n+ | ~cobol n => sc_r->cobol := prev.cobol + n+ | ~tcl n => sc_r->tcl := prev.tcl + n+ | ~r n => sc_r->r := prev.r + n+ | ~lua n => sc_r->lua := prev.lua + n+ | ~cpp n => sc_r->cpp := prev.cpp + n+ | ~lalrpop n => sc_r->lalrpop := prev.lalrpop + n+ | ~header n => sc_r->header := prev.header + n+ | ~sixten n => sc_r->sixten := prev.sixten + n+ | ~dhall n => sc_r->dhall := prev.dhall + n+ | ~ipkg n => sc_r->ipkg := prev.ipkg + n+ | ~justfile n => sc_r->justfile := prev.justfile + n+ | ~makefile n => sc_r->makefile := prev.makefile + n+ | ~ion n => sc_r->ion := prev.ion + n+ | ~bash n => sc_r->bash := prev.bash + n+ | ~hamlet n => sc_r->hamlet := prev.hamlet + n+ | ~cassius n => sc_r->cassius := prev.cassius + n+ | ~lucius n => sc_r->lucius := prev.lucius + n+ | ~julius n => sc_r->julius := prev.julius + n+ | ~mercury n => sc_r->mercury := prev.mercury + n+ | ~yacc n => sc_r->yacc := prev.yacc + n+ | ~lex n => sc_r->lex := prev.lex + n+ | ~coq n => sc_r->coq := prev.coq + n+ | ~jupyter n => sc_r->jupyter := prev.jupyter + n+ | ~java n => sc_r->java := prev.java + n+ | ~scala n => sc_r->scala := prev.scala + n+ | ~erlang n => sc_r->erlang := prev.erlang + n+ | ~elixir n => sc_r->elixir := prev.elixir + n+ | ~pony n => sc_r->pony := prev.pony + n+ | ~clojure n => sc_r->clojure := prev.clojure + n+ | ~cabal_project n => sc_r->cabal_project := prev.cabal_project + n+ | ~assembly n => sc_r->assembly := prev.assembly + n+ | ~nix n => sc_r->nix := prev.nix + n+ | ~php n => sc_r->php := prev.php + n+ | ~javascript n => sc_r->javascript := prev.javascript + n+ | ~kotlin n => sc_r->kotlin := prev.kotlin + n+ | ~fsharp n => sc_r->fsharp := prev.fsharp + n+ | ~fortran n => sc_r->fortran := prev.fortran + n+ | ~swift n => sc_r->swift := prev.swift + n+ | ~csharp n => sc_r->csharp := prev.csharp + n+ | ~nim n => sc_r->nim := prev.nim + n+ | ~cpp_header n => sc_r->cpp_header := prev.cpp_header + n+ | ~elisp n => sc_r->elisp := prev.elisp + n+ | ~plaintext n => sc_r->plaintext := prev.plaintext + n+ | ~rakefile n => sc_r->rakefile := prev.rakefile + n+ | ~llvm n => sc_r->llvm := prev.llvm + n+ | ~autoconf n => sc_r->autoconf := prev.autoconf + n+ | ~batch n => sc_r->batch := prev.batch + n+ | ~powershell n => sc_r->powershell := prev.powershell + n+ | ~m4 n => sc_r->m4 := prev.m4 + n+ | ~objective_c n => sc_r->objective_c := prev.objective_c + n+ | ~automake n => sc_r->automake := prev.automake + n+ | ~margaret n => sc_r->margaret := prev.margaret + n+ | ~unknown _ => ()+ in+ !sc_r+ end++fun free_pl(pl : pl_type) : void =+ case+ pl of+ | ~unknown _ => ()+ | ~rust _ => ()+ | ~haskell _ => ()+ | ~perl _ => ()+ | ~lucius _ => ()+ | ~cassius _ => ()+ | ~hamlet _ => ()+ | ~julius _ => ()+ | ~bash _ => ()+ | ~coq _ => ()+ | ~justfile _ => ()+ | ~makefile _ => ()+ | ~yaml _ => ()+ | ~toml _ => ()+ | ~dhall _ => ()+ | ~ipkg _ => ()+ | ~ion _ => ()+ | ~mercury _ => ()+ | ~yacc _ => ()+ | ~lex _ => ()+ | ~r _ => ()+ | ~c _ => ()+ | ~cpp _ => ()+ | ~lua _ => ()+ | ~lalrpop _ => ()+ | ~header _ => ()+ | ~sixten _ => ()+ | ~java _ => ()+ | ~scala _ => ()+ | ~elixir _ => ()+ | ~erlang _ => ()+ | ~happy _ => ()+ | ~alex _ => ()+ | ~go _ => ()+ | ~html _ => ()+ | ~css _ => ()+ | ~brainfuck _ => ()+ | ~ruby _ => ()+ | ~julia _ => ()+ | ~elm _ => ()+ | ~purescript _ => ()+ | ~vimscript _ => ()+ | ~ocaml _ => ()+ | ~madlang _ => ()+ | ~agda _ => ()+ | ~idris _ => ()+ | ~futhark _ => ()+ | ~ats _ => ()+ | ~tex _ => ()+ | ~cabal _ => ()+ | ~cobol _ => ()+ | ~tcl _ => ()+ | ~verilog _ => ()+ | ~vhdl _ => ()+ | ~markdown _ => ()+ | ~python _ => ()+ | ~pony _ => ()+ | ~jupyter _ => ()+ | ~clojure _ => ()+ | ~cabal_project _ => ()+ | ~assembly _ => ()+ | ~nix _ => ()+ | ~php _ => ()+ | ~javascript _ => ()+ | ~kotlin _ => ()+ | ~fsharp _ => ()+ | ~fortran _ => ()+ | ~swift _ => ()+ | ~csharp _ => ()+ | ~nim _ => ()+ | ~cpp_header _ => ()+ | ~elisp _ => ()+ | ~plaintext _ => ()+ | ~rakefile _ => ()+ | ~llvm _ => ()+ | ~autoconf _ => ()+ | ~batch _ => ()+ | ~powershell _ => ()+ | ~m4 _ => ()+ | ~objective_c _ => ()+ | ~automake _ => ()+ | ~margaret _ => ()++// match a particular word against a list of keywords+fun match_keywords { m : nat | m <= 10 } (keys : list(string, m), word : string) : bool =+ list_foldright_cloref( keys+ , lam (next, acc) =<cloref1> acc || eq_string_string(next, word)+ , false+ )++// TODO use list_vt{int}(0, 1, 2, 3, 4) instead?+// helper function for check_keywords+fun step_keyword(size : file, pre : pl_type, word : string, ext : string) : pl_type =+ case+ pre of+ | unknown _ => let+ + in+ case+ ext of+ | "y" => let+ val _ = free_pl(pre)+ var happy_keywords = list_cons("module", list_nil())+ in+ if match_keywords(happy_keywords, word) then+ happy(size)+ else+ if let+ var yacc_keywords = list_cons("struct", list_cons("char", list_cons("int", list_nil())))+ in+ match_keywords(yacc_keywords, word)+ end then+ yacc(size)+ else+ unknown+ end+ | "v" => let+ var _ = free_pl(pre)+ var verilog_keywords = list_cons( "endmodule"+ , list_cons( "posedge"+ , list_cons( "edge"+ , list_cons("always", list_cons("wire", list_nil()))+ )+ )+ )+ in+ if match_keywords(verilog_keywords, word) then+ verilog(size)+ else+ if let+ var coq_keywords = list_cons( "Qed"+ , list_cons( "Require"+ , list_cons( "Hypothesis"+ , list_cons( "Inductive"+ , list_cons( "Remark"+ , list_cons( "Lemma"+ , list_cons( "Proof"+ , list_cons( "Definition"+ , list_cons( "Theorem"+ , list_nil()+ )+ )+ )+ )+ )+ )+ )+ )+ )+ in+ match_keywords(coq_keywords, word)+ end then+ coq(size)+ else+ unknown+ end+ | "m" => let+ val _ = free_pl(pre)+ var mercury_keywords = list_cons("module", list_cons("pred", list_cons("mode", list_nil())))+ in+ if match_keywords(mercury_keywords, word) then+ mercury(size)+ else+ if let+ var objective_c_keywords = list_cons( "nil"+ , list_cons("nullable", list_cons("nonnull", list_nil()))+ )+ in+ match_keywords(objective_c_keywords, word)+ end then+ objective_c(size)+ else+ unknown+ end+ | _ => pre+ end+ | _ => pre++// Function to disambiguate extensions such as .v (Coq and Verilog) and .m+// (Mercury and Objective C). This should only be called when extensions are in+// conflict, as it reads the whole file.+fun check_keywords(s : string, size : file, ext : string) : pl_type =+ let+ var ref = fileref_open_opt(s, file_mode_r)+ in+ case+ ref of+ | ~Some_vt (x) => let+ var init: pl_type = unknown+ var viewstream = $EXTRA.streamize_fileref_word(x)+ val result = stream_vt_foldleft_cloptr( viewstream+ , init+ , lam (acc, next) => step_keyword(size, acc, next, ext)+ )+ val _ = fileref_close(x)+ in+ result+ end+ | ~None_vt() => (println!("\33[33mWarning:\33[0m could not open file at " + s) ; unknown)+ end++// Check shebang on scripts.+//+// TODO flexible parser that drops spaces as appropriate+// TODO check magic number so as to avoid checking shebang of binary file+fun check_shebang(s : string) : pl_type =+ let+ val ref = fileref_open_opt(s, file_mode_r)+ val str: string = case+ ref of+ | ~Some_vt (x) => let+ val s = strptr2string(fileref_get_line_string(x))+ val _ = fileref_close(x)+ in+ s+ end+ | ~None_vt() => (println!("\33[33mWarning:\33[0m could not open file at " + s) ; "")+ in+ case+ str of+ | "#!/usr/bin/env ion" => ion(line_count(s, Some("#")))+ | "#!/usr/bin/env bash" => bash(line_count(s, Some("#")))+ | "#!/bin/bash" => bash(line_count(s, Some("#")))+ | "#!python" => python(line_count(s, Some("#")))+ | "#!python2" => python(line_count(s, Some("#")))+ | "#!python3" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env python" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env python2" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env python3" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env perl" => perl(line_count(s, Some("#")))+ | "#!/usr/bin/env perl6" => perl(line_count(s, Some("#")))+ | "#!/usr/bin/perl" => perl(line_count(s, Some("#")))+ | "#!/usr/bin/env stack" => haskell(line_count(s, Some("--")))+ | "#!/usr/bin/env runhaskell" => haskell(line_count(s, Some("--")))+ | "#!/usr/bin/env node" => javascript(line_count(s, None))+ | _ => unknown+ end++// Match based on filename (for makefiles, etc.)+fun match_filename(s : string) : pl_type =+ let+ val (prf | str) = filename_get_base(s)+ val match = $UN.strptr2string(str)+ + prval () = prf(str)+ in+ case+ match of+ | "Makefile" => makefile(line_count(s, Some("#")))+ | "Makefile.tc" => makefile(line_count(s, Some("#")))+ | "makefile" => makefile(line_count(s, Some("#")))+ | "GNUmakefile" => makefile(line_count(s, Some("#")))+ | "Justfile" => justfile(line_count(s, Some("#")))+ | "justfile" => justfile(line_count(s, Some("#")))+ | "Rakefile" => rakefile(line_count(s, None))+ | "cabal.project.local" => cabal_project(line_count(s, Some("--")))+ | _ => check_shebang(s)+ end++// Match based on file extension (assuming the file name is passed in as an+// argument).+fun prune_extension(s : string, file_proper : string) : pl_type =+ let+ val (prf | str) = filename_get_ext(file_proper)+ val match: string = if strptr2ptr(str) > 0 then+ $UN.strptr2string(str)+ else+ ""+ + prval () = prf(str)+ in+ case+ match of+ | "hs" => haskell(line_count(s, Some("--")))+ | "hs-boot" => haskell(line_count(s, Some("--")))+ | "hsig" => haskell(line_count(s, Some("--")))+ | "rs" => rust(line_count(s, Some("//")))+ | "tex" => tex(line_count(s, Some("%")))+ | "md" => markdown(line_count(s, None))+ | "markdown" => markdown(line_count(s, None))+ | "dats" => ats(line_count(s, Some("//")))+ | "hats" => ats(line_count(s, Some("//")))+ | "cats" => ats(line_count(s, Some("//")))+ | "sats" => ats(line_count(s, Some("//")))+ | "py" => python(line_count(s, None))+ | "fut" => futhark(line_count(s, Some("--")))+ | "pl" => perl(line_count(s, None))+ | "agda" => agda(line_count(s, Some("--")))+ | "idr" => idris(line_count(s, Some("--")))+ | "v" => check_keywords(s, line_count(s, Some("--")), match)+ | "m" => check_keywords(s, line_count(s, None), match)+ | "vhdl" => vhdl(line_count(s, None))+ | "vhd" => vhdl(line_count(s, None))+ | "go" => go(line_count(s, Some("//")))+ | "vim" => vimscript(line_count(s, None))+ | "ml" => ocaml(line_count(s, None))+ | "purs" => purescript(line_count(s, None))+ | "elm" => elm(line_count(s, Some("--")))+ | "mad" => madlang(line_count(s, Some("#")))+ | "toml" => toml(line_count(s, Some("#")))+ | "cabal" => cabal(line_count(s, Some("--")))+ | "yml" => yaml(line_count(s, Some("#")))+ | "yaml" => yaml(line_count(s, Some("#")))+ | "y" => check_keywords(s, line_count(s, None), match)+ | "ypp" => yacc(line_count(s, Some("//")))+ | "x" => alex(line_count(s, Some("--")))+ | "l" => lex(line_count(s, None))+ | "lpp" => lex(line_count(s, None))+ | "html" => html(line_count(s, None))+ | "htm" => html(line_count(s, None))+ | "css" => css(line_count(s, None))+ | "vhdl" => vhdl(line_count(s, None))+ | "vhd" => vhdl(line_count(s, None))+ | "c" => c(line_count(s, Some("//")))+ | "b" => brainfuck(line_count(s, None))+ | "bf" => brainfuck(line_count(s, None))+ | "rb" => ruby(line_count(s, None))+ | "cob" => cobol(line_count(s, None))+ | "cbl" => cobol(line_count(s, None))+ | "cpy" => cobol(line_count(s, None))+ | "ml" => ocaml(line_count(s, None))+ | "tcl" => tcl(line_count(s, None))+ | "r" => r(line_count(s, None))+ | "R" => r(line_count(s, None))+ | "lua" => lua(line_count(s, None))+ | "cpp" => cpp(line_count(s, Some("//")))+ | "cc" => cpp(line_count(s, Some("//")))+ | "lalrpop" => lalrpop(line_count(s, Some("//")))+ | "h" => header(line_count(s, None))+ | "vix" => sixten(line_count(s, Some("--")))+ | "dhall" => dhall(line_count(s, None))+ | "ipkg" => ipkg(line_count(s, Some("--")))+ | "mk" => makefile(line_count(s, Some("#")))+ | "hamlet" => hamlet(line_count(s, None))+ | "cassius" => cassius(line_count(s, None))+ | "lucius" => cassius(line_count(s, None))+ | "julius" => julius(line_count(s, None))+ | "jl" => julia(line_count(s, None))+ | "ion" => ion(line_count(s, Some("#")))+ | "bash" => bash(line_count(s, Some("#")))+ | "ipynb" => jupyter(line_count(s, None))+ | "java" => java(line_count(s, None))+ | "scala" => scala(line_count(s, None))+ | "erl" => erlang(line_count(s, None))+ | "hrl" => erlang(line_count(s, None))+ | "ex" => elixir(line_count(s, None))+ | "exs" => elixir(line_count(s, None))+ | "pony" => pony(line_count(s, None))+ | "clj" => clojure(line_count(s, None))+ | "s" => assembly(line_count(s, Some(";")))+ | "S" => assembly(line_count(s, Some(";")))+ | "asm" => assembly(line_count(s, Some(";")))+ | "nix" => nix(line_count(s, None))+ | "php" => php(line_count(s, None))+ | "local" => match_filename(s)+ | "project" => cabal_project(line_count(s, Some("--")))+ | "js" => javascript(line_count(s, None))+ | "jsexe" => javascript(line_count(s, None))+ | "kt" => kotlin(line_count(s, None))+ | "kts" => kotlin(line_count(s, None))+ | "fs" => fsharp(line_count(s, None))+ | "f" => fortran(line_count(s, None))+ | "for" => fortran(line_count(s, None))+ | "f90" => fortran(line_count(s, None))+ | "f95" => fortran(line_count(s, None))+ | "swift" => swift(line_count(s, None))+ | "csharp" => csharp(line_count(s, None))+ | "nim" => nim(line_count(s, None))+ | "el" => elisp(line_count(s, None))+ | "txt" => plaintext(line_count(s, None))+ | "ll" => llvm(line_count(s, None))+ | "in" => autoconf(line_count(s, Some("#")))+ | "bat" => batch(line_count(s, None))+ | "ps1" => powershell(line_count(s, None))+ | "ac" => m4(line_count(s, None))+ | "mm" => objective_c(line_count(s, Some("//")))+ | "am" => automake(line_count(s, Some("#")))+ | "mgt" => margaret(line_count(s, Some("--")))+ | "" => match_filename(s)+ | "sh" => match_filename(s)+ | "yamllint" => match_filename(s)+ | _ => unknown+ end++// filter out directories containing artifacts+fun bad_dir(s : string, excludes : List0(string)) : bool =+ case+ s of+ | "." => true+ | ".." => true+ | ".pijul" => true+ | "_darcs" => true+ | ".hg" => true+ | ".git" => true+ | "target" => true+ | ".egg-info" => true+ | "nimcache" => true+ | ".shake" => true+ | "dist-newstyle" => true+ | "dist" => true+ | ".psc-package" => true+ | ".pulp-cache" => true+ | "output" => true+ | "bower_components" => true+ | "elm-stuff" => true+ | ".stack-work" => true+ | ".reco" => true+ | ".reco-work" => true+ | ".cabal-sandbox" => true+ | "node_modules" => true+ | ".lein-plugins" => true+ | ".sass-cache" => true+ | _ => list_exists_cloref(excludes, lam x => x = s || x = s + "/")++fnx step_stream( acc : source_contents+ , full_name : string+ , file_proper : string+ , excludes : List0(string)+ ) : source_contents =+ if test_file_isdir(full_name) != 0 then+ flow_stream(full_name, acc, excludes)+ else+ adjust_contents(acc, prune_extension(full_name, file_proper))+and flow_stream(s : string, init : source_contents, excludes : List0(string)) :+source_contents =+ let+ var files = streamize_dirname_fname(s)+ var ffiles = stream_vt_filter_cloptr(files, lam x => not(bad_dir(x, excludes)))+ in+ stream_vt_foldleft_cloptr( ffiles+ , init+ , lam (acc, next) => step_stream(acc, s + "/" + next, next, excludes)+ )+ end++fun empty_contents() : source_contents =+ let+ var isc = @{ rust = empty_file()+ , haskell = empty_file()+ , ats = empty_file()+ , python = empty_file()+ , vimscript = empty_file()+ , elm = empty_file()+ , idris = empty_file()+ , madlang = empty_file()+ , tex = empty_file()+ , markdown = empty_file()+ , yaml = empty_file()+ , toml = empty_file()+ , cabal = empty_file()+ , happy = empty_file()+ , alex = empty_file()+ , go = empty_file()+ , html = empty_file()+ , css = empty_file()+ , verilog = empty_file()+ , vhdl = empty_file()+ , c = empty_file()+ , purescript = empty_file()+ , futhark = empty_file()+ , brainfuck = empty_file()+ , ruby = empty_file()+ , julia = empty_file()+ , perl = empty_file()+ , ocaml = empty_file()+ , agda = empty_file()+ , cobol = empty_file()+ , tcl = empty_file()+ , r = empty_file()+ , lua = empty_file()+ , cpp = empty_file()+ , lalrpop = empty_file()+ , header = empty_file()+ , sixten = empty_file()+ , dhall = empty_file()+ , ipkg = empty_file()+ , makefile = empty_file()+ , justfile = empty_file()+ , ion = empty_file()+ , bash = empty_file()+ , hamlet = empty_file()+ , cassius = empty_file()+ , lucius = empty_file()+ , julius = empty_file()+ , mercury = empty_file()+ , yacc = empty_file()+ , lex = empty_file()+ , coq = empty_file()+ , jupyter = empty_file()+ , java = empty_file()+ , scala = empty_file()+ , erlang = empty_file()+ , elixir = empty_file()+ , pony = empty_file()+ , clojure = empty_file()+ , cabal_project = empty_file()+ , assembly = empty_file()+ , nix = empty_file()+ , php = empty_file()+ , javascript = empty_file()+ , kotlin = empty_file()+ , fsharp = empty_file()+ , fortran = empty_file()+ , swift = empty_file()+ , csharp = empty_file()+ , nim = empty_file()+ , cpp_header = empty_file()+ , elisp = empty_file()+ , plaintext = empty_file()+ , rakefile = empty_file()+ , llvm = empty_file()+ , autoconf = empty_file()+ , batch = empty_file()+ , powershell = empty_file()+ , m4 = empty_file()+ , objective_c = empty_file()+ , automake = empty_file()+ , margaret = empty_file()+ } : source_contents+ in+ isc+ end++fun map_stream(acc : source_contents, includes : List0(string), excludes : List0(string)) :+source_contents =+ list_foldleft_cloref( includes+ , acc+ , lam (acc, next) => if test_file_exists(next) || next = "" then+ step_stream(acc, next, next, excludes)+ else+ (prerr("\33[31mError:\33[0m directory '" + next + "' does not exist\n") ; (exit(1) ; acc))+ )++fun is_flag(s : string) : bool =+ string_is_prefix("-", s)++fun process_excludes(s : string, acc : command_line) : command_line =+ let+ val acc_r = ref<command_line>(acc)+ val () = if is_flag(s) then+ (println!("Error: flag " + s + " found where a directory name was expected") ; (exit(0) ; ()))+ else+ acc_r->excludes := list_cons(s, acc.excludes)+ in+ !acc_r+ end++fun process(s : string, acc : command_line, is_first : bool) : command_line =+ let+ val acc_r = ref<command_line>(acc)+ val () = if is_flag(s) then+ case+ s of+ | "--help" => acc_r->help := true+ | "-h" => acc_r->help := true+ | "--no-table" => if not(acc.no_table) then+ acc_r->no_table := true+ else+ (println!("\33[31mError:\33[0m flag " + s + " cannot appear twice") ; (exit(0) ; ()))+ | "-t" => if not(acc.no_table) then+ acc_r->no_table := true+ else+ (println!("\33[31mError:\33[0m flag " + s + " cannot appear twice") ; (exit(0) ; ()))+ | "--parallel" => acc_r->parallel := true+ | "-p" => acc_r->parallel := true+ | "--version" => acc_r->version := true+ | "-V" => acc_r->version := true+ | "-e" => (println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument") ;+ (exit(0) ; ()))+ | "--exclude" => (println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument"+ ) ; (exit(0) ; ()))+ | _ => (println!("\33[31mError:\33[0m flag '" + s + "' not recognized") ; (exit(0) ; ()))+ else+ if not(is_first) then+ acc_r->includes := list_cons(s, acc.includes)+ else+ ()+ in+ !acc_r+ end++fnx get_cli { n : int | n >= 1 }{ m : nat | m < n } .<n - m>. ( argc : int(n)+ , argv : !(argv(n))+ , current : int(m)+ , prev_is_exclude : bool+ , acc : command_line+ ) : command_line =+ let+ var arg = argv[current]+ in+ if current < argc - 1 then+ if arg != "--exclude" && arg != "-e" then+ let+ val c = get_cli(argc, argv, current + 1, false, acc)+ in+ if prev_is_exclude && current != 0 then+ process_excludes(arg, c)+ else+ if current != 0 then+ process(arg, c, current = 0)+ else+ c+ end+ else+ let+ val c = get_cli(argc, argv, current + 1, true, acc)+ in+ c+ end+ else+ if prev_is_exclude then+ process_excludes(arg, acc)+ else+ process(arg, acc, current = 0)+ end++fun version() : void =+ println!("polygot version 0.3.11\nCopyright (c) 2017 Vanessa McHale")++fun help() : void =+ print("polyglot - Count lines of code quickly.++\33[36mUSAGE:\33[0m poly [DIRECTORY] ... [OPTION] ...++\33[36mFLAGS:\33[0m+ -V, --version show version information+ -h, --help display this help and exit+ -e, --exclude exclude a directory+ -p, --parallel execute in parallel+ -t, --no-table display results in alternate format++When no directory is provided poly will execute in the+current directory.++Bug reports and updates: nest.pijul.com/vamchale/polyglot\n"+ )++fun head(xs : List0(string)) : string =+ case+ xs of+ | list_cons (x, xs) => x + ", " + head(xs)+ | list_nil() => ""++// TODO channel to draw work? e.g. take a channel of strings, return a channel of source_contents+fun work( excludes : List0(string)+ , send : channel(List0(string))+ , chan : channel(source_contents)+ ) : void =+ {+ val- (n) = channel_remove(send)+ var x = map_stream(empty_contents(), n, excludes)+ val () = channel_insert(chan, x)+ val- ~None_vt() = channel_unref(chan)+ val- () = case channel_unref<List0(string)>(send) of+ | ~None_vt() => ()+ | ~Some_vt (snd) => queue_free<List0(string)>(snd)+ }++// Function returning the number of CPU cores.+extern+fun ncpu () : int++%{^+#include <unistd.h>+int ncpu() {+ return sysconf(_SC_NPROCESSORS_ONLN);+}+%}++#define NCPU 4++fun apportion(includes : List0(string)) : (List0(string), List0(string)) =+ let+ var n = length(includes) / 2+ val (p, q) = list_split_at(includes, n)+ in+ (list_vt2t(p), q)+ end++// TODO maybe make a parallel fold?+fun threads(includes : List0(string), excludes : List0(string)) : source_contents =+ let+ val chan = channel_make<source_contents>(2)+ val chan2 = channel_ref(chan)+ val chan3 = channel_ref(chan)+ val send1 = channel_make<List0(string)>(1)+ val send2 = channel_make<List0(string)>(1)+ val send_r1 = channel_ref(send1)+ val send_r2 = channel_ref(send2)+ var new_includes = if length(includes) > 0 then+ includes+ else+ list_cons(".", list_nil())+ val (fst, snd) = apportion(new_includes)+ val _ = channel_insert(send1, fst)+ val _ = channel_insert(send2, snd)+ val t2 = athread_create_cloptr_exn(llam () => work(excludes, send_r1, chan2))+ val t3 = athread_create_cloptr_exn(llam () => work(excludes, send_r2, chan3))+ val- ~None_vt() = channel_unref(send1)+ val- ~None_vt() = channel_unref(send2)+ val- (n) = channel_remove(chan)+ val- (m) = channel_remove(chan)+ val () = ignoret(usleep(1u))+ val () = while(channel_refcount(chan) >= 2)()+ val r = add_contents(n, m)+ val- ~Some_vt (que) = channel_unref<source_contents>(chan)+ val () = queue_free<source_contents>(que)+ in+ r+ end++implement main0 (argc, argv) =+ let+ val cli = @{ version = false+ , help = false+ , no_table = false+ , parallel = false+ , excludes = list_nil()+ , includes = list_nil()+ } : command_line+ val parsed = get_cli(argc, argv, 0, false, cli)+ in+ if parsed.help then+ (help() ; exit(0))+ else+ if parsed.version then+ (version() ; exit(0))+ else+ let+ val result = if parsed.parallel then+ threads(parsed.includes, parsed.excludes)+ else+ if length(parsed.includes) > 0 then+ map_stream(empty_contents(), parsed.includes, parsed.excludes)+ else+ map_stream(empty_contents(), list_cons(".", list_nil()), parsed.excludes)+ in+ if parsed.no_table then+ print(make_output(result))+ else+ print(make_table(result))+ end+ end
+ test/data/polyglot.out view
@@ -0,0 +1,1619 @@+#include "share/atspre_staload.hats"+#include "share/HATS/atslib_staload_libats_libc.hats"+#include "prelude/DATS/filebas.dats"+#include "libats/ML/DATS/filebas_dirent.dats"+#include "libats/libc/DATS/dirent.dats"+#include "src/concurrency.dats"+#include "libats/DATS/athread_posix.dats"+#include "prelude/DATS/stream_vt.dats"++%{^+#include "libats/libc/CATS/string.cats"+#include "prelude/CATS/filebas.cats"+%}++staload "prelude/SATS/stream_vt.sats"+staload "libats/ML/DATS/list0.dats"+staload "libats/SATS/athread.sats"+staload "libats/ML/DATS/string.dats"+staload "libats/libc/SATS/stdio.sats"+staload "prelude/SATS/filebas.sats"+staload "src/filetype.sats"+staload "libats/ML/DATS/filebas.dats"+staload EXTRA = "libats/ML/SATS/filebas.sats"+staload "libats/libc/SATS/unistd.sats"+staload "libats/DATS/athread.dats"++fun to_file(s : string, pre : Option(string)) : file =+ let+ val is_comment = case+ pre of+ | Some (x) => string_is_prefix(x, s)+ | None => false+ in+ if s = "" then+ @{ lines = 1, blanks = 1, comments = 0, files = 0 }+ else+ if is_comment then+ @{ lines = 1, blanks = 0, comments = 1, files = 0 }+ else+ @{ lines = 1, blanks = 0, comments = 0, files = 0 }+ end++fun empty_file() : file =+ let+ var f = @{ files = 0, blanks = 0, comments = 0, lines = 0 } : file+ in+ f+ end++fun acc_file() : file =+ let+ var f = @{ files = 1, blanks = 0, comments = 0, lines = ~1 } : file+ in+ f+ end++// monoidal addition for 'file' type+fun add_results(x : file, y : file) : file =+ let+ var next = @{ lines = x.lines + y.lines+ , blanks = x.blanks + y.blanks+ , comments = x.comments + y.comments+ , files = x.files + y.files+ }+ in+ next+ end++overload + with add_results++// Given a string representing a filepath, return an integer.+fun line_count(s : string, pre : Option(string)) : file =+ let+ var ref = fileref_open_opt(s, file_mode_r)+ in+ case ref of+ | ~Some_vt (x) => + begin+ let+ var viewstream: stream_vt(string) = $EXTRA.streamize_fileref_line(x)+ val n: file = stream_vt_foldleft_cloptr( viewstream+ , acc_file()+ , lam (acc, f) =<cloptr1> acc + to_file(f, pre)+ )+ val _ = fileref_close(x)+ in+ n+ end+ end+ | ~None_vt() => ( println!("\33[33mWarning:\33[0m could not open file at " + s)+ ; to_file(s, None)+ )+ end++// Pad a string of bounded length on the right by adding spaces.+fnx right_pad { k : int | k >= 0 }{ m : int | m <= k } .<k>.+(s : string(m), n : int(k)) : string =+ case+ length(s) < n of+ | true when n > 0 => right_pad(s, n - 1) + " "+ | _ => s++// Pad a string on the left by adding spaces.+fnx left_pad { k : int | k >= 0 } .<k>. (s : string, n : int(k)) :+ string =+ case+ length(s) < n of+ | true when n > 0 => " " + left_pad(s, n - 1)+ | _ => s++// helper function for make_output+fun maybe_string(s : string, n : int) : string =+ if n > 0 then+ s + ": " + tostring_int(n) + "\n"+ else+ ""++// helper function for make_table+fun maybe_table { k : int | k >= 0 && k < 20 } ( s : string(k)+ , f : file+ ) : string =+ let+ var code = f.lines - f.comments - f.blanks+ in+ if f.files > 0 then+ " "+ + right_pad(s, 21)+ + left_pad(tostring_int(f.files), 5)+ + left_pad(tostring_int(f.lines), 12)+ + left_pad(tostring_int(code), 13)+ + left_pad(tostring_int(f.comments), 13)+ + left_pad(tostring_int(f.blanks), 13)+ + "\n"+ else+ ""+ end++// helper function for make_output+fun with_nonempty(s1 : string, s2 : string) : string =+ if s2 != "" then+ s1 + s2+ else+ ""++// helper function to make totals for tabular output.+fun sum_fields(sc : source_contents) : file =+ let+ var f = @{ lines = sc.rust.lines+ + sc.haskell.lines+ + sc.ats.lines+ + sc.python.lines+ + sc.vimscript.lines+ + sc.elm.lines+ + sc.idris.lines+ + sc.madlang.lines+ + sc.tex.lines+ + sc.markdown.lines+ + sc.yaml.lines+ + sc.toml.lines+ + sc.cabal.lines+ + sc.happy.lines+ + sc.alex.lines+ + sc.go.lines+ + sc.html.lines+ + sc.css.lines+ + sc.verilog.lines+ + sc.vhdl.lines+ + sc.c.lines+ + sc.purescript.lines+ + sc.futhark.lines+ + sc.brainfuck.lines+ + sc.ruby.lines+ + sc.julia.lines+ + sc.perl.lines+ + sc.ocaml.lines+ + sc.agda.lines+ + sc.cobol.lines+ + sc.tcl.lines+ + sc.r.lines+ + sc.lua.lines+ + sc.cpp.lines+ + sc.lalrpop.lines+ + sc.header.lines+ + sc.sixten.lines+ + sc.dhall.lines+ + sc.ipkg.lines+ + sc.makefile.lines+ + sc.justfile.lines+ + sc.ion.lines+ + sc.bash.lines+ + sc.hamlet.lines+ + sc.cassius.lines+ + sc.lucius.lines+ + sc.julius.lines+ + sc.mercury.lines+ + sc.yacc.lines+ + sc.lex.lines+ + sc.coq.lines+ + sc.jupyter.lines+ + sc.java.lines+ + sc.scala.lines+ + sc.erlang.lines+ + sc.elixir.lines+ + sc.pony.lines+ + sc.clojure.lines+ + sc.cabal_project.lines+ + sc.assembly.lines+ + sc.nix.lines+ + sc.php.lines+ + sc.javascript.lines+ + sc.kotlin.lines+ + sc.fsharp.lines+ + sc.fortran.lines+ + sc.swift.lines+ + sc.csharp.lines+ + sc.nim.lines+ + sc.cpp_header.lines+ + sc.elisp.lines+ + sc.plaintext.lines+ + sc.rakefile.lines+ + sc.llvm.lines+ + sc.autoconf.lines+ + sc.batch.lines+ + sc.powershell.lines+ + sc.m4.lines+ + sc.objective_c.lines+ + sc.automake.lines+ , blanks = sc.rust.blanks+ + sc.haskell.blanks+ + sc.ats.blanks+ + sc.python.blanks+ + sc.vimscript.blanks+ + sc.elm.blanks+ + sc.idris.blanks+ + sc.madlang.blanks+ + sc.tex.blanks+ + sc.markdown.blanks+ + sc.yaml.blanks+ + sc.toml.blanks+ + sc.cabal.blanks+ + sc.happy.blanks+ + sc.alex.blanks+ + sc.go.blanks+ + sc.html.blanks+ + sc.css.blanks+ + sc.verilog.blanks+ + sc.vhdl.blanks+ + sc.c.blanks+ + sc.purescript.blanks+ + sc.futhark.blanks+ + sc.brainfuck.blanks+ + sc.ruby.blanks+ + sc.julia.blanks+ + sc.perl.blanks+ + sc.ocaml.blanks+ + sc.agda.blanks+ + sc.cobol.blanks+ + sc.tcl.blanks+ + sc.r.blanks+ + sc.lua.blanks+ + sc.cpp.blanks+ + sc.lalrpop.blanks+ + sc.header.blanks+ + sc.sixten.blanks+ + sc.dhall.blanks+ + sc.ipkg.blanks+ + sc.makefile.blanks+ + sc.justfile.blanks+ + sc.ion.blanks+ + sc.bash.blanks+ + sc.hamlet.blanks+ + sc.cassius.blanks+ + sc.lucius.blanks+ + sc.julius.blanks+ + sc.mercury.blanks+ + sc.yacc.blanks+ + sc.lex.blanks+ + sc.coq.blanks+ + sc.jupyter.blanks+ + sc.java.blanks+ + sc.scala.blanks+ + sc.erlang.blanks+ + sc.elixir.blanks+ + sc.pony.blanks+ + sc.clojure.blanks+ + sc.cabal_project.blanks+ + sc.assembly.blanks+ + sc.nix.blanks+ + sc.php.blanks+ + sc.javascript.blanks+ + sc.kotlin.blanks+ + sc.fsharp.blanks+ + sc.fortran.blanks+ + sc.swift.blanks+ + sc.csharp.blanks+ + sc.nim.blanks+ + sc.cpp_header.blanks+ + sc.elisp.blanks+ + sc.plaintext.blanks+ + sc.rakefile.blanks+ + sc.llvm.blanks+ + sc.autoconf.blanks+ + sc.batch.blanks+ + sc.powershell.blanks+ + sc.m4.blanks+ + sc.objective_c.blanks+ + sc.automake.blanks+ , comments = sc.rust.comments+ + sc.haskell.comments+ + sc.ats.comments+ + sc.python.comments+ + sc.vimscript.comments+ + sc.elm.comments+ + sc.idris.comments+ + sc.madlang.comments+ + sc.tex.comments+ + sc.markdown.comments+ + sc.yaml.comments+ + sc.toml.comments+ + sc.cabal.comments+ + sc.happy.comments+ + sc.alex.comments+ + sc.go.comments+ + sc.html.comments+ + sc.css.comments+ + sc.verilog.comments+ + sc.vhdl.comments+ + sc.c.comments+ + sc.purescript.comments+ + sc.futhark.comments+ + sc.brainfuck.comments+ + sc.ruby.comments+ + sc.julia.comments+ + sc.perl.comments+ + sc.ocaml.comments+ + sc.agda.comments+ + sc.cobol.comments+ + sc.tcl.comments+ + sc.r.comments+ + sc.lua.comments+ + sc.cpp.comments+ + sc.lalrpop.comments+ + sc.header.comments+ + sc.sixten.comments+ + sc.dhall.comments+ + sc.ipkg.comments+ + sc.makefile.comments+ + sc.justfile.comments+ + sc.ion.comments+ + sc.bash.comments+ + sc.hamlet.comments+ + sc.cassius.comments+ + sc.lucius.comments+ + sc.julius.comments+ + sc.mercury.comments+ + sc.yacc.comments+ + sc.lex.comments+ + sc.coq.comments+ + sc.jupyter.comments+ + sc.java.comments+ + sc.scala.comments+ + sc.erlang.comments+ + sc.elixir.comments+ + sc.pony.comments+ + sc.clojure.comments+ + sc.cabal_project.comments+ + sc.assembly.comments+ + sc.nix.comments+ + sc.php.comments+ + sc.javascript.comments+ + sc.kotlin.comments+ + sc.fsharp.comments+ + sc.fortran.comments+ + sc.swift.comments+ + sc.csharp.comments+ + sc.nim.comments+ + sc.cpp_header.comments+ + sc.elisp.comments+ + sc.plaintext.comments+ + sc.rakefile.comments+ + sc.llvm.comments+ + sc.autoconf.comments+ + sc.batch.comments+ + sc.powershell.comments+ + sc.m4.comments+ + sc.objective_c.comments+ + sc.automake.comments+ , files = sc.rust.files+ + sc.haskell.files+ + sc.ats.files+ + sc.python.files+ + sc.vimscript.files+ + sc.elm.files+ + sc.idris.files+ + sc.madlang.files+ + sc.tex.files+ + sc.markdown.files+ + sc.yaml.files+ + sc.toml.files+ + sc.cabal.files+ + sc.happy.files+ + sc.alex.files+ + sc.go.files+ + sc.html.files+ + sc.css.files+ + sc.verilog.files+ + sc.vhdl.files+ + sc.c.files+ + sc.purescript.files+ + sc.futhark.files+ + sc.brainfuck.files+ + sc.ruby.files+ + sc.julia.files+ + sc.perl.files+ + sc.ocaml.files+ + sc.agda.files+ + sc.cobol.files+ + sc.tcl.files+ + sc.r.files+ + sc.lua.files+ + sc.cpp.files+ + sc.lalrpop.files+ + sc.header.files+ + sc.sixten.files+ + sc.dhall.files+ + sc.ipkg.files+ + sc.makefile.files+ + sc.justfile.files+ + sc.ion.files+ + sc.bash.files+ + sc.hamlet.files+ + sc.cassius.files+ + sc.lucius.files+ + sc.julius.files+ + sc.mercury.files+ + sc.yacc.files+ + sc.lex.files+ + sc.coq.files+ + sc.jupyter.files+ + sc.java.files+ + sc.scala.files+ + sc.erlang.files+ + sc.elixir.files+ + sc.pony.files+ + sc.clojure.files+ + sc.cabal_project.files+ + sc.assembly.files+ + sc.nix.files+ + sc.php.files+ + sc.javascript.files+ + sc.kotlin.files+ + sc.fsharp.files+ + sc.fortran.files+ + sc.swift.files+ + sc.csharp.files+ + sc.nim.files+ + sc.cpp_header.files+ + sc.elisp.files+ + sc.plaintext.files+ + sc.rakefile.files+ + sc.llvm.files+ + sc.autoconf.files+ + sc.batch.files+ + sc.powershell.files+ + sc.m4.files+ + sc.objective_c.files+ + sc.automake.files+ }+ in+ f+ end++// function to print tabular output at the end+fun make_table(isc : source_contents) : string =+ "-------------------------------------------------------------------------------\n \33[35mLanguage\33[0m \33[35mFiles\33[0m \33[35mLines\33[0m \33[35mCode\33[0m \33[35mComments\33[0m \33[35mBlanks\33[0m\n-------------------------------------------------------------------------------\n"+ + maybe_table("Alex", isc.alex)+ + maybe_table("Agda", isc.agda)+ + maybe_table("Assembly", isc.assembly)+ + maybe_table("ATS", isc.ats)+ + maybe_table("Autoconf", isc.autoconf)+ + maybe_table("Automake", isc.automake)+ + maybe_table("Bash", isc.bash)+ + maybe_table("Batch", isc.batch)+ + maybe_table("Brainfuck", isc.brainfuck)+ + maybe_table("C", isc.c)+ + maybe_table("C Header", isc.header)+ + maybe_table("C++ cpp_header", isc.cpp_header)+ + maybe_table("C++", isc.cpp)+ + maybe_table("C#", isc.csharp)+ + maybe_table("Cabal", isc.cabal)+ + maybe_table("Cabal Project", isc.cabal_project)+ + maybe_table("Cassius", isc.cassius)+ + maybe_table("COBOL", isc.cobol)+ + maybe_table("Coq", isc.coq)+ + maybe_table("CSS", isc.css)+ + maybe_table("Dhall", isc.dhall)+ + maybe_table("Elixir", isc.elixir)+ + maybe_table("Elm", isc.elm)+ + maybe_table("Emacs Lisp", isc.elisp)+ + maybe_table("Erlang", isc.erlang)+ + maybe_table("F#", isc.fsharp)+ + maybe_table("Fortran", isc.fortran)+ + maybe_table("Go", isc.go)+ + maybe_table("Hamlet", isc.hamlet)+ + maybe_table("Happy", isc.happy)+ + maybe_table("Haskell", isc.haskell)+ + maybe_table("HTML", isc.html)+ + maybe_table("Idris", isc.idris)+ + maybe_table("iPKG", isc.ipkg)+ + maybe_table("Ion", isc.ion)+ + maybe_table("Java", isc.java)+ + maybe_table("JavaScript", isc.javascript)+ + maybe_table("Julius", isc.julius)+ + maybe_table("Julia", isc.julia)+ + maybe_table("Jupyter", isc.jupyter)+ + maybe_table("Justfile", isc.justfile)+ + maybe_table("Kotlin", isc.kotlin)+ + maybe_table("LALRPOP", isc.lalrpop)+ + maybe_table("Lex", isc.lex)+ + maybe_table("LLVM", isc.llvm)+ + maybe_table("Lua", isc.lua)+ + maybe_table("Lucius", isc.lucius)+ + maybe_table("M4", isc.m4)+ + maybe_table("Madlang", isc.madlang)+ + maybe_table("Makefile", isc.makefile)+ + maybe_table("Margaret", isc.margaret)+ + maybe_table("Markdown", isc.markdown)+ + maybe_table("Mercury", isc.mercury)+ + maybe_table("Nim", isc.nim)+ + maybe_table("Nix", isc.nix)+ + maybe_table("Objective C", isc.objective_c)+ + maybe_table("OCaml", isc.ocaml)+ + maybe_table("Perl", isc.perl)+ + maybe_table("PHP", isc.php)+ + maybe_table("Plaintext", isc.plaintext)+ + maybe_table("PowerShell", isc.powershell)+ + maybe_table("Pony", isc.pony)+ + maybe_table("Python", isc.python)+ + maybe_table("PureScript", isc.purescript)+ + maybe_table("R", isc.r)+ + maybe_table("Rakefile", isc.rakefile)+ + maybe_table("Ruby", isc.ruby)+ + maybe_table("Rust", isc.rust)+ + maybe_table("Scala", isc.scala)+ + maybe_table("Sixten", isc.sixten)+ + maybe_table("Swift", isc.swift)+ + maybe_table("TCL", isc.tcl)+ + maybe_table("TeX", isc.tex)+ + maybe_table("TOML", isc.toml)+ + maybe_table("Verilog", isc.verilog)+ + maybe_table("VHDL", isc.vhdl)+ + maybe_table("Vimscript", isc.vimscript)+ + maybe_table("Yacc", isc.yacc)+ + maybe_table("YAML", isc.yaml)+ + "-------------------------------------------------------------------------------\n"+ + maybe_table("Total", sum_fields(isc))+ + "-------------------------------------------------------------------------------\n"++// Function to print output sorted by type of language.+fun make_output(isc : source_contents) : string =+ with_nonempty( "\33[33mProgramming Languages:\33[0m\n"+ , maybe_string("Agda", isc.agda.lines)+ + maybe_string("Assembly", isc.assembly.lines)+ + maybe_string("ATS", isc.ats.lines)+ + maybe_string("Brainfuck", isc.brainfuck.lines)+ + maybe_string("C", isc.c.lines)+ + maybe_string("C Header", isc.header.lines)+ + maybe_string("C++", isc.cpp.lines)+ + maybe_string("C++ Header", isc.cpp_header.lines)+ + maybe_string("C#", isc.csharp.lines)+ + maybe_string("COBOL", isc.cobol.lines)+ + maybe_string("Coq", isc.coq.lines)+ + maybe_string("Elixir", isc.elixir.lines)+ + maybe_string("Elm", isc.elm.lines)+ + maybe_string("Erlang", isc.erlang.lines)+ + maybe_string("F#", isc.fsharp.lines)+ + maybe_string("Fortran", isc.fortran.lines)+ + maybe_string("Go", isc.go.lines)+ + maybe_string("Haskell", isc.haskell.lines)+ + maybe_string("Idris", isc.idris.lines)+ + maybe_string("Kotline", isc.kotlin.lines)+ + maybe_string("Java", isc.java.lines)+ + maybe_string("Julia", isc.julia.lines)+ + maybe_string("Lua", isc.lua.lines)+ + maybe_string("Margaret", isc.margaret.lines)+ + maybe_string("Mercury", isc.mercury.lines)+ + maybe_string("Nim", isc.nim.lines)+ + maybe_string("Objective C", isc.objective_c.lines)+ + maybe_string("OCaml", isc.ocaml.lines)+ + maybe_string("Perl", isc.perl.lines)+ + maybe_string("Pony", isc.pony.lines)+ + maybe_string("PureScript", isc.purescript.lines)+ + maybe_string("Python", isc.python.lines)+ + maybe_string("R", isc.r.lines)+ + maybe_string("Ruby", isc.ruby.lines)+ + maybe_string("Rust", isc.rust.lines)+ + maybe_string("Scala", isc.scala.lines)+ + maybe_string("Sixten", isc.sixten.lines)+ + maybe_string("Swift", isc.swift.lines)+ + maybe_string("TCL", isc.tcl.lines)+ )+ + with_nonempty( "\n\33[33mEditor Plugins:\33[0m\n"+ , maybe_string("Emacs Lisp", isc.elisp.lines)+ + maybe_string("Vimscript", isc.vimscript.lines)+ )+ + with_nonempty( "\n\33[33mDocumentation:\33[0m\n"+ , maybe_string("Markdown", isc.markdown.lines)+ + maybe_string("Plaintext", isc.plaintext.lines)+ + maybe_string("TeX", isc.tex.lines)+ )+ + with_nonempty( "\n\33[33mConfiguration:\33[0m\n"+ , maybe_string("Cabal", isc.cabal.lines)+ + maybe_string("Cabal Project", isc.cabal_project.lines)+ + maybe_string("Dhall", isc.dhall.lines)+ + maybe_string("iPKG", isc.ipkg.lines)+ + maybe_string("TOML", isc.toml.lines)+ + maybe_string("YAML", isc.yaml.lines)+ )+ + with_nonempty( "\n\33[33mShell:\33[0m\n"+ , maybe_string("Bash", isc.bash.lines)+ + maybe_string("Batch", isc.batch.lines)+ + maybe_string("Ion", isc.ion.lines)+ + maybe_string("PowerShell", isc.powershell.lines)+ )+ + with_nonempty( "\n\33[33mParser Generators:\33[0m\n"+ , maybe_string("Alex", isc.alex.lines)+ + maybe_string("Happy", isc.happy.lines)+ + maybe_string("LALRPOP", isc.lalrpop.lines)+ + maybe_string("Lex", isc.lex.lines)+ + maybe_string("Yacc", isc.yacc.lines)+ )+ + with_nonempty( "\n\33[33mWeb:\33[0m\n"+ , maybe_string("Cassius", isc.cassius.lines)+ + maybe_string("CSS", isc.css.lines)+ + maybe_string("Hamlet", isc.hamlet.lines)+ + maybe_string("HTML", isc.html.lines)+ + maybe_string("JavaScript", isc.javascript.lines)+ + maybe_string("Julius", isc.julius.lines)+ + maybe_string("Lucius", isc.lucius.lines)+ )+ + with_nonempty( "\n\33[33mHardware:\33[0m\n"+ , maybe_string("Verilog", isc.verilog.lines)+ + maybe_string("VHDL", isc.vhdl.lines)+ )+ + with_nonempty( "\n\33[33mNotebooks:\33[0m\n"+ , maybe_string("Jupyter", isc.jupyter.lines)+ )+ + with_nonempty( "\n\33[33mOther:\33[0m\n"+ , maybe_string("Autoconf", isc.autoconf.lines)+ + maybe_string("Automake", isc.automake.lines)+ + maybe_string("Justfile", isc.justfile.lines)+ + maybe_string("LLVM", isc.llvm.lines)+ + maybe_string("M4", isc.m4.lines)+ + maybe_string("Madlang", isc.madlang.lines)+ + maybe_string("Makefile", isc.makefile.lines)+ + maybe_string("Rakefile", isc.rakefile.lines)+ )++fun add_contents(x : source_contents, y : source_contents) :+ source_contents =+ let+ var next = @{ rust = x.rust + y.rust+ , haskell = x.haskell + y.haskell+ , ats = x.ats + y.ats+ , python = x.python + y.python+ , vimscript = x.vimscript + y.vimscript+ , elm = x.elm + y.elm+ , idris = x.idris + y.idris+ , madlang = x.madlang + y.madlang+ , tex = x.tex + y.tex+ , markdown = x.markdown + y.markdown+ , yaml = x.yaml + y.yaml+ , toml = x.toml + y.toml+ , cabal = x.cabal + y.cabal+ , happy = x.happy + y.happy+ , alex = x.alex + y.alex+ , go = x.go + y.go+ , html = x.html + y.html+ , css = x.css + y.css+ , verilog = x.verilog + y.verilog+ , vhdl = x.vhdl + y.vhdl+ , c = x.c + y.c+ , purescript = x.purescript + y.purescript+ , futhark = x.futhark + y.futhark+ , brainfuck = x.brainfuck + y.brainfuck+ , ruby = x.ruby + y.ruby+ , julia = x.julia + y.julia+ , perl = x.perl + y.perl+ , ocaml = x.ocaml + y.ocaml+ , agda = x.agda + y.agda+ , cobol = x.cobol + y.cobol+ , tcl = x.tcl + y.tcl+ , r = x.r + y.r+ , lua = x.lua + y.lua+ , cpp = x.cpp + y.cpp+ , lalrpop = x.lalrpop + y.lalrpop+ , header = x.header + y.header+ , sixten = x.sixten + y.sixten+ , dhall = x.dhall + y.dhall+ , ipkg = x.ipkg + y.ipkg+ , makefile = x.makefile + y.makefile+ , justfile = x.justfile + y.justfile+ , ion = x.ion + y.ion+ , bash = x.bash + y.bash+ , hamlet = x.hamlet + y.hamlet+ , cassius = x.cassius + y.cassius+ , lucius = x.lucius + y.lucius+ , julius = x.julius + y.julius+ , mercury = x.mercury + y.mercury+ , yacc = x.yacc + y.yacc+ , lex = x.lex + y.lex+ , coq = x.coq + y.coq+ , jupyter = x.jupyter + y.jupyter+ , java = x.java + y.java+ , scala = x.scala + y.scala+ , erlang = x.erlang + y.erlang+ , elixir = x.elixir + y.elixir+ , pony = x.pony + y.pony+ , clojure = x.clojure + y.clojure+ , cabal_project = x.cabal_project + y.cabal_project+ , assembly = x.assembly + y.assembly+ , nix = x.nix + y.nix+ , php = x.php + y.php+ , javascript = x.javascript + y.javascript+ , kotlin = x.kotlin + y.kotlin+ , fsharp = x.fsharp + y.fsharp+ , fortran = x.fortran + y.fortran+ , swift = x.swift + y.swift+ , csharp = x.csharp + y.csharp+ , nim = x.nim + y.nim+ , cpp_header = x.cpp_header + y.cpp_header+ , elisp = x.elisp + y.elisp+ , plaintext = x.plaintext + y.plaintext+ , rakefile = x.rakefile + y.rakefile+ , llvm = x.llvm + y.llvm+ , autoconf = x.autoconf + y.autoconf+ , batch = x.batch + y.batch+ , powershell = x.powershell + y.powershell+ , m4 = x.m4 + y.m4+ , objective_c = x.objective_c + y.objective_c+ , automake = x.automake + y.automake+ , margaret = x.margaret + y.margaret+ } : source_contents+ in+ next+ end++// This is the step function used when streaming directory contents. +fun adjust_contents(prev : source_contents, scf : pl_type) :+ source_contents =+ let+ val sc_r = ref<source_contents>(prev)+ val _ = case+ scf of+ | ~haskell n => sc_r->haskell := prev.haskell + n+ | ~ats n => sc_r->ats := prev.ats + n+ | ~rust n => sc_r->rust := prev.rust + n+ | ~markdown n => sc_r->markdown := prev.markdown + n+ | ~python n => sc_r->python := prev.python + n+ | ~vimscript n => sc_r->vimscript := prev.vimscript + n+ | ~yaml n => sc_r->yaml := prev.yaml + n+ | ~toml n => sc_r->toml := prev.toml + n+ | ~happy n => sc_r->happy := prev.happy + n+ | ~alex n => sc_r->alex := prev.alex + n+ | ~idris n => sc_r->idris := prev.idris + n+ | ~madlang n => sc_r->madlang := prev.madlang + n+ | ~elm n => sc_r->elm := prev.elm + n+ | ~c n => sc_r->c := prev.c + n+ | ~go n => sc_r->go := prev.go + n+ | ~cabal n => sc_r->cabal := prev.cabal + n+ | ~verilog n => sc_r->verilog := prev.verilog + n+ | ~vhdl n => sc_r->vhdl := prev.vhdl + n+ | ~html n => sc_r->html := prev.html + n+ | ~css n => sc_r->css := prev.css + n+ | ~purescript n => sc_r->purescript := prev.purescript + n+ | ~futhark n => sc_r->futhark := prev.futhark + n+ | ~brainfuck n => sc_r->brainfuck := prev.brainfuck + n+ | ~ruby n => sc_r->ruby := prev.ruby + n+ | ~julia n => sc_r->julia := prev.julia + n+ | ~tex n => sc_r->tex := prev.tex + n+ | ~perl n => sc_r->perl := prev.perl + n+ | ~ocaml n => sc_r->ocaml := prev.ocaml + n+ | ~agda n => sc_r->agda := prev.agda + n+ | ~cobol n => sc_r->cobol := prev.cobol + n+ | ~tcl n => sc_r->tcl := prev.tcl + n+ | ~r n => sc_r->r := prev.r + n+ | ~lua n => sc_r->lua := prev.lua + n+ | ~cpp n => sc_r->cpp := prev.cpp + n+ | ~lalrpop n => sc_r->lalrpop := prev.lalrpop + n+ | ~header n => sc_r->header := prev.header + n+ | ~sixten n => sc_r->sixten := prev.sixten + n+ | ~dhall n => sc_r->dhall := prev.dhall + n+ | ~ipkg n => sc_r->ipkg := prev.ipkg + n+ | ~justfile n => sc_r->justfile := prev.justfile + n+ | ~makefile n => sc_r->makefile := prev.makefile + n+ | ~ion n => sc_r->ion := prev.ion + n+ | ~bash n => sc_r->bash := prev.bash + n+ | ~hamlet n => sc_r->hamlet := prev.hamlet + n+ | ~cassius n => sc_r->cassius := prev.cassius + n+ | ~lucius n => sc_r->lucius := prev.lucius + n+ | ~julius n => sc_r->julius := prev.julius + n+ | ~mercury n => sc_r->mercury := prev.mercury + n+ | ~yacc n => sc_r->yacc := prev.yacc + n+ | ~lex n => sc_r->lex := prev.lex + n+ | ~coq n => sc_r->coq := prev.coq + n+ | ~jupyter n => sc_r->jupyter := prev.jupyter + n+ | ~java n => sc_r->java := prev.java + n+ | ~scala n => sc_r->scala := prev.scala + n+ | ~erlang n => sc_r->erlang := prev.erlang + n+ | ~elixir n => sc_r->elixir := prev.elixir + n+ | ~pony n => sc_r->pony := prev.pony + n+ | ~clojure n => sc_r->clojure := prev.clojure + n+ | ~cabal_project n => sc_r->cabal_project := prev.cabal_project + n+ | ~assembly n => sc_r->assembly := prev.assembly + n+ | ~nix n => sc_r->nix := prev.nix + n+ | ~php n => sc_r->php := prev.php + n+ | ~javascript n => sc_r->javascript := prev.javascript + n+ | ~kotlin n => sc_r->kotlin := prev.kotlin + n+ | ~fsharp n => sc_r->fsharp := prev.fsharp + n+ | ~fortran n => sc_r->fortran := prev.fortran + n+ | ~swift n => sc_r->swift := prev.swift + n+ | ~csharp n => sc_r->csharp := prev.csharp + n+ | ~nim n => sc_r->nim := prev.nim + n+ | ~cpp_header n => sc_r->cpp_header := prev.cpp_header + n+ | ~elisp n => sc_r->elisp := prev.elisp + n+ | ~plaintext n => sc_r->plaintext := prev.plaintext + n+ | ~rakefile n => sc_r->rakefile := prev.rakefile + n+ | ~llvm n => sc_r->llvm := prev.llvm + n+ | ~autoconf n => sc_r->autoconf := prev.autoconf + n+ | ~batch n => sc_r->batch := prev.batch + n+ | ~powershell n => sc_r->powershell := prev.powershell + n+ | ~m4 n => sc_r->m4 := prev.m4 + n+ | ~objective_c n => sc_r->objective_c := prev.objective_c + n+ | ~automake n => sc_r->automake := prev.automake + n+ | ~margaret n => sc_r->margaret := prev.margaret + n+ | ~unknown _ => ()+ in+ !sc_r+ end++fun free_pl(pl : pl_type) : void =+ case+ pl of+ | ~unknown _ => ()+ | ~rust _ => ()+ | ~haskell _ => ()+ | ~perl _ => ()+ | ~lucius _ => ()+ | ~cassius _ => ()+ | ~hamlet _ => ()+ | ~julius _ => ()+ | ~bash _ => ()+ | ~coq _ => ()+ | ~justfile _ => ()+ | ~makefile _ => ()+ | ~yaml _ => ()+ | ~toml _ => ()+ | ~dhall _ => ()+ | ~ipkg _ => ()+ | ~ion _ => ()+ | ~mercury _ => ()+ | ~yacc _ => ()+ | ~lex _ => ()+ | ~r _ => ()+ | ~c _ => ()+ | ~cpp _ => ()+ | ~lua _ => ()+ | ~lalrpop _ => ()+ | ~header _ => ()+ | ~sixten _ => ()+ | ~java _ => ()+ | ~scala _ => ()+ | ~elixir _ => ()+ | ~erlang _ => ()+ | ~happy _ => ()+ | ~alex _ => ()+ | ~go _ => ()+ | ~html _ => ()+ | ~css _ => ()+ | ~brainfuck _ => ()+ | ~ruby _ => ()+ | ~julia _ => ()+ | ~elm _ => ()+ | ~purescript _ => ()+ | ~vimscript _ => ()+ | ~ocaml _ => ()+ | ~madlang _ => ()+ | ~agda _ => ()+ | ~idris _ => ()+ | ~futhark _ => ()+ | ~ats _ => ()+ | ~tex _ => ()+ | ~cabal _ => ()+ | ~cobol _ => ()+ | ~tcl _ => ()+ | ~verilog _ => ()+ | ~vhdl _ => ()+ | ~markdown _ => ()+ | ~python _ => ()+ | ~pony _ => ()+ | ~jupyter _ => ()+ | ~clojure _ => ()+ | ~cabal_project _ => ()+ | ~assembly _ => ()+ | ~nix _ => ()+ | ~php _ => ()+ | ~javascript _ => ()+ | ~kotlin _ => ()+ | ~fsharp _ => ()+ | ~fortran _ => ()+ | ~swift _ => ()+ | ~csharp _ => ()+ | ~nim _ => ()+ | ~cpp_header _ => ()+ | ~elisp _ => ()+ | ~plaintext _ => ()+ | ~rakefile _ => ()+ | ~llvm _ => ()+ | ~autoconf _ => ()+ | ~batch _ => ()+ | ~powershell _ => ()+ | ~m4 _ => ()+ | ~objective_c _ => ()+ | ~automake _ => ()+ | ~margaret _ => ()++// match a particular word against a list of keywords+fun match_keywords { m : nat | m <= 10 } ( keys : list(string, m)+ , word : string+ ) : bool =+ list_foldright_cloref(keys, lam (next, acc) =<cloref1> acc+ || eq_string_string(next, word), false)++// TODO use list_vt{int}(0, 1, 2, 3, 4) instead?+// helper function for check_keywords+fun step_keyword( size : file+ , pre : pl_type+ , word : string+ , ext : string+ ) : pl_type =+ case+ pre of+ | unknown _ => let+ + in+ case+ ext of+ | "y" => let+ val _ = free_pl(pre)+ var happy_keywords = list_cons("module", list_nil())+ in+ if match_keywords(happy_keywords, word) then+ happy(size)+ else+ if let+ var yacc_keywords = list_cons( "struct"+ , list_cons("char", list_cons("int", list_nil()))+ )+ in+ match_keywords(yacc_keywords, word)+ end then+ yacc(size)+ else+ unknown+ end+ | "v" => let+ var _ = free_pl(pre)+ var verilog_keywords = list_cons( "endmodule"+ , list_cons( "posedge"+ , list_cons( "edge"+ , list_cons("always", list_cons("wire", list_nil()))+ )+ )+ )+ in+ if match_keywords( verilog_keywords+ , word+ ) then+ verilog(size)+ else+ if let+ var coq_keywords = list_cons( "Qed"+ , list_cons( "Require"+ , list_cons( "Hypothesis"+ , list_cons( "Inductive"+ , list_cons( "Remark"+ , list_cons( "Lemma"+ , list_cons( "Proof"+ , list_cons( "Definition"+ , list_cons( "Theorem"+ , list_nil()+ )+ )+ )+ )+ )+ )+ )+ )+ )+ in+ match_keywords(coq_keywords, word)+ end then+ coq(size)+ else+ unknown+ end+ | "m" => let+ val _ = free_pl(pre)+ var mercury_keywords = list_cons( "module"+ , list_cons("pred", list_cons("mode", list_nil()))+ )+ in+ if match_keywords(mercury_keywords, word) then+ mercury(size)+ else+ if let+ var objective_c_keywords = list_cons( "nil"+ , list_cons("nullable", list_cons("nonnull", list_nil()))+ )+ in+ match_keywords(objective_c_keywords, word)+ end then+ objective_c(size)+ else+ unknown+ end+ | _ => pre+ end+ | _ => pre++// Function to disambiguate extensions such as .v (Coq and Verilog) and .m+// (Mercury and Objective C). This should only be called when extensions are in+// conflict, as it reads the whole file.+fun check_keywords(s : string, size : file, ext : string) : pl_type =+ let+ var ref = fileref_open_opt(s, file_mode_r)+ in+ case+ ref of+ | ~Some_vt (x) => let+ var init: pl_type = unknown+ var viewstream = $EXTRA.streamize_fileref_word(x)+ val result = stream_vt_foldleft_cloptr( viewstream+ , init+ , lam (acc, next) =>+ step_keyword(size, acc, next, ext)+ )+ val _ = fileref_close(x)+ in+ result+ end+ | ~None_vt() => ( println!("\33[33mWarning:\33[0m could not open file at " + s)+ ; unknown+ )+ end++// Check shebang on scripts.+//+// TODO flexible parser that drops spaces as appropriate+// TODO check magic number so as to avoid checking shebang of binary file+fun check_shebang(s : string) : pl_type =+ let+ val ref = fileref_open_opt(s, file_mode_r)+ val str: string = case+ ref of+ | ~Some_vt (x) => let+ val s = strptr2string(fileref_get_line_string(x))+ val _ = fileref_close(x)+ in+ s+ end+ | ~None_vt() => ( println!("\33[33mWarning:\33[0m could not open file at " + s)+ ; ""+ )+ in+ case+ str of+ | "#!/usr/bin/env ion" => ion(line_count(s, Some("#")))+ | "#!/usr/bin/env bash" => bash(line_count(s, Some("#")))+ | "#!/bin/bash" => bash(line_count(s, Some("#")))+ | "#!python" => python(line_count(s, Some("#")))+ | "#!python2" => python(line_count(s, Some("#")))+ | "#!python3" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env python" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env python2" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env python3" => python(line_count(s, Some("#")))+ | "#!/usr/bin/env perl" => perl(line_count(s, Some("#")))+ | "#!/usr/bin/env perl6" => perl(line_count(s, Some("#")))+ | "#!/usr/bin/perl" => perl(line_count(s, Some("#")))+ | "#!/usr/bin/env stack" => haskell(line_count(s, Some("--")))+ | "#!/usr/bin/env runhaskell" => haskell(line_count(s, Some("--")))+ | "#!/usr/bin/env node" => javascript(line_count(s, None))+ | _ => unknown+ end++// Match based on filename (for makefiles, etc.)+fun match_filename(s : string) : pl_type =+ let+ val (prf | str) = filename_get_base(s)+ val match = $UN.strptr2string(str)+ prval () = prf(str)+ in+ case+ match of+ | "Makefile" => makefile(line_count(s, Some("#")))+ | "Makefile.tc" => makefile(line_count(s, Some("#")))+ | "makefile" => makefile(line_count(s, Some("#")))+ | "GNUmakefile" => makefile(line_count(s, Some("#")))+ | "Justfile" => justfile(line_count(s, Some("#")))+ | "justfile" => justfile(line_count(s, Some("#")))+ | "Rakefile" => rakefile(line_count(s, None))+ | "cabal.project.local" => cabal_project(line_count(s, Some("--")))+ | _ => check_shebang(s)+ end++// Match based on file extension (assuming the file name is passed in as an+// argument).+fun prune_extension(s : string, file_proper : string) : pl_type =+ let+ val (prf | str) = filename_get_ext(file_proper)+ val match: string = if strptr2ptr(str) > 0 then+ $UN.strptr2string(str)+ else+ ""+ prval () = prf(str)+ in+ case+ match of+ | "hs" => haskell(line_count(s, Some("--")))+ | "hs-boot" => haskell(line_count(s, Some("--")))+ | "hsig" => haskell(line_count(s, Some("--")))+ | "rs" => rust(line_count(s, Some("//")))+ | "tex" => tex(line_count(s, Some("%")))+ | "md" => markdown(line_count(s, None))+ | "markdown" => markdown(line_count(s, None))+ | "dats" => ats(line_count(s, Some("//")))+ | "hats" => ats(line_count(s, Some("//")))+ | "cats" => ats(line_count(s, Some("//")))+ | "sats" => ats(line_count(s, Some("//")))+ | "py" => python(line_count(s, None))+ | "fut" => futhark(line_count(s, Some("--")))+ | "pl" => perl(line_count(s, None))+ | "agda" => agda(line_count(s, Some("--")))+ | "idr" => idris(line_count(s, Some("--")))+ | "v" => check_keywords(s, line_count(s, Some("--")), match)+ | "m" => check_keywords(s, line_count(s, None), match)+ | "vhdl" => vhdl(line_count(s, None))+ | "vhd" => vhdl(line_count(s, None))+ | "go" => go(line_count(s, Some("//")))+ | "vim" => vimscript(line_count(s, None))+ | "ml" => ocaml(line_count(s, None))+ | "purs" => purescript(line_count(s, None))+ | "elm" => elm(line_count(s, Some("--")))+ | "mad" => madlang(line_count(s, Some("#")))+ | "toml" => toml(line_count(s, Some("#")))+ | "cabal" => cabal(line_count(s, Some("--")))+ | "yml" => yaml(line_count(s, Some("#")))+ | "yaml" => yaml(line_count(s, Some("#")))+ | "y" => check_keywords(s, line_count(s, None), match)+ | "ypp" => yacc(line_count(s, Some("//")))+ | "x" => alex(line_count(s, Some("--")))+ | "l" => lex(line_count(s, None))+ | "lpp" => lex(line_count(s, None))+ | "html" => html(line_count(s, None))+ | "htm" => html(line_count(s, None))+ | "css" => css(line_count(s, None))+ | "vhdl" => vhdl(line_count(s, None))+ | "vhd" => vhdl(line_count(s, None))+ | "c" => c(line_count(s, Some("//")))+ | "b" => brainfuck(line_count(s, None))+ | "bf" => brainfuck(line_count(s, None))+ | "rb" => ruby(line_count(s, None))+ | "cob" => cobol(line_count(s, None))+ | "cbl" => cobol(line_count(s, None))+ | "cpy" => cobol(line_count(s, None))+ | "ml" => ocaml(line_count(s, None))+ | "tcl" => tcl(line_count(s, None))+ | "r" => r(line_count(s, None))+ | "R" => r(line_count(s, None))+ | "lua" => lua(line_count(s, None))+ | "cpp" => cpp(line_count(s, Some("//")))+ | "cc" => cpp(line_count(s, Some("//")))+ | "lalrpop" => lalrpop(line_count(s, Some("//")))+ | "h" => header(line_count(s, None))+ | "vix" => sixten(line_count(s, Some("--")))+ | "dhall" => dhall(line_count(s, None))+ | "ipkg" => ipkg(line_count(s, Some("--")))+ | "mk" => makefile(line_count(s, Some("#")))+ | "hamlet" => hamlet(line_count(s, None))+ | "cassius" => cassius(line_count(s, None))+ | "lucius" => cassius(line_count(s, None))+ | "julius" => julius(line_count(s, None))+ | "jl" => julia(line_count(s, None))+ | "ion" => ion(line_count(s, Some("#")))+ | "bash" => bash(line_count(s, Some("#")))+ | "ipynb" => jupyter(line_count(s, None))+ | "java" => java(line_count(s, None))+ | "scala" => scala(line_count(s, None))+ | "erl" => erlang(line_count(s, None))+ | "hrl" => erlang(line_count(s, None))+ | "ex" => elixir(line_count(s, None))+ | "exs" => elixir(line_count(s, None))+ | "pony" => pony(line_count(s, None))+ | "clj" => clojure(line_count(s, None))+ | "s" => assembly(line_count(s, Some(";")))+ | "S" => assembly(line_count(s, Some(";")))+ | "asm" => assembly(line_count(s, Some(";")))+ | "nix" => nix(line_count(s, None))+ | "php" => php(line_count(s, None))+ | "local" => match_filename(s)+ | "project" => cabal_project(line_count(s, Some("--")))+ | "js" => javascript(line_count(s, None))+ | "jsexe" => javascript(line_count(s, None))+ | "kt" => kotlin(line_count(s, None))+ | "kts" => kotlin(line_count(s, None))+ | "fs" => fsharp(line_count(s, None))+ | "f" => fortran(line_count(s, None))+ | "for" => fortran(line_count(s, None))+ | "f90" => fortran(line_count(s, None))+ | "f95" => fortran(line_count(s, None))+ | "swift" => swift(line_count(s, None))+ | "csharp" => csharp(line_count(s, None))+ | "nim" => nim(line_count(s, None))+ | "el" => elisp(line_count(s, None))+ | "txt" => plaintext(line_count(s, None))+ | "ll" => llvm(line_count(s, None))+ | "in" => autoconf(line_count(s, Some("#")))+ | "bat" => batch(line_count(s, None))+ | "ps1" => powershell(line_count(s, None))+ | "ac" => m4(line_count(s, None))+ | "mm" => objective_c(line_count(s, Some("//")))+ | "am" => automake(line_count(s, Some("#")))+ | "mgt" => margaret(line_count(s, Some("--")))+ | "" => match_filename(s)+ | "sh" => match_filename(s)+ | "yamllint" => match_filename(s)+ | _ => unknown+ end++// filter out directories containing artifacts+fun bad_dir(s : string, excludes : List0(string)) : bool =+ case+ s of+ | "." => true+ | ".." => true+ | ".pijul" => true+ | "_darcs" => true+ | ".hg" => true+ | ".git" => true+ | "target" => true+ | ".egg-info" => true+ | "nimcache" => true+ | ".shake" => true+ | "dist-newstyle" => true+ | "dist" => true+ | ".psc-package" => true+ | ".pulp-cache" => true+ | "output" => true+ | "bower_components" => true+ | "elm-stuff" => true+ | ".stack-work" => true+ | ".reco" => true+ | ".reco-work" => true+ | ".cabal-sandbox" => true+ | "node_modules" => true+ | ".lein-plugins" => true+ | ".sass-cache" => true+ | _ => list_exists_cloref(excludes, lam x => x = s || x = s + "/")++fnx step_stream( acc : source_contents+ , full_name : string+ , file_proper : string+ , excludes : List0(string)+ ) : source_contents =+ if test_file_isdir(full_name) != 0 then+ flow_stream(full_name, acc, excludes)+ else+ adjust_contents(acc, prune_extension(full_name, file_proper))+and flow_stream( s : string+ , init : source_contents+ , excludes : List0(string)+ ) : source_contents =+ let+ var files = streamize_dirname_fname(s)+ var ffiles = stream_vt_filter_cloptr(files, lam x => not(bad_dir( x+ , excludes+ )))+ in+ stream_vt_foldleft_cloptr( ffiles+ , init+ , lam (acc, next) =>+ step_stream(acc, s + "/" + next, next, excludes)+ )+ end++fun empty_contents() : source_contents =+ let+ var isc = @{ rust = empty_file()+ , haskell = empty_file()+ , ats = empty_file()+ , python = empty_file()+ , vimscript = empty_file()+ , elm = empty_file()+ , idris = empty_file()+ , madlang = empty_file()+ , tex = empty_file()+ , markdown = empty_file()+ , yaml = empty_file()+ , toml = empty_file()+ , cabal = empty_file()+ , happy = empty_file()+ , alex = empty_file()+ , go = empty_file()+ , html = empty_file()+ , css = empty_file()+ , verilog = empty_file()+ , vhdl = empty_file()+ , c = empty_file()+ , purescript = empty_file()+ , futhark = empty_file()+ , brainfuck = empty_file()+ , ruby = empty_file()+ , julia = empty_file()+ , perl = empty_file()+ , ocaml = empty_file()+ , agda = empty_file()+ , cobol = empty_file()+ , tcl = empty_file()+ , r = empty_file()+ , lua = empty_file()+ , cpp = empty_file()+ , lalrpop = empty_file()+ , header = empty_file()+ , sixten = empty_file()+ , dhall = empty_file()+ , ipkg = empty_file()+ , makefile = empty_file()+ , justfile = empty_file()+ , ion = empty_file()+ , bash = empty_file()+ , hamlet = empty_file()+ , cassius = empty_file()+ , lucius = empty_file()+ , julius = empty_file()+ , mercury = empty_file()+ , yacc = empty_file()+ , lex = empty_file()+ , coq = empty_file()+ , jupyter = empty_file()+ , java = empty_file()+ , scala = empty_file()+ , erlang = empty_file()+ , elixir = empty_file()+ , pony = empty_file()+ , clojure = empty_file()+ , cabal_project = empty_file()+ , assembly = empty_file()+ , nix = empty_file()+ , php = empty_file()+ , javascript = empty_file()+ , kotlin = empty_file()+ , fsharp = empty_file()+ , fortran = empty_file()+ , swift = empty_file()+ , csharp = empty_file()+ , nim = empty_file()+ , cpp_header = empty_file()+ , elisp = empty_file()+ , plaintext = empty_file()+ , rakefile = empty_file()+ , llvm = empty_file()+ , autoconf = empty_file()+ , batch = empty_file()+ , powershell = empty_file()+ , m4 = empty_file()+ , objective_c = empty_file()+ , automake = empty_file()+ , margaret = empty_file()+ } : source_contents+ in+ isc+ end++fun map_stream( acc : source_contents+ , includes : List0(string)+ , excludes : List0(string)+ ) : source_contents =+ list_foldleft_cloref( includes+ , acc+ , lam (acc, next) =>+ if test_file_exists(next) || next = "" then+ step_stream(acc, next, next, excludes)+ else+ ( prerr("\33[31mError:\33[0m directory '" + next + "' does not exist\n")+ ; exit(1)+ ; acc+ )+ )++fun is_flag(s : string) : bool =+ string_is_prefix("-", s)++fun process_excludes(s : string, acc : command_line) : command_line =+ let+ val acc_r = ref<command_line>(acc)+ val () = if is_flag(s) then+ ( println!("Error: flag " + s + " found where a directory name was expected")+ ; exit(0)+ ; ()+ )+ else+ acc_r->excludes := list_cons(s, acc.excludes)+ in+ !acc_r+ end++fun process(s : string, acc : command_line, is_first : bool) :+ command_line =+ let+ val acc_r = ref<command_line>(acc)+ val () = if is_flag(s) then+ case+ s of+ | "--help" => acc_r->help := true+ | "-h" => acc_r->help := true+ | "--no-table" => if not(acc.no_table) then+ acc_r->no_table := true+ else+ ( println!("\33[31mError:\33[0m flag " + s + " cannot appear twice")+ ; exit(0)+ ; ()+ )+ | "-t" => if not(acc.no_table) then+ acc_r->no_table := true+ else+ ( println!("\33[31mError:\33[0m flag " + s + " cannot appear twice")+ ; exit(0)+ ; ()+ )+ | "--parallel" => acc_r->parallel := true+ | "-p" => acc_r->parallel := true+ | "--version" => acc_r->version := true+ | "-V" => acc_r->version := true+ | "-e" => ( println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument")+ ; exit(0)+ ; ()+ )+ | "--exclude" => ( println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument")+ ; exit(0)+ ; ()+ )+ | _ => ( println!("\33[31mError:\33[0m flag '" + s + "' not recognized")+ ; exit(0)+ ; ()+ )+ else+ if not(is_first) then+ acc_r->includes := list_cons(s, acc.includes)+ else+ ()+ in+ !acc_r+ end++fnx get_cli { n : int | n >= 1 }{ m : nat | m < n } .<n-m>.+( argc : int(n)+, argv : !argv(n)+, current : int(m)+, prev_is_exclude : bool+, acc : command_line+) : command_line =+ let+ var arg = argv[current]+ in+ if current < argc - 1 then+ if arg != "--exclude" && arg != "-e" then+ let+ val c = get_cli(argc, argv, current + 1, false, acc)+ in+ if prev_is_exclude && current != 0 then+ process_excludes(arg, c)+ else+ if current != 0 then+ process(arg, c, current = 0)+ else+ c+ end+ else+ let+ val c = get_cli(argc, argv, current + 1, true, acc)+ in+ c+ end+ else+ if prev_is_exclude then+ process_excludes(arg, acc)+ else+ process(arg, acc, current = 0)+ end++fun version() : void =+ println!("polygot version 0.3.11\nCopyright (c) 2017 Vanessa McHale")++fun help() : void =+ print("polyglot - Count lines of code quickly.++\33[36mUSAGE:\33[0m poly [DIRECTORY] ... [OPTION] ...++\33[36mFLAGS:\33[0m+ -V, --version show version information+ -h, --help display this help and exit+ -e, --exclude exclude a directory+ -p, --parallel execute in parallel+ -t, --no-table display results in alternate format++When no directory is provided poly will execute in the+current directory.++Bug reports and updates: nest.pijul.com/vamchale/polyglot\n")++fun head(xs : List0(string)) : string =+ case+ xs of+ | list_cons (x, xs) => x + ", " + head(xs)+ | list_nil() => ""++// TODO channel to draw work? e.g. take a channel of strings, return a channel of source_contents+fun work( excludes : List0(string)+ , send : channel(List0(string))+ , chan : channel(source_contents)+ ) : void =+ {+ val- (n) = channel_remove(send)+ var x = map_stream(empty_contents(), n, excludes)+ val () = channel_insert(chan, x)+ val- ~None_vt() = channel_unref(chan)+ val- () = case channel_unref<List0(string)>(send) of+ | ~None_vt() => ()+ | ~Some_vt (snd) => queue_free<List0(string)>(snd)+ }++// Function returning the number of CPU cores.+extern+fun ncpu() : int++%{^+#include <unistd.h>+int ncpu() {+ return sysconf(_SC_NPROCESSORS_ONLN);+}+%}++#define NCPU 4++fun apportion(includes : List0(string)) :+ (List0(string), List0(string)) =+ let+ var n = length(includes) / 2+ val (p, q) = list_split_at(includes, n)+ in+ (list_vt2t(p), q)+ end++// TODO maybe make a parallel fold?+fun threads(includes : List0(string), excludes : List0(string)) :+ source_contents =+ let+ val chan = channel_make<source_contents>(2)+ val chan2 = channel_ref(chan)+ val chan3 = channel_ref(chan)+ val send1 = channel_make<List0(string)>(1)+ val send2 = channel_make<List0(string)>(1)+ val send_r1 = channel_ref(send1)+ val send_r2 = channel_ref(send2)+ var new_includes = if length(includes) > 0 then+ includes+ else+ list_cons(".", list_nil())+ val (fst, snd) = apportion(new_includes)+ val _ = channel_insert(send1, fst)+ val _ = channel_insert(send2, snd)+ val t2 = athread_create_cloptr_exn(llam () =>+ work(excludes, send_r1, chan2))+ val t3 = athread_create_cloptr_exn(llam () =>+ work(excludes, send_r2, chan3))+ val- ~None_vt() = channel_unref(send1)+ val- ~None_vt() = channel_unref(send2)+ val- (n) = channel_remove(chan)+ val- (m) = channel_remove(chan)+ val () = ignoret(usleep(1u))+ val () = while(channel_refcount(chan) >= 2)()+ val r = add_contents(n, m)+ val- ~Some_vt (que) = channel_unref<source_contents>(chan)+ val () = queue_free<source_contents>(que)+ in+ r+ end++implement main0 (argc, argv) =+ let+ val cli = @{ version = false+ , help = false+ , no_table = false+ , parallel = false+ , excludes = list_nil()+ , includes = list_nil()+ } : command_line+ val parsed = get_cli(argc, argv, 0, false, cli)+ in+ if parsed.help then+ (help() ; exit(0))+ else+ if parsed.version then+ (version() ; exit(0))+ else+ let+ val result = if parsed.parallel then+ threads(parsed.includes, parsed.excludes)+ else+ if length(parsed.includes) > 0 then+ map_stream(empty_contents(), parsed.includes, parsed.excludes)+ else+ map_stream( empty_contents()+ , list_cons(".", list_nil())+ , parsed.excludes+ )+ in+ if parsed.no_table then+ print(make_output(result))+ else+ print(make_table(result))+ end+ end
+ test/data/toml-parse.dats view
@@ -0,0 +1,244 @@+#include "share/atspre_staload.hats"+#include "share/HATS/atslib_staload_libats_libc.hats"++staload UN = "prelude/SATS/unsafe.sats"+staload "src/types.sats"+staload "prelude/basics_sta.sats"+staload "libats/libc/SATS/stdio.sats"+staload "prelude/SATS/string.sats"++fun snoc(s : string, c : char) : string =+ let+ val sc = char2string(c)+ val x = string0_append(s, sc)+ in+ strptr2string(x)+ end++fun next {m : nat} (x : string(m)) : Option_vt(char) =+ if length(x) > 0 then+ Some_vt(string_head(x))+ else+ None_vt++fun stop_plain_string(c : char) : bool =+ case+ c of+ | '\n' => true+ | '#' => true+ | _ => false++fun map {a : vtype}{b : vtype} (f : a -<lincloptr1> b, x : parser(a)) : parser(b) =+ let+ val g = x.modify+ in+ @{ modify = llam c =<lincloptr1> + begin+ let+ val (y, z): (cstream, a) = g(c)+ val w: b = f(z)+ in+ (cloptr_free($UN.castvwtp0(f)) ; cloptr_free($UN.castvwtp0(g)) ; (y, w))+ end+ end }+ end++extern+fun bind {a : vtype}{b : vtype} (x : parser(a), f : a -<lincloptr1> parser(b)) : parser(b)++fun pure {a : vtype} (x : a) : parser(a) =+ @{ modify = llam c =<lincloptr1> (c, x) }++fun chain {a : vtype}{b : vtype} (x : parser(a), y : parser(b)) : parser(b) =+ @{ modify = llam c =<lincloptr1> let+ val f = x.modify+ val g = y.modify+ val (pre_res, _) = f(c)+ val (res, y) = g(pre_res)+ val _ = cloptr_free($UN.castvwtp0(f))+ val _ = cloptr_free($UN.castvwtp0(g))+ in+ (res, y)+ end }++fun run_parser {a : vtype} (in_stream : cstream, parser : parser(a)) : a =+ let+ val g = parser.modify+ val (s, z) = g(in_stream)+ val _ = stream_vt_free(s)+ val _ = cloptr_free($UN.castvwtp0(g))+ in+ z+ end++fun consume_space() : parser(null) =+ pre_consume_space() where+ { fun pre_consume_space() : parser(null) =+ let+ fnx loop(input : cstream) : (cstream, null) =+ case+ !input of+ | ~stream_vt_cons (' ', xs) => loop(xs)+ | ~stream_vt_cons (_, xs) => (xs, null)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), null)+ in+ @{ modify = llam (input) =<lincloptr1> loop(input) }+ end }++fun consume_int() : parser(token) =+ pre_consume_int() where+ { fun pre_consume_int() : parser(token) =+ let+ fun loop(input : cstream, data : int) : (cstream, int) =+ case+ !input of+ | ~stream_vt_cons ('0', xs) => loop(xs, 10 * data)+ | ~stream_vt_cons ('1', xs) => loop(xs, 10 * data + 1)+ | ~stream_vt_cons ('2', xs) => loop(xs, 10 * data + 2)+ | ~stream_vt_cons ('3', xs) => loop(xs, 10 * data + 3)+ | ~stream_vt_cons ('4', xs) => loop(xs, 10 * data + 4)+ | ~stream_vt_cons ('5', xs) => loop(xs, 10 * data + 5)+ | ~stream_vt_cons ('6', xs) => loop(xs, 10 * data + 6)+ | ~stream_vt_cons ('7', xs) => loop(xs, 10 * data + 7)+ | ~stream_vt_cons ('8', xs) => loop(xs, 10 * data + 8)+ | ~stream_vt_cons ('9', xs) => loop(xs, 10 * data + 9)+ | ~stream_vt_cons (_, xs) => (xs, data)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), data)+ + fun data(input : cstream) : (cstream, token) =+ let+ val (x, y) = loop(input, 0)+ in+ (x, int_tok(y))+ end+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun is_letter(c : char) : bool =+ case+ c of+ | 'a' => true+ | 'b' => true+ | 'c' => true+ | 'd' => true+ | 'e' => true+ | 'f' => true+ | 'g' => true+ | 'h' => true+ | 'i' => true+ | 'j' => true+ | 'k' => true+ | 'l' => true+ | 'm' => true+ | 'n' => true+ | 'o' => true+ | 'p' => true+ | 'q' => true+ | 'r' => true+ | 's' => true+ | 't' => true+ | 'u' => true+ | 'v' => true+ | 'w' => true+ | 'x' => true+ | 'y' => true+ | 'z' => true+ | '-' => true+ | _ => false++fun free_tok(t : token) : void =+ case+ t of+ | ~string_tok (_) => ()+ | ~int_tok (_) => ()+ | ~eq_tok() => ()+ | ~pound_tok() => ()+ | ~float_tok (_) => ()+ | ~bool_tok (_) => ()++fun mk_eq(s : string) : token =+ eq_tok()++// TODO consider list_vt(char)? what would that accomplish/help+// FIXME this is stupid as hell.+fun consume_eq() : parser(token) =+ map(llam x =<lincloptr1> mk_eq(x), pre_consume_identifier()) where+ { fun pre_consume_identifier() : parser(string) =+ let+ fun loop(input : cstream, data : string) : (cstream, string) =+ case+ !input of+ | ~stream_vt_cons ('=', xs) => loop(xs, snoc(data, '='))+ | ~stream_vt_cons (_, xs) => (xs, data)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), "")+ + fun data(input : cstream) : (cstream, string) =+ loop(input, "")+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun consume_identifier() : parser(token) =+ map(llam x =<lincloptr1> string_tok(x), pre_consume_identifier()) where+ { fun pre_consume_identifier() : parser(string) =+ let+ fun loop(input : cstream, data : string) : (cstream, string) =+ case+ !input of+ | ~stream_vt_cons (c, xs) when is_letter(c) => loop(xs, snoc(data, c))+ | ~stream_vt_cons (_, xs) => (xs, data)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), "")+ + fun data(input : cstream) : (cstream, string) =+ loop(input, "")+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun consume_quoted() : parser(token) =+ map(llam x =<lincloptr1> string_tok(x), pre_consume_quoted()) where+ { fun pre_consume_quoted() : parser(string) =+ let+ fun loop(input : cstream, is_escaped : bool, data : string) : (cstream, string) =+ case+ !input of+ | ~stream_vt_cons ('\\', xs) => loop(xs, true, data)+ | ~stream_vt_cons (x, xs) => + begin+ if not(is_escaped) then+ if x = '"' then+ (xs, data)+ else+ loop(xs, false, snoc(data, x))+ else+ loop(xs, false, snoc(data, x))+ end+ | ~stream_vt_nil() => (prerr!("Error: missing \"") ; exit(1) ; ($ldelay(stream_vt_nil), ""))+ + fun data(input : cstream) : (cstream, string) =+ loop(input, false, "")+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun tokenize(input : cstream) : tstream =+ case+ !input of+ | ~stream_vt_cons (x, xs) => (stream_vt_free(xs) ; $ldelay(stream_vt_nil()))+ | ~stream_vt_nil() => $ldelay(stream_vt_nil())++fun display_token(t : token) : void =+ case+ t of+ | ~string_tok (s) => println!(s)+ | ~int_tok (i) => println!(tostring_int(i))+ | ~eq_tok() => println!("=")+ | ~pound_tok() => println!("#")+ | ~float_tok (x) => ()+ | ~bool_tok (b) => ()++implement main0 () =+ let+ var fr = fileref_open_exn("junk1", file_mode_r)+ var stream = streamize_fileref_char(fr)+ val t1: token = run_parser(stream, consume_quoted())+ var fr = fileref_open_exn("junk2", file_mode_r)+ var stream = streamize_fileref_char(fr)+ val t2: token = run_parser(stream, consume_int())+ var fr = fileref_open_exn("junk3", file_mode_r)+ var stream = streamize_fileref_char(fr)+ val t3: token = run_parser(stream, chain(consume_identifier(), chain(consume_eq(), consume_int())))+ in+ (display_token(t1) ; display_token(t2) ; display_token(t3))+ end
+ test/data/toml-parse.out view
@@ -0,0 +1,260 @@+#include "share/atspre_staload.hats"+#include "share/HATS/atslib_staload_libats_libc.hats"++staload UN = "prelude/SATS/unsafe.sats"+staload "src/types.sats"+staload "prelude/basics_sta.sats"+staload "libats/libc/SATS/stdio.sats"+staload "prelude/SATS/string.sats"++fun snoc(s : string, c : char) : string =+ let+ val sc = char2string(c)+ val x = string0_append(s, sc)+ in+ strptr2string(x)+ end++fun next {m:nat} (x : string(m)) : Option_vt(char) =+ if length(x) > 0 then+ Some_vt(string_head(x))+ else+ None_vt++fun stop_plain_string(c : char) : bool =+ case+ c of+ | '\n' => true+ | '#' => true+ | _ => false++fun map {a:vtype}{b:vtype} (f : a -<lincloptr1> b, x : parser(a)) :+ parser(b) =+ let+ val g = x.modify+ in+ @{ modify = llam c =<lincloptr1>+ + begin+ let+ val (y, z): (cstream, a) = g(c)+ val w: b = f(z)+ in+ (cloptr_free($UN.castvwtp0(f)); cloptr_free($UN.castvwtp0(g)); (y, w))+ end+ end }+ end++extern+fun bind {a:vtype}{b:vtype} ( x : parser(a)+ , f : a -<lincloptr1> parser(b)+ ) : parser(b)++fun pure {a:vtype} (x : a) : parser(a) =+ @{ modify = llam c =<lincloptr1> (c, x) }++fun chain {a:vtype}{b:vtype} (x : parser(a), y : parser(b)) :+ parser(b) =+ @{ modify = llam c =<lincloptr1>+ let+ val f = x.modify+ val g = y.modify+ val (pre_res, _) = f(c)+ val (res, y) = g(pre_res)+ val _ = cloptr_free($UN.castvwtp0(f))+ val _ = cloptr_free($UN.castvwtp0(g))+ in+ (res, y)+ end }++fun run_parser {a:vtype} (in_stream : cstream, parser : parser(a)) : a =+ let+ val g = parser.modify+ val (s, z) = g(in_stream)+ val _ = stream_vt_free(s)+ val _ = cloptr_free($UN.castvwtp0(g))+ in+ z+ end++fun consume_space() : parser(null) =+ pre_consume_space() where+ { fun pre_consume_space() : parser(null) =+ let+ fnx loop(input : cstream) : (cstream, null) =+ case+ !input of+ | ~stream_vt_cons (' ', xs) => loop(xs)+ | ~stream_vt_cons (_, xs) => (xs, null)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), null)+ in+ @{ modify = llam (input) =<lincloptr1> loop(input) }+ end }++fun consume_int() : parser(token) =+ pre_consume_int() where+ { fun pre_consume_int() : parser(token) =+ let+ fun loop(input : cstream, data : int) : (cstream, int) =+ case+ !input of+ | ~stream_vt_cons ('0', xs) => loop(xs, 10 * data)+ | ~stream_vt_cons ('1', xs) => loop(xs, 10 * data + 1)+ | ~stream_vt_cons ('2', xs) => loop(xs, 10 * data + 2)+ | ~stream_vt_cons ('3', xs) => loop(xs, 10 * data + 3)+ | ~stream_vt_cons ('4', xs) => loop(xs, 10 * data + 4)+ | ~stream_vt_cons ('5', xs) => loop(xs, 10 * data + 5)+ | ~stream_vt_cons ('6', xs) => loop(xs, 10 * data + 6)+ | ~stream_vt_cons ('7', xs) => loop(xs, 10 * data + 7)+ | ~stream_vt_cons ('8', xs) => loop(xs, 10 * data + 8)+ | ~stream_vt_cons ('9', xs) => loop(xs, 10 * data + 9)+ | ~stream_vt_cons (_, xs) => (xs, data)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), data)+ + fun data(input : cstream) : (cstream, token) =+ let+ val (x, y) = loop(input, 0)+ in+ (x, int_tok(y))+ end+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun is_letter(c : char) : bool =+ case+ c of+ | 'a' => true+ | 'b' => true+ | 'c' => true+ | 'd' => true+ | 'e' => true+ | 'f' => true+ | 'g' => true+ | 'h' => true+ | 'i' => true+ | 'j' => true+ | 'k' => true+ | 'l' => true+ | 'm' => true+ | 'n' => true+ | 'o' => true+ | 'p' => true+ | 'q' => true+ | 'r' => true+ | 's' => true+ | 't' => true+ | 'u' => true+ | 'v' => true+ | 'w' => true+ | 'x' => true+ | 'y' => true+ | 'z' => true+ | '-' => true+ | _ => false++fun free_tok(t : token) : void =+ case+ t of+ | ~string_tok (_) => ()+ | ~int_tok (_) => ()+ | ~eq_tok() => ()+ | ~pound_tok() => ()+ | ~float_tok (_) => ()+ | ~bool_tok (_) => ()++fun mk_eq(s : string) : token =+ eq_tok()++// TODO consider list_vt(char)? what would that accomplish/help+// FIXME this is stupid as hell.+fun consume_eq() : parser(token) =+ map(llam x =<lincloptr1> mk_eq(x), pre_consume_identifier()) where+ { fun pre_consume_identifier() : parser(string) =+ let+ fun loop(input : cstream, data : string) : (cstream, string) =+ case+ !input of+ | ~stream_vt_cons ('=', xs) => loop(xs, snoc(data, '='))+ | ~stream_vt_cons (_, xs) => (xs, data)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), "")+ + fun data(input : cstream) : (cstream, string) =+ loop(input, "")+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun consume_identifier() : parser(token) =+ map( llam x =<lincloptr1> string_tok(x)+ , pre_consume_identifier()+ ) where+ { fun pre_consume_identifier() : parser(string) =+ let+ fun loop(input : cstream, data : string) : (cstream, string) =+ case+ !input of+ | ~stream_vt_cons (c, xs) when is_letter(c) => loop(xs, snoc(data, c))+ | ~stream_vt_cons (_, xs) => (xs, data)+ | ~stream_vt_nil() => ($ldelay(stream_vt_nil), "")+ + fun data(input : cstream) : (cstream, string) =+ loop(input, "")+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun consume_quoted() : parser(token) =+ map(llam x =<lincloptr1> string_tok(x), pre_consume_quoted()) where+ { fun pre_consume_quoted() : parser(string) =+ let+ fun loop(input : cstream, is_escaped : bool, data : string) :+ (cstream, string) =+ case+ !input of+ | ~stream_vt_cons ('\\', xs) => loop(xs, true, data)+ | ~stream_vt_cons (x, xs) => + begin+ if not(is_escaped) then+ if x = '"' then+ (xs, data)+ else+ loop(xs, false, snoc(data, x))+ else+ loop(xs, false, snoc(data, x))+ end+ | ~stream_vt_nil() => ( prerr!("Error: missing \"")+ ; exit(1)+ ; ($ldelay(stream_vt_nil), "")+ )+ + fun data(input : cstream) : (cstream, string) =+ loop(input, false, "")+ in+ @{ modify = llam (input) =<lincloptr1> data(input) }+ end }++fun tokenize(input : cstream) : tstream =+ case+ !input of+ | ~stream_vt_cons (x, xs) => ( stream_vt_free(xs)+ ; $ldelay(stream_vt_nil())+ )+ | ~stream_vt_nil() => $ldelay(stream_vt_nil())++fun display_token(t : token) : void =+ case+ t of+ | ~string_tok (s) => println!(s)+ | ~int_tok (i) => println!(tostring_int(i))+ | ~eq_tok() => println!("=")+ | ~pound_tok() => println!("#")+ | ~float_tok (x) => ()+ | ~bool_tok (b) => ()++implement main0 () =+ let+ var fr = fileref_open_exn("junk1", file_mode_r)+ var stream = streamize_fileref_char(fr)+ val t1: token = run_parser(stream, consume_quoted())+ var fr = fileref_open_exn("junk2", file_mode_r)+ var stream = streamize_fileref_char(fr)+ val t2: token = run_parser(stream, consume_int())+ var fr = fileref_open_exn("junk3", file_mode_r)+ var stream = streamize_fileref_char(fr)+ val t3: token = run_parser( stream+ , chain(consume_identifier(), chain(consume_eq(), consume_int()))+ )+ in+ (display_token(t1) ; display_token(t2) ; display_token(t3))+ end
+ test/data/types.out view
@@ -0,0 +1,24 @@+datavtype null =+ | null++datavtype token =+ | string_tok of string+ | int_tok of int+ | eq_tok+ | pound_tok+ | float_tok of float+ | bool_tok of bool++datavtype error_state =+ | okay+ | error_state of string++vtypedef cstream = stream_vt(char)+vtypedef tstream = stream_vt(token)++datavtype either(a : t@ype, b : t@ype+) =+ | left of a+ | right of b++vtypedef parser(a : vt@ype+) =+ @{ modify = cstream -<lincloptr1> (cstream, a) }
+ test/data/types.sats view
@@ -0,0 +1,23 @@+datavtype null =+ | null++datavtype token =+ | string_tok of string+ | int_tok of int+ | eq_tok+ | pound_tok+ | float_tok of float+ | bool_tok of bool++datavtype error_state =+ | okay+ | error_state of string++vtypedef cstream = stream_vt(char)+vtypedef tstream = stream_vt(token)++datavtype either(a : t@ype, b : t@ype+) =+ | left of a+ | right of b++vtypedef parser(a : vt@ype+) = @{ modify = cstream -<lincloptr1> (cstream, a) }