diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -1,5 +1,5 @@ name: language-ats -version: 0.1.1.12 +version: 0.1.1.13 synopsis: Parser and pretty-printer for ATS. description: Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license: BSD3 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 @@ -123,6 +123,10 @@ | length (showFast d2) >= 30 = d1 <$> indent 4 d2 | otherwise = d1 <+> d2 +prettyArgsProof :: (Pretty a) => Maybe a -> [Doc] -> Doc +prettyArgsProof (Just e) = prettyArgsG ("(" <> pretty e <+> "| ") ")" +prettyArgsProof Nothing = prettyArgs + instance Pretty Expression where pretty = cata a . rewriteATS where a (IfF e e' (Just e'')) = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e'' @@ -150,15 +154,14 @@ a (UnaryF Negate e) = "~" <> e a (NamedValF nam) = pretty nam a (CallF nam [] [] Nothing []) = pretty nam <> "()" - a (CallF nam [] [] (Just e) xs) = pretty nam <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs -- FIXME split eagerly on "|" - a (CallF nam [] [] Nothing xs) = pretty nam <> prettyArgs xs + a (CallF nam [] [] e xs) = pretty nam <> prettyArgsProof e xs a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us - a (CallF nam [] us Nothing xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsG "(" ")" xs + a (CallF nam [] us e xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs a (CallF nam is [] Nothing []) = pretty nam <> prettyImplicits is a (CallF nam is [] Nothing [x]) | startsParens x = pretty nam <> prettyImplicits is <> pretty x - a (CallF nam is [] Nothing xs) = pretty nam <> prettyImplicits is <> prettyArgs xs - a (CallF nam is [] (Just e) xs) = pretty nam <> prettyImplicits is <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs + a (CallF nam is [] e xs) = pretty nam <> prettyImplicits is <> prettyArgsProof e xs + a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs a (CaseF _ add e cs) = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs) a (IfCaseF _ cs) = "ifcase" <$> indent 2 (prettyIfCase cs) a (VoidLiteralF _) = "()" @@ -193,7 +196,6 @@ a (AddrAtF _ e) = "addr@" <> e a (ViewAtF _ e) = "view@" <> e a (ListLiteralF _ s t es) = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es - a CallF{} = undefined a BinListF{} = undefined -- Shouldn't happen prettyImplicits = mconcat . fmap (prettyArgsU "<" ">") . reverse prettyIfCase [] = mempty @@ -465,24 +467,29 @@ (<#>) :: Doc -> Doc -> Doc (<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b) +prettySigG :: (Pretty a) => Doc -> String -> Maybe a -> Doc +prettySigG d si (Just rt) = d <> ":" <> text si <#> pretty rt <> d +prettySigG _ _ _ = mempty + +prettySig :: (Pretty a) => String -> Maybe a -> Doc +prettySig = prettySigG space + +prettyTermetric :: Pretty a => Maybe a -> Doc +prettyTermetric (Just t) = softline <> ".<" <> pretty t <> ">." <> softline +prettyTermetric Nothing = mempty + -- FIXME figure out a nicer algorithm for when/how to split lines. --- aka don't use '' in places. instance Pretty PreFunction where - pretty (PreF i si [] [] NoA (Just rt) Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack - pretty (PreF i si [] [] as (Just rt) Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si [] [] as (Just rt) (Just t) (Just e)) = pretty i ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si [] us as (Just rt) (Just t) (Just e)) = pretty i fancyU us ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si [] us NoA (Just rt) Nothing (Just e)) = pretty i fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si [] us as (Just rt) Nothing (Just e)) = pretty i fancyU us prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si pus [] as (Just rt) Nothing (Just e)) = fancyU pus pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si pus [] as (Just rt) (Just t) (Just e)) = fancyU pus pretty i <+> ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si pus us as (Just rt) (Just t) (Just e)) = fancyU pus pretty i fancyU us ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si pus us as (Just rt) Nothing (Just e)) = fancyU pus pretty i fancyU us prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) - pretty (PreF i si [] [] as (Just rt) Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt - pretty (PreF i si [] us [] (Just rt) Nothing Nothing) = pretty i fancyU us <+> ":" <> text si <#> pretty rt - pretty (PreF i si [] us as (Just rt) Nothing Nothing) = pretty i fancyU us prettyArgs as <+> ":" <> text si <#> pretty rt - pretty (PreF i si pus us as (Just rt) Nothing Nothing) = fancyU pus pretty i fancyU us prettyArgs as <+> ":" <> text si <#> pretty rt - pretty _ = undefined + pretty (PreF i si [] [] NoA rt Nothing (Just e)) = pretty i <> prettySig si rt <> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack + pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e) + pretty (PreF i si [] us NoA rt t (Just e)) = pretty i fancyU us <> prettyTermetric t <> prettySig si rt <> "=" <$> indent 2 (pretty e) + pretty (PreF i si [] us as rt t (Just e)) = pretty i fancyU us <> prettyTermetric t <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus pretty i <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus us as rt t (Just e)) = fancyU pus pretty i fancyU us <> prettyTermetric t <> prettyArgs as <> prettySig si rt <> "=" <$> indent 2 (pretty e) + pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt + pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i fancyU us <+> ":" <> text si <#> pretty rt + pretty (PreF i si [] us as rt Nothing Nothing) = pretty i fancyU us prettyArgs as <+> ":" <> text si <#> pretty rt + pretty (PreF i si pus us as rt t Nothing) = fancyU pus pretty i <> prettyTermetric t fancyU us prettyArgs as <+> ":" <> text si <#> pretty rt instance Pretty DataPropLeaf where pretty (DataPropLeaf us e Nothing) = "|" <+> foldMap pretty (reverse us) <+> pretty e @@ -494,62 +501,77 @@ pretty Pre{} = "prefix" pretty Post{} = "postfix" +prettyMaybeType :: (Pretty a) => Maybe a -> Doc +prettyMaybeType (Just a) = " =" <+> pretty a +prettyMaybeType _ = mempty + +valSig :: (Pretty a) => Maybe a -> Doc +valSig = prettySigG mempty mempty + instance Pretty Declaration where - pretty (AbsType _ s as Nothing) = "abstype" <+> text s <> prettyArgs as - pretty (AbsType _ s as (Just t)) = "abstype" <+> text s <> prettyArgs as <+> "=" <+> pretty t - pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettyArgs as - pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettyArgs as <+> "=" <+> pretty t - pretty (SumViewType s [] ls) = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls - pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls - pretty (SumType s [] ls) = "datatype" <+> text s <+> "=" <$> prettyLeaf ls - pretty (SumType s as ls) = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls - pretty (Impl [] i) = "implement" <+> pretty i - pretty (Impl us i) = "implement" <+> mconcat (fmap pretty us) <+> pretty i - pretty (ProofImpl i) = "primplmnt" <+> pretty i - pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e - pretty (Val a Nothing p e) = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e - pretty (Val a (Just t) p e) = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e - pretty (Var (Just t) p Nothing e) = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e - pretty (Var Nothing p e Nothing) = "var" <+> pretty p <+> "=" <+> pretty e - pretty (Var (Just t) p e Nothing) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e - pretty (Include s) = "#include" <+> pretty s - pretty (Staload b Nothing s) = bool "" "#" b <> "staload" <+> pretty s - pretty (Staload b (Just q) s) = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s - pretty (CBlock s) = string s - pretty (Comment s) = string s - pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n - pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n - pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n' + pretty (AbsType _ s as Nothing) = "abstype" <+> text s <> prettyArgs as + pretty (AbsType _ s as (Just t)) = "abstype" <+> text s <> prettyArgs as <+> "=" <+> pretty t + pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettyArgs as + pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettyArgs as <+> "=" <+> pretty t + pretty (SumViewType s [] ls) = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls + pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls + pretty (SumType s [] ls) = "datatype" <+> text s <+> "=" <$> prettyLeaf ls + pretty (SumType s as ls) = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls + pretty (Impl [] i) = "implement" <+> pretty i + pretty (Impl us i) = "implement" <+> mconcat (fmap pretty us) <+> pretty i + pretty (ProofImpl i) = "primplmnt" <+> pretty i + pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e + pretty (AndDecl t p e) = "and" <+> pretty p <> valSig t <+> "=" <+> pretty e + pretty (Val a t p e) = "val" <> pretty a <+> pretty p <> valSig t <+> "=" <+> pretty e + pretty (Var (Just t) p Nothing (Just e)) = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e + pretty (Var Nothing p e Nothing) = "var" <+> pretty p <+> "=" <+> pretty e + pretty (Var (Just t) p e Nothing) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e + pretty (Var _ _ _ Just{}) = undefined + pretty (Include s) = "#include" <+> pretty s + pretty (Staload b Nothing s) = bool "" "#" b <> "staload" <+> pretty s + pretty (Staload b (Just q) s) = bool "" "#" b <> "staload" <+> pretty q <+> "=" <+> pretty s + pretty (CBlock s) = string s + pretty (Comment s) = string s + pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n + pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n + pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n' -- We use 'text' here, which means indentation might get fucked up for -- C preprocessor macros, but you absolutely deserve it if you indent your -- macros. - pretty (Define s) = text s - pretty (Func _ (Fn pref)) = "fn" pretty pref - pretty (Func _ (Fun pref)) = "fun" pretty pref - pretty (Func _ (CastFn pref)) = "castfn" pretty pref - pretty (Func _ (Fnx pref)) = "fnx" pretty pref - pretty (Func _ (And pref)) = "and" pretty pref - pretty (Func _ (Praxi pref)) = "praxi" pretty pref - pretty (Func _ (PrFun pref)) = "prfun" pretty pref - pretty (Func _ (PrFn pref)) = "prfn" pretty pref - pretty (Extern _ d) = "extern" <$> pretty d - pretty (DataProp _ s as ls) = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls - pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> text s <+> "=" <#> pretty t - pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettyArgs as <+> "=" <#> pretty t - pretty (TypeDef _ s [] t) = "typedef" <+> text s <+> "=" <+> pretty t - pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettyArgs as <+> "=" <+> pretty t - pretty (AbsProp _ n as) = "absprop" <+> text n <+> prettyArgs as - pretty (Assume n NoA e) = "assume" pretty n <+> "=" pretty e - pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e - pretty (SymIntr _ n) = "symintr" <+> pretty n - pretty (Stacst _ n t Nothing) = "stacst" pretty n <+> ":" pretty t - pretty (Stacst _ n t (Just e)) = "stacst" pretty n <+> ":" pretty t <+> "=" pretty e - pretty (PropDef _ s as t) = "propdef" text s <+> prettyArgs as <+> "=" pretty t - pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end" - pretty (FixityDecl f (Left s) ss) = pretty f <+> "(" <> text s <> ")" <+> hsep (fmap text ss) - pretty (FixityDecl f (Right i) ss) = pretty f <+> pretty i <+> hsep (fmap text ss) - pretty (StaVal us i t) = "val" mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t - pretty (Stadef i n []) = "stadef" <+> text i <+> pretty n - pretty (Stadef i n as) = "stadef" <+> text i <+> pretty n <> prettyArgs as - pretty _ = undefined - + pretty (Define s) = text s + pretty (Func _ (Fn pref)) = "fn" pretty pref + pretty (Func _ (Fun pref)) = "fun" pretty pref + pretty (Func _ (CastFn pref)) = "castfn" pretty pref + pretty (Func _ (Fnx pref)) = "fnx" pretty pref + pretty (Func _ (And pref)) = "and" pretty pref + pretty (Func _ (Praxi pref)) = "praxi" pretty pref + pretty (Func _ (PrFun pref)) = "prfun" pretty pref + pretty (Func _ (PrFn pref)) = "prfn" pretty pref + pretty (Extern _ d) = "extern" <$> pretty d + pretty (DataProp _ s as ls) = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls + pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> text s <+> "=" <#> pretty t + pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettyArgs as <+> "=" <#> pretty t + pretty (TypeDef _ s [] t) = "typedef" <+> text s <+> "=" <+> pretty t + pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettyArgs as <+> "=" <+> pretty t + pretty (AbsProp _ n as) = "absprop" <+> text n <+> prettyArgs as + pretty (Assume n NoA e) = "assume" pretty n <+> "=" pretty e + pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e + pretty (SymIntr _ n) = "symintr" <+> pretty n + pretty (Stacst _ n t Nothing) = "stacst" pretty n <+> ":" pretty t + pretty (Stacst _ n t (Just e)) = "stacst" pretty n <+> ":" pretty t <+> "=" pretty e + pretty (PropDef _ s as t) = "propdef" text s <+> prettyArgs as <+> "=" pretty t + pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end" + pretty (FixityDecl f (Left s) ss) = pretty f <+> "(" <> text s <> ")" <+> hsep (fmap text ss) + pretty (FixityDecl f (Right i) ss) = pretty f <+> pretty i <+> hsep (fmap text ss) + pretty (StaVal us i t) = "val" mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t + pretty (Stadef i n []) = "stadef" <+> text i <+> pretty n + pretty (Stadef i n as) = "stadef" <+> text i <+> pretty n <> prettyArgs as + pretty (AbsView _ i as t) = "absview" <+> text i <> prettyArgs as <> prettyMaybeType t + pretty (AbsVT0p _ i as t) = "absvt@ype" <+> text i <> prettyArgs as <> prettyMaybeType t + pretty (AbsT0p _ i t) = "abst@ype" <+> text i <+> "=" <+> pretty t + pretty (ViewDef _ s [] t) = "viewdef" <+> text s <+> "=" <#> pretty t + pretty (ViewDef _ s as t) = "viewdef" <+> text s <> prettyArgs as <+> "=" <#> pretty t + pretty (TKind _ n s) = pretty n <+> "=" <+> text s + pretty (SortDef _ s t) = "sortdef" <+> text s <+> "=" <+> pretty t + pretty (AndD d (SortDef _ i t)) = pretty d <+> "and" <+> text i <+> "=" <+> pretty t + pretty AndD{} = undefined -- probably not valid syntax if we get to this point diff --git a/test/data/cli.out b/test/data/cli.out --- a/test/data/cli.out +++ b/test/data/cli.out @@ -17,7 +17,7 @@ vtypedef parser(a : vt@ype+) = @{ modify = Strptr1 - (a, Strptr1) } -fn run_parser {a:vt@ype+} (p : parser(a), s : Strptr1) : a = +fn run_parser {a:vt@ype+}(p : parser(a), s : Strptr1) : a = let val (x, _) = p.modify(s) in @@ -60,9 +60,9 @@ ; () ) -fun process_short { s : int | s > 0 } ( s : string(s) - , acc : command_line - ) : command_line = +fun process_short { s : int | s > 0 }( s : string(s) + , acc : command_line + ) : command_line = let var str = string_make_substring(s, i2sz(0), i2sz(1)) var acc_r = ref(acc) diff --git a/test/data/combinatorics.out b/test/data/combinatorics.out --- a/test/data/combinatorics.out +++ b/test/data/combinatorics.out @@ -21,13 +21,12 @@ | 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)) : +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 = +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)) : [ n : nat | n > 0 ] intinf(n) = diff --git a/test/data/fact.out b/test/data/fact.out --- a/test/data/fact.out +++ b/test/data/fact.out @@ -12,7 +12,7 @@ (* (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) 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 @@ -16,7 +16,7 @@ | 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 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,13 +19,13 @@ 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. @@ -75,7 +75,7 @@ , r )) -fun get_multiplicity { p : nat | p > 1 } (n : intGte(0), p : int(p)) : +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) diff --git a/test/data/polyglot.out b/test/data/polyglot.out --- a/test/data/polyglot.out +++ b/test/data/polyglot.out @@ -113,9 +113,9 @@ "" // helper function for make_table -fun maybe_table { k : int | k >= 0 && k < 20 } ( s : string(k) - , f : file - ) : string = +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 @@ -920,9 +920,9 @@ | ~margaret _ => () // match a particular word against a list of keywords -fun match_keywords { m : nat | m <= 10 } ( keys : list(string, m) - , word : string - ) : bool = +fun match_keywords { m : nat | m <= 10 }( keys : list(string, m) + , word : string + ) : bool = list_foldright_cloref(keys, lam (next, acc) = acc || eq_string_string(next, word), 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 @@ -49,11 +49,10 @@ , 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)) : - parser(b) = +fun chain {a:vtype}{b:vtype}(x : parser(a), y : parser(b)) : parser(b) = @{ modify = llam c = let val f = x.modify @@ -66,7 +65,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)