ats-format 0.1.3.5 → 0.1.3.6
raw patch · 12 files changed
+89/−85 lines, 12 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- ats-format.cabal +1/−1
- src/Language/ATS/PrettyPrint.hs +12/−6
- src/Language/ATS/Types.hs +1/−1
- test/data/combinatorics.out +5/−6
- test/data/concurrency.out +18/−18
- test/data/fact.out +4/−4
- test/data/factorial.out +1/−1
- test/data/fast-combinatorics.out +8/−9
- test/data/left-pad.out +3/−3
- test/data/number-theory.out +24/−23
- test/data/numerics.out +4/−4
- test/data/toml-parse.out +8/−9
ats-format.cabal view
@@ -1,5 +1,5 @@ name: ats-format-version: 0.1.3.5+version: 0.1.3.6 synopsis: A source-code formatter for ATS description: An opinionated source-code formatter for [ATS](http://www.ats-lang.org/). homepage: https://hub.darcs.net/vmchale/ats-format#readme
src/Language/ATS/PrettyPrint.hs view
@@ -241,12 +241,18 @@ a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p a (ExistentialPatternF e p) = pretty e <> p +singleArg :: Arg -> Doc+singleArg = argHelper (<>)++argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc+argHelper _ (Arg (First s)) = pretty s+argHelper _ (Arg (Second t)) = pretty t+argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t+argHelper op (PrfArg a a') = pretty a `op` "|" `op` pretty a'+argHelper _ NoArgs = undefined -- in theory we handle this elsewhere.+ instance Pretty Arg where- pretty (Arg (First s)) = pretty s- pretty (Arg (Second t)) = pretty t- pretty (Arg (Both s t)) = pretty s <+> colon <+> pretty t- pretty (PrfArg a a') = pretty a <+> "|" <+> pretty a'- pretty NoArgs = undefined+ pretty = argHelper (<+>) squish :: BinOp -> Bool squish Add = True@@ -325,7 +331,7 @@ instance Pretty Universal where pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments- pretty (Universal [x] Nothing Nothing) = lbrace <> pretty x <> rbrace -- FIXME universals can now be length-one arguments+ pretty (Universal [x] Nothing Nothing) = lbrace <> singleArg x <> rbrace -- FIXME universals can now be length-one arguments pretty (Universal bs ty Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbrace pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbrace where go (Arg (First s)) = pretty s
src/Language/ATS/Types.hs view
@@ -191,7 +191,7 @@ deriving (Show, Eq, Generic, NFData) -- | Wrapper for existential quantifiers/types-data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe Expression } -- TODO #[id:int] existentials+data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe Expression } deriving (Show, Eq, Generic, NFData) -- | @~@ is used to negate numbers in ATS
test/data/combinatorics.out view
@@ -7,27 +7,26 @@ 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) =+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 =+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 =+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)) :+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)) :
test/data/concurrency.out view
@@ -17,30 +17,30 @@ absprop ISNIL (id : int, b : bool) extern-fun {a : vt0p} queue_is_nil {id : int} (!queue(a, id)) :+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)) :+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}+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}+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)+fun {a:vt0p} queue_make (cap : intGt(0)) : queue(a) extern-fun {a : t@ype} queue_free (que : queue(a)) : void+fun {a:t@ype} queue_free (que : queue(a)) : void assume queue_vtype(a : vt0p, id : int) = deqarray(a) @@ -53,18 +53,18 @@ vtypedef channel(a : vt0p) = channel_vtype(a) extern-fun {a : vt0p} channel_insert (!channel(a), a) : void+fun {a:vt0p} channel_insert (!channel(a), a) : void extern-fun {a : vt0p} channel_remove (chan : !channel(a)) : a+fun {a:vt0p} channel_remove (chan : !channel(a)) : a extern-fun {a : vt0p} channel_remove_helper ( chan : !channel(a)- , !queue(a) >> _- ) : a+fun {a:vt0p} channel_remove_helper ( chan : !channel(a)+ , !queue(a) >> _+ ) : a extern-fun {a : vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) :+fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) : void datavtype channel_ =@@ -78,16 +78,16 @@ } extern-fun {a : vt0p} channel_make (cap : intGt(0)) : channel(a)+fun {a:vt0p} channel_make (cap : intGt(0)) : channel(a) extern-fun {a : vt0p} channel_ref (ch : !channel(a)) : channel(a)+fun {a:vt0p} channel_ref (ch : !channel(a)) : channel(a) extern-fun {a : vt0p} channel_unref (ch : channel(a)) : Option_vt(queue(a))+fun {a:vt0p} channel_unref (ch : channel(a)) : Option_vt(queue(a)) extern-fun channel_refcount {a : vt0p} (ch : !channel(a)) : intGt(0)+fun channel_refcount {a:vt0p} (ch : !channel(a)) : intGt(0) assume channel_vtype(a : vt0p) = channel_ @@ -101,7 +101,7 @@ let prval () = __assert(prf) where { extern- praxi __assert {id : int} (p : ISNIL(id, false)) : [ false ] void }+ praxi __assert {id:int} (p : ISNIL(id, false)) : [ false ] void } in deqarray_takeout_atbeg<a>(xs) end@@ -110,7 +110,7 @@ { prval () = __assert(prf) where { extern- praxi __assert {id : int} (p : ISFULL(id, false)) : [ false ] void }+ praxi __assert {id:int} (p : ISFULL(id, false)) : [ false ] void } val () = deqarray_insert_atend<a>(xs, x) }
test/data/fact.out view
@@ -12,11 +12,11 @@ (* (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 =+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 =+ 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
test/data/factorial.out view
@@ -1,4 +1,4 @@-fun factorial_recursion {n : nat} .<n>. (n : int(n)) : int =+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.out view
@@ -4,19 +4,19 @@ staload "libats/libc/SATS/math.sats" -fnx fact {n : nat} .<n>. (k : int(n)) :<> int =+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 =+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 =+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@@ -45,9 +45,8 @@ 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 =+ 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@@ -67,15 +66,15 @@ end extern-fun choose_ats {n : nat}{ m : nat | m <= n } : (int(n), int(m)) -> int =+fun choose_ats {n:nat}{ m : nat | m <= n } : (int(n), int(m)) -> int = "mac#" extern-fun double_factorial {n : nat} : int(n) -> int =+fun double_factorial {n:nat} : int(n) -> int = "mac#" extern-fun factorial_ats {n : nat} : int(n) -> int =+fun factorial_ats {n:nat} : int(n) -> int = "mac#" extern
test/data/left-pad.out view
@@ -11,7 +11,7 @@ ) : [ cushion : nat ] (PAD(p, l, cushion) | strnptr(cushion+l)) extern-fun {t : t@ype} fill_list {n : nat} (size : ssize_t(n), c : t) :+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) =@@ -58,10 +58,10 @@ (let prval _ = lemma_not_empty(s) where { extern- praxi lemma_not_empty {n : int} (x : string(n)) : [ n > 0 ] void }+ 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 }+ 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))
test/data/number-theory.out view
@@ -19,21 +19,21 @@ fn divides(m : int, n : int) :<> bool = n % m = 0 -fnx gcd {k : nat}{l : nat} (m : int(l), n : int(k)) : int =+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 =+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) =+ 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@@ -48,9 +48,9 @@ // 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) =+ 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@@ -70,9 +70,10 @@ 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))+ | { 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 =@@ -82,9 +83,9 @@ 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 =+ 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@@ -98,9 +99,9 @@ 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 =+ 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@@ -118,9 +119,9 @@ // 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 =+ 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@@ -180,6 +181,6 @@ end extern-fun chinese_remainder {n : nat} ( residues : list_vt(int, n)- , moduli : list_vt(int, n)- ) : Option_vt(int)+fun chinese_remainder {n:nat} ( residues : list_vt(int, n)+ , moduli : list_vt(int, n)+ ) : Option_vt(int)
test/data/numerics.out view
@@ -5,7 +5,7 @@ staload "libats/libc/SATS/math.sats" staload UN = "prelude/SATS/unsafe.sats" -fun exp {n : nat} .<n>. (x : int, n : int(n)) :<> int =+fun exp {n:nat} .<n>. (x : int, n : int(n)) :<> int = case+ x of | 0 => 0 | x => @@ -41,9 +41,9 @@ | k => begin let- fun loop {n : nat}{m : nat} .<max(0,m-n)>. ( i : int(n)- , bound : int(m)- ) :<> bool =+ 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
test/data/toml-parse.out view
@@ -15,7 +15,7 @@ strptr2string(x) end -fun next {m : nat} (x : string(m)) : Option_vt(char) =+fun next {m:nat} (x : string(m)) : Option_vt(char) = if length(x) > 0 then Some_vt(string_head(x)) else@@ -27,7 +27,7 @@ | '#' => true | _ => false -fun map {a : vtype}{b : vtype} (f : a -<lincloptr1> b, x : parser(a)) :+fun map {a:vtype}{b:vtype} (f : a -<lincloptr1> b, x : parser(a)) : parser(b) = let val g = x.modify@@ -45,14 +45,14 @@ end extern-fun bind {a : vtype}{b : vtype} ( x : parser(a)- , f : a -<lincloptr1> parser(b)- ) : parser(b)+fun bind {a:vtype}{b:vtype} ( x : parser(a)+ , f : a -<lincloptr1> parser(b)+ ) : parser(b) -fun pure {a : vtype} (x : a) : parser(a) =+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)) :+fun chain {a:vtype}{b:vtype} (x : parser(a), y : parser(b)) : parser(b) = @{ modify = llam c =<lincloptr1> let@@ -66,8 +66,7 @@ (res, y) end } -fun run_parser {a : vtype} (in_stream : cstream, parser : parser(a)) :- a =+fun run_parser {a:vtype} (in_stream : cstream, parser : parser(a)) : a = let val g = parser.modify val (s, z) = g(in_stream)