ats-format 0.1.3.6 → 0.2.0.0

raw patch · 12 files changed

+81/−59 lines, 12 filesdep ~htoml-megaparsecPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: htoml-megaparsec

API changes (from Hackage documentation)

Files

• Justfile +1/−1
• ats-format.cabal +1/−1
• src/Language/ATS.hs +11/−1
• src/Language/ATS/Parser.y +16/−11
• src/Language/ATS/PrettyPrint.hs +19/−19
• src/Language/ATS/Types.hs +12/−4
• test/data/concurrency.out +10/−11
• test/data/fast-combinatorics.out +2/−2
• test/data/filetype.out +2/−2
• test/data/left-pad.out +2/−2
• test/data/number-theory.out +2/−2
• test/data/numerics.out +3/−3

@@ -63,7 +63,7 @@     cd polyglot && atsfmt src/concurrency.dats -i     cd polyglot && atsfmt src/shared.dats -i     cd polyglot && atsfmt src/filetype.sats -i-    cd polyglot && ./shake.hs+    cd polyglot && ./bash/setup.sh && ./build     @rm -rf polyglot  size:

@@ -1,5 +1,5 @@ name:                ats-format-version:             0.1.3.6+version:             0.2.0.0 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

@@ -1,10 +1,12 @@ -- | Main module for the library-module Language.ATS ( -- * Functions+module Language.ATS ( -- * Functions for working with syntax                       lexATS                     , parseATS                     , printATS                     , printATSCustom                     , printATSFast+                    -- * Library functions+                    , getDependencies                     -- * Syntax Tree                     , ATS (..)                     , Declaration (..)@@ -36,6 +38,7 @@                     -- * Lenses                     , leaves                     , constructorUniversals+                    -- * Library functions                     -- * Executable                     , exec                     ) where@@ -45,3 +48,10 @@ import           Language.ATS.Parser import           Language.ATS.PrettyPrint import           Language.ATS.Types+import Data.Maybe (catMaybes)++getDependencies :: ATS -> [FilePath]+getDependencies (ATS ds) = catMaybes (g <$> ds)+    where g (Staload _ s) = Just s+          g (Include s) = Just s+          g _ = Nothing

@@ -430,12 +430,12 @@           | dollar {% Left $ Expected $1 "$" "Termination metric" }  -- | Parse an existential quantier on a type-Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 False Nothing (Just $4) }+Existential : lsqbracket Args vbar StaticExpression rsqbracket { Existential $2 False Nothing (Just $4) }             | lsqbracket Args rsqbracket { Existential $2 False Nothing Nothing }             | openExistential Args rsqbracket { Existential $2 True Nothing Nothing }-            | openExistential Args vbar Expression rsqbracket { Existential $2 True Nothing (Just $4) }+            | openExistential Args vbar StaticExpression rsqbracket { Existential $2 True Nothing (Just $4) }             | lsqbracket Args colon Type rsqbracket { Existential $2 False (Just $4) Nothing } -- FIXME arguments should include more than just ':'-            | lsqbracket Expression rsqbracket { Existential [] False Nothing (Just $2) }+            | lsqbracket StaticExpression rsqbracket { Existential [] False Nothing (Just $2) }              -- | Parse a universal quantifier on a type Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }@@ -548,13 +548,16 @@ Signature : signature { $1 }           | colon { "" } +OptType : Type { Just $1 }+        | { Nothing }+ -- | Parse a type signature and optional function body-PreFunction : FunName openParen FullArgs closeParen Signature Type OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }-            | FunName Universals OptTermetric Signature Type OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }-            | FunName Universals OptTermetric doubleParens Signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }-            | FunName Universals OptTermetric openParen FullArgs closeParen Signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }-            | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }-            | Universals FunName Universals OptTermetric Signature Type OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }+PreFunction : FunName openParen FullArgs closeParen Signature OptType OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }+            | FunName Universals OptTermetric Signature OptType OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }+            | FunName Universals OptTermetric doubleParens Signature OptType OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }+            | FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }+            | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }+            | Universals FunName Universals OptTermetric Signature OptType OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }             | prval {% Left $ Expected $1 "Function signature" "prval" }             | var {% Left $ Expected $1 "Function signature" "var" }             | val {% Left $ Expected (token_posn $1) "Function signature" "val" }@@ -629,6 +632,8 @@           | Operators Operator { $2 : $1 }           | Operators identifier { to_string $2 : $1 } +StackFunction : openParen Args closeParen Signature Type plainArrow Expression { StackF $4 $2 $5 $7 }+ -- | Parse a declaration Declaration : include string { Include $2 }             | define { Define $1 }@@ -646,8 +651,8 @@             | val Pattern eq Expression { Val (get_addendum $1) Nothing $2 $4 }             | var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing }             | var Pattern colon Type { Var (Just $4) $2 Nothing Nothing }-            | var Pattern eq fixAt IdentifierOr openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt (PreF (Unqualified $5) $9 [] [] $7 $10 Nothing (Just $12))) Nothing }-            | var Pattern eq lambdaAt openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (PreF (Unnamed $4) $8 [] [] $6 $9 Nothing (Just $11))) Nothing }+            | var Pattern eq fixAt IdentifierOr openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt $5 undefined) Nothing }+            | var Pattern eq lambdaAt openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (undefined)) Nothing }             | prval Pattern eq Expression { PrVal $2 $4 }             | praxi PreFunction { Func $1 (Praxi $2) }             | primplmnt Implementation { ProofImpl $2 }

@@ -206,14 +206,12 @@         a (BeginF _ e)             | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")             | otherwise = e-        a (FixAtF (PreF n s [] [] as t Nothing (Just e))) = "fix@" <+> pretty n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)-        a (LambdaAtF (PreF Unnamed{} s [] [] as t Nothing (Just e))) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)+        a (FixAtF n (StackF s as t e)) = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)+        a (LambdaAtF (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)         a (AddrAtF _ e)                = "addr@" <> e         a (ViewAtF _ e)                = "view@" <> e         a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es         a BinListF{} = undefined-        a FixAtF{} = undefined-        a LambdaAtF{} = undefined         a CallF{} = undefined         prettyCases []              = mempty         prettyCases [(s, l, t)]     = "|" <+> pretty s <+> pretty l <+> t@@ -242,7 +240,8 @@         a (ExistentialPatternF e p)    = pretty e <> p  singleArg :: Arg -> Doc-singleArg = argHelper (<>)+singleArg x@Arg{} = argHelper (<>) x+singleArg x       = pretty x  argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc argHelper _ (Arg (First s))   = pretty s@@ -322,6 +321,7 @@  instance Pretty Existential where     pretty (Existential [] b Nothing (Just e)) = withHashtag b <+> pretty e <+> rbracket+    pretty (Existential [x@Arg{}] b Nothing Nothing) = withHashtag b <> singleArg x <> rbracket     pretty (Existential bs b ty Nothing)  = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket     pretty (Existential bs b ty (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket         where go (Arg (First s))  = pretty s@@ -476,20 +476,20 @@ -- 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 [] [] [NoArgs] 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 rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] [] as 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 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 [NoArgs] rt Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si pus [] as 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 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 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 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 Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt+    pretty (PreF i si [] [] [NoArgs] (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 [NoArgs] (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  instance Pretty DataPropLeaf where

@@ -37,6 +37,7 @@     , StaticExpression (..)     , StaticExpressionF (..)     , Fixity (..)+    , StackFunction (..)     , rewriteATS     , rewriteDecl     -- * Lenses@@ -191,7 +192,7 @@     deriving (Show, Eq, Generic, NFData)  -- | Wrapper for existential quantifiers/types-data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe Expression }+data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe StaticExpression }     deriving (Show, Eq, Generic, NFData)  -- | @~@ is used to negate numbers in ATS@@ -277,8 +278,8 @@                 | Begin AlexPosn Expression                 | BinList { _op :: BinOp, _exprs :: [Expression] }                 | PrecedeList { _exprs :: [Expression] }-                | FixAt PreFunction-                | LambdaAt PreFunction+                | FixAt String StackFunction+                | LambdaAt StackFunction                 | ParenExpr AlexPosn Expression                 deriving (Show, Eq, Generic, NFData) @@ -304,12 +305,19 @@               | CastFn PreFunction               deriving (Show, Eq, Generic, NFData) +data StackFunction = StackF { stSig        :: String+                            , stArgs       :: [Arg]+                            , stReturnType :: Type+                            , stExpression :: Expression+                            }+                            deriving (Show, Eq, Generic, NFData)+ data PreFunction = PreF { fname         :: Name -- ^ Function name                         , sig           :: String -- ^ e.g. <> or \<!wrt>                         , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic                         , universals    :: [Universal] -- ^ Universal quantifiers/refinement type                         , args          :: [Arg] -- ^ Actual function arguments-                        , returnType    :: Type -- ^ Return type+                        , returnType    :: Maybe Type -- ^ Return type                         , termetric     :: Maybe StaticExpression -- ^ Optional termination metric                         , expression    :: Maybe Expression -- ^ Expression holding the actual function body (not present in static templates)                         }

@@ -12,29 +12,28 @@ 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)+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))+  [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))+  [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+  #[id2:int] void  extern fun {a:vt0p} queue_remove {id:int}-(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) :-  #[ id2 : int ] a+(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a  extern fun {a:vt0p} queue_make  (cap : intGt(0)) : queue(a)@@ -172,12 +171,12 @@ implement {a} channel_make (cap) =   let     extern-    praxi __assert() : [ l : agz ] void+    praxi __assert() : [l:agz] void     -    prval [ l0 : addr ]() = __assert()-    prval [ l1 : addr ]() = __assert()-    prval [ l2 : addr ]() = __assert()-    prval [ l3 : addr ]() = __assert()+    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

@@ -31,7 +31,7 @@   end  // FIXME-fun bad(n : int) : [ m : nat ] int(m) =+fun bad(n : int) : [m:nat] int(m) =   case+ n of     | 0 => 0     | n => 1 + bad(n - 1)@@ -43,7 +43,7 @@       begin         let           var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))-          var bound: [ m : nat ] int(m) = bad(pre_bound)+          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 =

@@ -5,8 +5,8 @@ typedef command_line = @{ version = bool                         , help = bool                         , table = bool-                        , excludes = [ m : nat ] list(string, m)-                        , includes = [ m : nat ] list(string, m)+                        , excludes = [m:nat] list(string, m)+                        , includes = [m:nat] list(string, m)                         }  // Program state, tracking *all* supported file types in an unboxed structure.

@@ -8,7 +8,7 @@ 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))+                                             ) : [cushion:nat] (PAD(p, l, cushion) | strnptr(cushion+l))  extern fun {t:t@ype} fill_list {n:nat} (size : ssize_t(n), c : t) :@@ -51,7 +51,7 @@     val _ = if list_vt_length(args) = 3 then       (let         val c = '0'-        val s = g1ofg0(args[1]) : [ n : nat ] string(n)+        val s = g1ofg0(args[1]) : [n:nat] string(n)         val pad = g1ofg0(g0string2int(args[2]))       in         if length(s) > 0 && pad > 0 then

@@ -9,8 +9,8 @@  // 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)+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 =

@@ -24,13 +24,13 @@           1       end -castfn lemma_bounded(i : int) : [ n : nat ] int(n) =+castfn lemma_bounded(i : int) : [n:nat] int(n) =   $UN.cast(i) -fun sqrt_bad(k : intGt(0)) : [ m : nat ] int(m) =+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)+    var bound: [m:nat] int(m) = lemma_bounded(pre_bound)   in     bound   end