mirror of
https://github.com/anoma/juvix.git
synced 2024-10-26 17:52:17 +03:00
Fix remove unexpected whitespaces introduced by formatting (#2489)
- Closes #2059
This commit is contained in:
parent
145f20fc68
commit
47c8df11f1
@ -4,10 +4,9 @@ import Commands.Base
|
||||
import Commands.Format.Options
|
||||
import Data.Text qualified as Text
|
||||
import Juvix.Formatter
|
||||
import Juvix.Prelude.Pretty
|
||||
|
||||
data FormatNoEditRenderMode
|
||||
= ReformattedFile (NonEmpty AnsiText)
|
||||
= ReformattedFile Text
|
||||
| InputPath (Path Abs File)
|
||||
| Silent
|
||||
|
||||
@ -72,9 +71,9 @@ renderModeFromOptions target opts formattedInfo
|
||||
| opts ^. formatInPlace = whenContentsModified (EditInPlace formattedInfo)
|
||||
| opts ^. formatCheck = NoEdit Silent
|
||||
| otherwise = case target of
|
||||
TargetFile {} -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContentsAnsi))
|
||||
TargetFile {} -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContents))
|
||||
TargetProject {} -> whenContentsModified (NoEdit (InputPath (formattedInfo ^. formattedFileInfoPath)))
|
||||
TargetStdin -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContentsAnsi))
|
||||
TargetStdin -> NoEdit (ReformattedFile (formattedInfo ^. formattedFileInfoContents))
|
||||
where
|
||||
whenContentsModified :: FormatRenderMode -> FormatRenderMode
|
||||
whenContentsModified res
|
||||
@ -91,9 +90,9 @@ renderFormattedOutput target opts fInfo = do
|
||||
EditInPlace i@FormattedFileInfo {..} ->
|
||||
runTempFileIO
|
||||
. restoreFileOnError _formattedFileInfoPath
|
||||
$ writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText)
|
||||
$ writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContents)
|
||||
NoEdit m -> case m of
|
||||
ReformattedFile ts -> forM_ ts renderStdOut
|
||||
ReformattedFile ts -> renderStdOut ts
|
||||
InputPath p -> say (pack (toFilePath p))
|
||||
Silent -> return ()
|
||||
|
||||
|
@ -36,6 +36,7 @@ import Juvix.Compiler.Pipeline.Package.Loader.EvalEff.IO
|
||||
import Juvix.Compiler.Pipeline.Repl
|
||||
import Juvix.Compiler.Pipeline.Run
|
||||
import Juvix.Compiler.Pipeline.Setup (entrySetup)
|
||||
import Juvix.Data.CodeAnn (Ann)
|
||||
import Juvix.Data.Effect.Git
|
||||
import Juvix.Data.Effect.Process
|
||||
import Juvix.Data.Error.GenericError qualified as Error
|
||||
@ -308,9 +309,9 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
|
||||
printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl ()
|
||||
printDoc = \case
|
||||
Nothing -> do
|
||||
s' <- ppConcrete s
|
||||
renderOut (mkAnsiText @Text "No documentation available for ")
|
||||
renderOutLn s'
|
||||
let s' :: Doc Ann = pretty s
|
||||
msg = "No documentation available for" <+> s'
|
||||
renderOutLn (toAnsiText True msg)
|
||||
Just ju -> printConcrete ju
|
||||
|
||||
getDocFunction :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
|
||||
|
@ -15,7 +15,7 @@ ppOutDefaultNoComments :: (PrettyPrint c) => c -> AnsiText
|
||||
ppOutDefaultNoComments = mkAnsiText . PPOutput . docNoComments defaultOptions
|
||||
|
||||
ppOutDefault :: (HasLoc c, PrettyPrint c) => Comments -> c -> AnsiText
|
||||
ppOutDefault cs = mkAnsiText . PPOutput . doc defaultOptions cs
|
||||
ppOutDefault cs = mkAnsiText . PPOutput . docDefault cs
|
||||
|
||||
ppOut :: (CanonicalProjection a Options, PrettyPrint c, HasLoc c) => a -> Comments -> c -> AnsiText
|
||||
ppOut o cs = mkAnsiText . PPOutput . doc (project o) cs
|
||||
|
@ -70,6 +70,9 @@ doc opts cs x = docHelper (Just (fileComments file cs)) opts x
|
||||
file :: Path Abs File
|
||||
file = getLoc x ^. intervalFile
|
||||
|
||||
docDefault :: (PrettyPrint c, HasLoc c) => Comments -> c -> Doc Ann
|
||||
docDefault cs = doc defaultOptions cs
|
||||
|
||||
ppModulePathType ::
|
||||
forall t s r.
|
||||
(SingI t, SingI s, Members '[ExactPrint, Reader Options] r) =>
|
||||
|
@ -1,19 +1,18 @@
|
||||
module Juvix.Formatter where
|
||||
|
||||
import Data.List.NonEmpty qualified as NonEmpty
|
||||
import Data.Text qualified as T
|
||||
import Juvix.Compiler.Concrete.Language
|
||||
import Juvix.Compiler.Concrete.Print (ppOutDefault)
|
||||
import Juvix.Compiler.Concrete.Print (docDefault)
|
||||
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
|
||||
import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context
|
||||
import Juvix.Compiler.Pipeline.EntryPoint
|
||||
import Juvix.Data.CodeAnn
|
||||
import Juvix.Extra.Paths
|
||||
import Juvix.Prelude
|
||||
import Juvix.Prelude.Pretty
|
||||
|
||||
data FormattedFileInfo = FormattedFileInfo
|
||||
{ _formattedFileInfoPath :: Path Abs File,
|
||||
_formattedFileInfoContentsAnsi :: NonEmpty AnsiText,
|
||||
_formattedFileInfoContents :: Text,
|
||||
_formattedFileInfoContentsModified :: Bool
|
||||
}
|
||||
|
||||
@ -40,18 +39,6 @@ instance Semigroup FormatResult where
|
||||
instance Monoid FormatResult where
|
||||
mempty = FormatResultOK
|
||||
|
||||
combineResults :: [FormatResult] -> FormatResult
|
||||
combineResults = mconcat
|
||||
|
||||
ansiPlainText :: NonEmpty AnsiText -> Text
|
||||
ansiPlainText = T.concat . toList . fmap toPlainText
|
||||
|
||||
formattedFileInfoContentsText :: SimpleGetter FormattedFileInfo Text
|
||||
formattedFileInfoContentsText = to infoToPlainText
|
||||
where
|
||||
infoToPlainText :: FormattedFileInfo -> Text
|
||||
infoToPlainText fInfo = ansiPlainText (fInfo ^. formattedFileInfoContentsAnsi)
|
||||
|
||||
-- | Format a single Juvix file.
|
||||
--
|
||||
-- If the file requires formatting then the function returns 'FormatResultNotFormatted'.
|
||||
@ -68,7 +55,7 @@ format ::
|
||||
format p = do
|
||||
originalContents <- readFile' p
|
||||
runReader originalContents $ do
|
||||
formattedContents <- formatPath p
|
||||
formattedContents :: Text <- formatPath p
|
||||
formatResultFromContents formattedContents p
|
||||
|
||||
-- | Format a Juvix project.
|
||||
@ -102,13 +89,16 @@ formatProject p = do
|
||||
Sem r (FormatResult, Recurse Rel)
|
||||
handler cd _ files res = do
|
||||
let juvixFiles = [cd <//> f | f <- files, isJuvixFile f]
|
||||
subRes <- combineResults <$> mapM format juvixFiles
|
||||
subRes <- mconcat <$> mapM format juvixFiles
|
||||
return (res <> subRes, RecurseFilter (\hasJuvixYaml d -> not hasJuvixYaml && not (isHiddenDirectory d)))
|
||||
|
||||
formatPath :: (Members '[Reader Text, ScopeEff] r) => Path Abs File -> Sem r (NonEmpty AnsiText)
|
||||
formatPath ::
|
||||
(Members '[Reader Text, ScopeEff] r) =>
|
||||
Path Abs File ->
|
||||
Sem r Text
|
||||
formatPath p = do
|
||||
res <- scopeFile p
|
||||
formatScoperResult res
|
||||
formatScoperResult False res
|
||||
|
||||
formatStdin ::
|
||||
forall r.
|
||||
@ -118,19 +108,19 @@ formatStdin = do
|
||||
res <- scopeStdin
|
||||
let originalContents = fromMaybe "" (res ^. Scoper.resultParserResult . resultEntry . entryPointStdin)
|
||||
runReader originalContents $ do
|
||||
formattedContents <- formatScoperResult res
|
||||
formattedContents :: Text <- formatScoperResult False res
|
||||
formatResultFromContents formattedContents formatStdinPath
|
||||
|
||||
formatResultFromContents ::
|
||||
forall r.
|
||||
(Members '[Reader Text, Output FormattedFileInfo] r) =>
|
||||
NonEmpty AnsiText ->
|
||||
Text ->
|
||||
Path Abs File ->
|
||||
Sem r FormatResult
|
||||
formatResultFromContents formattedContents filepath = do
|
||||
originalContents <- ask
|
||||
if
|
||||
| originalContents /= ansiPlainText formattedContents -> mkResult FormatResultNotFormatted
|
||||
| originalContents /= formattedContents -> mkResult FormatResultNotFormatted
|
||||
| otherwise -> mkResult FormatResultOK
|
||||
where
|
||||
mkResult :: FormatResult -> Sem r FormatResult
|
||||
@ -138,31 +128,42 @@ formatResultFromContents formattedContents filepath = do
|
||||
output
|
||||
( FormattedFileInfo
|
||||
{ _formattedFileInfoPath = filepath,
|
||||
_formattedFileInfoContentsAnsi = formattedContents,
|
||||
_formattedFileInfoContents = formattedContents,
|
||||
_formattedFileInfoContentsModified = res == FormatResultNotFormatted
|
||||
}
|
||||
)
|
||||
return res
|
||||
|
||||
formatScoperResult :: (Members '[Reader Text] r) => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText)
|
||||
formatScoperResult res = do
|
||||
formatScoperResult' ::
|
||||
Bool -> Text -> Scoper.ScoperResult -> Text
|
||||
formatScoperResult' force original sres =
|
||||
run . runReader original $ formatScoperResult force sres
|
||||
|
||||
formatScoperResult ::
|
||||
(Members '[Reader Text] r) =>
|
||||
Bool ->
|
||||
Scoper.ScoperResult ->
|
||||
Sem r Text
|
||||
formatScoperResult force res = do
|
||||
let cs = res ^. Scoper.comments
|
||||
formattedModules <-
|
||||
runReader cs
|
||||
. mapM formatTopModule
|
||||
$ res ^. Scoper.resultModules
|
||||
$ res
|
||||
^. Scoper.resultModules
|
||||
let txt :: Text = toPlainTextTrim . mconcat . NonEmpty.toList $ formattedModules
|
||||
|
||||
case res ^. Scoper.mainModule . modulePragmas of
|
||||
Just pragmas ->
|
||||
case pragmas ^. withLocParam . withSourceValue . pragmasFormat of
|
||||
Just PragmaFormat {..}
|
||||
| not _pragmaFormat ->
|
||||
NonEmpty.singleton . mkAnsiText @Text <$> ask
|
||||
| not _pragmaFormat && not force -> ask @Text
|
||||
_ ->
|
||||
return formattedModules
|
||||
return txt
|
||||
Nothing ->
|
||||
return formattedModules
|
||||
return txt
|
||||
where
|
||||
formatTopModule :: (Members '[Reader Comments] r) => Module 'Scoped 'ModuleTop -> Sem r AnsiText
|
||||
formatTopModule :: (Members '[Reader Comments] r) => Module 'Scoped 'ModuleTop -> Sem r (Doc Ann)
|
||||
formatTopModule m = do
|
||||
cs <- ask
|
||||
return (ppOutDefault cs m)
|
||||
cs :: Comments <- ask
|
||||
return $ docDefault cs m
|
||||
|
@ -123,6 +123,14 @@ toAnsiText useColors
|
||||
toPlainText :: (HasTextBackend a) => a -> Text
|
||||
toPlainText = Text.renderStrict . toTextStream
|
||||
|
||||
toPlainTextTrim :: (HasTextBackend a) => a -> Text
|
||||
toPlainTextTrim =
|
||||
Text.unlines
|
||||
. map Text.stripEnd
|
||||
. dropWhile Text.null
|
||||
. Text.lines
|
||||
. toPlainText
|
||||
|
||||
prettyText :: (Pretty a) => a -> Text
|
||||
prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
|
||||
|
||||
@ -157,31 +165,31 @@ hsepMaybe l
|
||||
| null l = Nothing
|
||||
| otherwise = Just (hsep l)
|
||||
|
||||
nest' :: Doc ann -> Doc ann
|
||||
nest' :: Doc a -> Doc a
|
||||
nest' = nest 2
|
||||
|
||||
indent' :: Doc ann -> Doc ann
|
||||
indent' :: Doc a -> Doc a
|
||||
indent' = indent 2
|
||||
|
||||
hang' :: Doc ann -> Doc ann
|
||||
hang' :: Doc a -> Doc a
|
||||
hang' = hang 2
|
||||
|
||||
spaceOrEmpty :: Doc ann
|
||||
spaceOrEmpty :: Doc a
|
||||
spaceOrEmpty = flatAlt (pretty ' ') mempty
|
||||
|
||||
oneLineOrNext :: Doc ann -> Doc ann
|
||||
oneLineOrNext :: Doc a -> Doc a
|
||||
oneLineOrNext x = PP.group (flatAlt (line <> indent' x) (space <> x))
|
||||
|
||||
oneLineOrNextNoIndent :: Doc ann -> Doc ann
|
||||
oneLineOrNextNoIndent :: Doc a -> Doc a
|
||||
oneLineOrNextNoIndent x = PP.group (flatAlt (line <> x) (space <> x))
|
||||
|
||||
oneLineOrNextBlock :: Doc ann -> Doc ann
|
||||
oneLineOrNextBlock :: Doc a -> Doc a
|
||||
oneLineOrNextBlock x = PP.group (flatAlt (line <> indent' x <> line) (space <> x <> space))
|
||||
|
||||
oneLineOrNextBraces :: Doc ann -> Doc ann
|
||||
oneLineOrNextBraces :: Doc a -> Doc a
|
||||
oneLineOrNextBraces x = PP.group (flatAlt (lbrace <> line <> indent' x <> line <> rbrace) (lbrace <> x <> rbrace))
|
||||
|
||||
nextLine :: Doc ann -> Doc ann
|
||||
nextLine :: Doc a -> Doc a
|
||||
nextLine x = PP.group (line <> x)
|
||||
|
||||
ordinal :: Int -> Doc a
|
||||
@ -212,5 +220,5 @@ articleFor n
|
||||
| isVowel (Text.head n) = "an"
|
||||
| otherwise = "a"
|
||||
|
||||
itemize :: (Functor f, Foldable f) => f (Doc ann) -> Doc ann
|
||||
itemize :: (Functor f, Foldable f) => f (Doc a) -> Doc a
|
||||
itemize = vsep . fmap ("• " <>)
|
||||
|
@ -2,16 +2,17 @@ module Format where
|
||||
|
||||
import Base
|
||||
import Juvix.Compiler.Concrete qualified as Concrete
|
||||
import Juvix.Compiler.Concrete.Print qualified as P
|
||||
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
|
||||
import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
|
||||
import Juvix.Compiler.Pipeline.Setup
|
||||
import Juvix.Prelude.Pretty
|
||||
import Juvix.Formatter
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
_dir :: Path Abs Dir,
|
||||
_file :: Path Abs File
|
||||
_file :: Path Abs File,
|
||||
_expectedFile :: Maybe (Path Abs File),
|
||||
_force :: Bool
|
||||
}
|
||||
|
||||
makeLenses ''PosTest
|
||||
@ -19,13 +20,11 @@ makeLenses ''PosTest
|
||||
root :: Path Abs Dir
|
||||
root = relToProject $(mkRelDir "tests/positive")
|
||||
|
||||
renderCode :: (HasLoc a, P.PrettyPrint a) => P.Comments -> a -> Text
|
||||
renderCode c = toPlainText . P.ppOutDefault c
|
||||
|
||||
posTest :: String -> Path Rel Dir -> Path Rel File -> PosTest
|
||||
posTest _name rdir rfile =
|
||||
posTest :: String -> Path Rel Dir -> Path Rel File -> Maybe (Path Rel File) -> Bool -> PosTest
|
||||
posTest _name rdir rfile efile _force =
|
||||
let _dir = root <//> rdir
|
||||
_file = _dir <//> rfile
|
||||
_expectedFile = (_dir <//>) <$> efile
|
||||
in PosTest {..}
|
||||
|
||||
testDescr :: PosTest -> TestDescr
|
||||
@ -37,7 +36,9 @@ testDescr PosTest {..} =
|
||||
entryPoint <- defaultEntryPointCwdIO _file
|
||||
let maybeFile = entryPoint ^? entryPointModulePaths . _head
|
||||
f <- fromMaybeM (assertFailure "Not a module") (return maybeFile)
|
||||
|
||||
original :: Text <- readFile (toFilePath f)
|
||||
|
||||
step "Parsing"
|
||||
p :: Parser.ParserResult <- snd <$> runIO' entryPoint upToParsing
|
||||
|
||||
@ -51,11 +52,15 @@ testDescr PosTest {..} =
|
||||
Concrete.fromParsed p
|
||||
)
|
||||
|
||||
let formatted :: Text
|
||||
formatted = renderCode (s ^. Scoper.comments) (s ^. Scoper.mainModule)
|
||||
|
||||
step "Format"
|
||||
assertEqDiffText "check: pretty . scope . parse = id" original formatted
|
||||
let formatted = formatScoperResult' _force original s
|
||||
case _expectedFile of
|
||||
Nothing -> do
|
||||
step "Format"
|
||||
assertEqDiffText "check: pretty . scope . parse = id" original formatted
|
||||
Just eFile -> do
|
||||
step "Checking against expected output file"
|
||||
expFile :: Text <- readFile (toFilePath eFile)
|
||||
assertEqDiffText "Compare to expected output" formatted expFile
|
||||
}
|
||||
|
||||
allTests :: TestTree
|
||||
@ -69,9 +74,13 @@ tests =
|
||||
[ posTest
|
||||
"Format"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Format.juvix"),
|
||||
posTest
|
||||
"Records"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Format.juvix")
|
||||
Nothing
|
||||
False,
|
||||
posTest
|
||||
"TrailingWhitespace"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "LocalModWithAxiom.juvix")
|
||||
(Just $(mkRelFile "LocalModWithAxiom.juvix.formatted"))
|
||||
True
|
||||
]
|
||||
|
@ -2,5 +2,6 @@ module DefaultArgCycle;
|
||||
|
||||
import Stdlib.Data.Nat open;
|
||||
|
||||
fun {a : Nat := 1} {b : Nat := fun {c := 3} + a + 1} {c : Nat := b + a + 1}
|
||||
: Nat := a * b + c;
|
||||
fun {a : Nat := 1} {b : Nat := fun {c := 3}
|
||||
+ a
|
||||
+ 1} {c : Nat := b + a + 1} : Nat := a * b + c;
|
||||
|
@ -3,28 +3,30 @@ module AmbiguousCoercions;
|
||||
type Unit := unit;
|
||||
|
||||
trait
|
||||
type T A := mkT { pp : A → A };
|
||||
type T A := mkT {pp : A → A};
|
||||
|
||||
trait
|
||||
type T1 A := mkT1 { pp : A → A };
|
||||
type T1 A := mkT1 {pp : A → A};
|
||||
|
||||
trait
|
||||
type T2 A := mkT2 { pp : A → A };
|
||||
type T2 A := mkT2 {pp : A → A};
|
||||
|
||||
instance
|
||||
unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit});
|
||||
unitT1 : T1 Unit := mkT1 (pp := λ {_ := unit});
|
||||
|
||||
instance
|
||||
unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit});
|
||||
unitT2 : T2 Unit := mkT2 (pp := λ {_ := unit});
|
||||
|
||||
coercion instance
|
||||
fromT1toT {A} {{T1 A}} : T A := mkT@{
|
||||
pp := T1.pp
|
||||
};
|
||||
fromT1toT {A} {{T1 A}} : T A :=
|
||||
mkT@{
|
||||
pp := T1.pp
|
||||
};
|
||||
|
||||
coercion instance
|
||||
fromT2toT {A} {{T2 A}} : T A := mkT@{
|
||||
pp := T2.pp
|
||||
};
|
||||
fromT2toT {A} {{T2 A}} : T A :=
|
||||
mkT@{
|
||||
pp := T2.pp
|
||||
};
|
||||
|
||||
main : Unit := T.pp unit;
|
||||
|
@ -3,7 +3,9 @@ module CoercionTargetNotATrait;
|
||||
trait
|
||||
type T A := mkT {a : A};
|
||||
|
||||
type Maybe A := just A | nothing;
|
||||
type Maybe A :=
|
||||
| just A
|
||||
| nothing;
|
||||
|
||||
coercion instance
|
||||
inst {A} {{T A}} : Maybe A := nothing;
|
||||
|
@ -2,5 +2,6 @@ module DefaultArgCycleArity;
|
||||
|
||||
import Stdlib.Data.Nat open;
|
||||
|
||||
fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b + a + 1}
|
||||
: Nat := a * b + c;
|
||||
fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b
|
||||
+ a
|
||||
+ 1} : Nat := a * b + c;
|
||||
|
@ -1,6 +1,7 @@
|
||||
module DefaultTypeError;
|
||||
|
||||
type T := mkT;
|
||||
|
||||
type U := mkU;
|
||||
|
||||
g {a : T := mkU} : T := a;
|
||||
|
@ -9,13 +9,15 @@ trait
|
||||
type T2 A := mkT2 {pp : A -> A};
|
||||
|
||||
coercion instance
|
||||
fromT1toT2 {A} {{T1 A}} : T2 A := mkT2@{
|
||||
pp := T1.pp
|
||||
};
|
||||
fromT1toT2 {A} {{T1 A}} : T2 A :=
|
||||
mkT2@{
|
||||
pp := T1.pp
|
||||
};
|
||||
|
||||
coercion instance
|
||||
fromT2toT1 {A} {{T2 A}} : T1 A := mkT1@{
|
||||
pp := T2.pp
|
||||
};
|
||||
fromT2toT1 {A} {{T2 A}} : T1 A :=
|
||||
mkT1@{
|
||||
pp := T2.pp
|
||||
};
|
||||
|
||||
main : Unit := T1.pp unit;
|
||||
|
@ -23,11 +23,11 @@ import Data.Bool;
|
||||
open Data.Bool;
|
||||
|
||||
even : ℕ → Bool
|
||||
|
||||
|
||||
| zero := true
|
||||
| (suc n) := odd n;
|
||||
|
||||
odd : ℕ → Bool
|
||||
|
||||
|
||||
| zero := false
|
||||
| (suc n) := even n;
|
||||
|
@ -3,6 +3,7 @@ module DefaultArguments;
|
||||
type T := t;
|
||||
|
||||
g : T := f;
|
||||
|
||||
f {a : T := g} : T := a;
|
||||
|
||||
main : T := f;
|
||||
|
@ -3,7 +3,7 @@ module Mutual;
|
||||
axiom A : Type;
|
||||
|
||||
f : A -> A -> A
|
||||
|
||||
|
||||
| x y := g x (f x x);
|
||||
|
||||
g : A -> A -> A
|
||||
|
@ -9,11 +9,11 @@ type Ord :=
|
||||
| Lim : (ℕ -> Ord) -> Ord;
|
||||
|
||||
addord : Ord -> Ord -> Ord
|
||||
|
||||
|
||||
| Zord y := y
|
||||
| (SOrd x) y := SOrd (addord x y)
|
||||
| (Lim f) y := Lim (aux-addord f y);
|
||||
|
||||
aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
|
||||
|
||||
|
||||
| f y z := addord (f z) y;
|
||||
|
@ -4,7 +4,7 @@ axiom A : Type;
|
||||
|
||||
terminating
|
||||
f : A -> A -> A
|
||||
|
||||
|
||||
| x y := g x (f x x);
|
||||
|
||||
g : A -> A -> A
|
||||
|
@ -3,7 +3,7 @@ module TerminatingG;
|
||||
axiom A : Type;
|
||||
|
||||
f : A -> A -> A
|
||||
|
||||
|
||||
| x y := g x (f x x);
|
||||
|
||||
terminating
|
||||
|
@ -18,13 +18,13 @@ axiom c : C;
|
||||
|
||||
axiom d : D;
|
||||
|
||||
mk {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) : A × f2 × C :=
|
||||
f1, x, f3;
|
||||
mk {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2)
|
||||
: A × f2 × C := f1, x, f3;
|
||||
|
||||
x1 : A × B × C := mk (x := b);
|
||||
|
||||
mk2 {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) {f4 : D := d} (y : f2) : A × f2 × C :=
|
||||
f1, x, f3;
|
||||
mk2 {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) {f4 : D := d} (y : f2)
|
||||
: A × f2 × C := f1, x, f3;
|
||||
|
||||
x2 : A × B × C := mk2 (x := b) (y := b);
|
||||
|
||||
|
@ -188,12 +188,14 @@ f : Nat -> Nat :=
|
||||
};
|
||||
|
||||
module Patterns;
|
||||
|
||||
syntax operator × functor;
|
||||
syntax operator , pair;
|
||||
type × (A : Type) (B : Type) := , : A → B → A × B;
|
||||
|
||||
f : Nat × Nat × Nat × Nat -> Nat
|
||||
| (a, b, c, d) := a;
|
||||
|
||||
end;
|
||||
|
||||
module UnicodeStrings;
|
||||
@ -201,6 +203,7 @@ module UnicodeStrings;
|
||||
end;
|
||||
|
||||
module Comments;
|
||||
|
||||
axiom a1 : Type;
|
||||
-- attached to a1
|
||||
|
||||
|
@ -13,11 +13,11 @@ not : _
|
||||
| true := false;
|
||||
|
||||
odd : _
|
||||
|
||||
|
||||
| zero := false
|
||||
| (suc n) := even n;
|
||||
|
||||
even : _
|
||||
|
||||
|
||||
| zero := true
|
||||
| (suc n) := odd n;
|
||||
|
29
tests/positive/LocalModWithAxiom.juvix
Normal file
29
tests/positive/LocalModWithAxiom.juvix
Normal file
@ -0,0 +1,29 @@
|
||||
{-# format: false #-}
|
||||
module LocalModWithAxiom;
|
||||
|
||||
module A;
|
||||
|
||||
axiom B : Type;
|
||||
|
||||
end;
|
||||
|
||||
module C;
|
||||
|
||||
|
||||
|
||||
axiom D : Type;
|
||||
|
||||
module E;
|
||||
|
||||
|
||||
|
||||
axiom F : Type;
|
||||
|
||||
end;
|
||||
|
||||
end;
|
||||
|
||||
|
||||
|
||||
|
||||
|
21
tests/positive/LocalModWithAxiom.juvix.formatted
Normal file
21
tests/positive/LocalModWithAxiom.juvix.formatted
Normal file
@ -0,0 +1,21 @@
|
||||
{-# format: false #-}
|
||||
module LocalModWithAxiom;
|
||||
|
||||
module A;
|
||||
|
||||
axiom B : Type;
|
||||
|
||||
end;
|
||||
|
||||
module C;
|
||||
|
||||
axiom D : Type;
|
||||
|
||||
module E;
|
||||
|
||||
axiom F : Type;
|
||||
|
||||
end;
|
||||
|
||||
end;
|
||||
|
@ -11,7 +11,7 @@ type List (a : Type) :=
|
||||
:: : a → List a → List a;
|
||||
|
||||
Forest : Type -> Type
|
||||
|
||||
|
||||
| A := List (Tree A);
|
||||
|
||||
--- N-Ary tree.
|
||||
|
@ -4,4 +4,5 @@ import Stdlib.Prelude open;
|
||||
import PackageDescription.V1 open;
|
||||
|
||||
package : Package :=
|
||||
defaultPackage {name := "package-juvix"; dependencies := []};
|
||||
defaultPackage
|
||||
{name := "package-juvix"; dependencies := []};
|
||||
|
@ -5,6 +5,6 @@ import PackageDescription.V1 open;
|
||||
|
||||
package : Package :=
|
||||
defaultPackage
|
||||
{name := "abc";
|
||||
version := mkVersion 0 0 0 ;
|
||||
dependencies := [git "name" "url" "ref1"]};
|
||||
{name := "abc";
|
||||
version := mkVersion 0 0 0;
|
||||
dependencies := [git "name" "url" "ref1"]};
|
||||
|
@ -23,11 +23,11 @@ import Data.Bool;
|
||||
open Data.Bool;
|
||||
|
||||
even : ℕ → Bool
|
||||
|
||||
|
||||
| zero := true
|
||||
| (suc n) := odd n;
|
||||
|
||||
odd : ℕ → Bool
|
||||
|
||||
|
||||
| zero := false
|
||||
| (suc n) := even n;
|
||||
|
@ -4,7 +4,7 @@ axiom A : Type;
|
||||
|
||||
terminating
|
||||
f : A -> A -> A
|
||||
|
||||
|
||||
| x y := g x (f x x);
|
||||
|
||||
terminating
|
||||
|
@ -328,3 +328,4 @@ tests:
|
||||
stdout:
|
||||
contains: juvix format error
|
||||
exit-status: 1
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user