packages feed

language-ats 0.1.1.12 → 0.1.1.13

raw patch · 9 files changed

+122/−102 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

language-ats.cabal view
@@ -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
src/Language/ATS/PrettyPrint.hs view
@@ -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
test/data/cli.out view
@@ -17,7 +17,7 @@ vtypedef parser(a : vt@ype+) =   @{ modify = Strptr1 -<lincloptr1> (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<command_line>(acc)
test/data/combinatorics.out view
@@ -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 } .<m>. (i : int(m)) :       [ n : nat | n > 0 ] intinf(n) =
test/data/fact.out view
@@ -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} .<n>. ( pf : !int @ l | n : int(n)                                    , res : ptr(l)
test/data/fast-combinatorics.out view
@@ -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 } .<m>. (i : int(m)) : int =       case+ i of
test/data/number-theory.out view
@@ -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)
test/data/polyglot.out view
@@ -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) =<cloref1> acc                        || eq_string_string(next, word), 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@@ -49,11 +49,10 @@                             , 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)) :-  parser(b) =+fun chain {a:vtype}{b:vtype}(x : parser(a), y : parser(b)) : parser(b) =   @{ modify = llam c =<lincloptr1>                 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)