diff --git a/ats-format.cabal b/ats-format.cabal --- a/ats-format.cabal +++ b/ats-format.cabal @@ -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 diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 diff --git a/test/data/combinatorics.out b/test/data/combinatorics.out --- a/test/data/combinatorics.out +++ b/test/data/combinatorics.out @@ -7,27 +7,26 @@ staload "contrib/atscntrb-hx-intinf/SATS/intinf.sats" staload UN = "prelude/SATS/unsafe.sats" -fnx fact {n : nat} .. (k : int(n)) : [ n : nat | n > 0 ] intinf(n) = +fnx fact {n:nat} .. (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} .. (k : int(n)) : Intinf = +fnx dfact {n:nat} .. (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 } .. (i : int(m)) : diff --git a/test/data/concurrency.out b/test/data/concurrency.out --- a/test/data/concurrency.out +++ b/test/data/concurrency.out @@ -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(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(xs, x) } diff --git a/test/data/fact.out b/test/data/fact.out --- a/test/data/fact.out +++ b/test/data/fact.out @@ -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} .. ( pf : !int @ l | n : int(n) - , res : ptr(l) - ) : void = + fun loop {n:nat}{l:addr} .. ( pf : !int @ l | n : int(n) + , res : ptr(l) + ) : void = if n > 0 then let val () = !res := n * !res diff --git a/test/data/factorial.out b/test/data/factorial.out --- a/test/data/factorial.out +++ b/test/data/factorial.out @@ -1,4 +1,4 @@ -fun factorial_recursion {n : nat} .. (n : int(n)) : int = +fun factorial_recursion {n:nat} .. (n : int(n)) : int = case+ n of | 0 => 1 | n =>> factorial_recursion(n - 1) * n diff --git a/test/data/fast-combinatorics.out b/test/data/fast-combinatorics.out --- a/test/data/fast-combinatorics.out +++ b/test/data/fast-combinatorics.out @@ -4,19 +4,19 @@ staload "libats/libc/SATS/math.sats" -fnx fact {n : nat} .. (k : int(n)) :<> int = +fnx fact {n:nat} .. (k : int(n)) :<> int = case+ k of | 0 => 1 | k =>> fact(k - 1) * k -fnx dfact {n : nat} .. (k : int(n)) :<> int = +fnx dfact {n:nat} .. (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 } .. (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} .. ( i : int(n) - , bound : int(m) - ) :<> bool = + fun loop {n:nat}{m:nat} .. (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 diff --git a/test/data/left-pad.out b/test/data/left-pad.out --- a/test/data/left-pad.out +++ b/test/data/left-pad.out @@ -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)) diff --git a/test/data/number-theory.out b/test/data/number-theory.out --- a/test/data/number-theory.out +++ b/test/data/number-theory.out @@ -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 } .. ( n : int(k) - , acc : int(m) - ) :<> stream_vt(int) = + fun loop {k:nat}{ m : nat | m > 0 && 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 } .. ( n : int(k) - , acc : int(m) - ) :<> stream_vt(int) = + fun loop {k:nat}{ m : nat | m > 0 && 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 } .. ( n : int(k) - , acc : int(m) - ) :<> int = + fun loop {k:nat}{ m : nat | m > 0 && 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 } .. ( n : int(k) - , acc : int(m) - ) :<> int = + fun loop {k:nat}{ m : nat | m > 0 && 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 } .. ( n : int(k) - , acc : int(m) - ) :<> int = + fun loop {k:nat}{ m : nat | m > 0 && 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) diff --git a/test/data/numerics.out b/test/data/numerics.out --- a/test/data/numerics.out +++ b/test/data/numerics.out @@ -5,7 +5,7 @@ staload "libats/libc/SATS/math.sats" staload UN = "prelude/SATS/unsafe.sats" -fun exp {n : nat} .. (x : int, n : int(n)) :<> int = +fun exp {n:nat} .. (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} .. ( i : int(n) - , bound : int(m) - ) :<> bool = + fun loop {n:nat}{m:nat} .. ( i : int(n) + , bound : int(m) + ) :<> bool = if i < bound then if k % i = 0 then false diff --git a/test/data/toml-parse.out b/test/data/toml-parse.out --- a/test/data/toml-parse.out +++ b/test/data/toml-parse.out @@ -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 - b, x : parser(a)) : +fun map {a:vtype}{b:vtype} (f : a - 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 - parser(b) - ) : parser(b) +fun bind {a:vtype}{b:vtype} ( x : parser(a) + , f : a - parser(b) + ) : parser(b) -fun pure {a : vtype} (x : a) : parser(a) = +fun pure {a:vtype} (x : a) : parser(a) = @{ modify = llam c = (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 = 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)