idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-23 22:22:07 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] --install-with-src; refactoring around FCs (#1450)

Browse Source 
Why:

* To implement robust cross-project go-to-definition in LSP
  i.e you can jump to definition of any global name coming
  from library dependencies, as well as from the local project files.

What it does:

*  Modify `FC`s to carry `ModuleIdent` for .idr sources,
   file name for .ipkg sources or nothing for interactive runs.

*  Add `--install-with-src` to install the source code alongside
   the ttc binaries. The source is installed into the same directory
   as the corresponding ttc file. Installed sources are made read-only.

*  As we install the sources pinned to the related ttc files we gain
   the versioning of sources for free.
This commit is contained in:
Ruslan Feizerakhmanov 2021-06-05 14:53:22 +03:00 committed by GitHub
parent baa6051d69
commit 7aee7c9b7c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
143 changed files with 918 additions and 619 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Makefile
View File

@ -149,6 +149,9 @@ install: install-idris2 install-support install-libs
install-api: src/IdrisPaths.idr
${IDRIS2_BOOT} --install ${IDRIS2_LIB_IPKG}
install-with-src-api: src/IdrisPaths.idr
${IDRIS2_BOOT} --install-with-src ${IDRIS2_LIB_IPKG}
install-idris2:
mkdir -p ${PREFIX}/bin/
install ${TARGET} ${PREFIX}/bin
@ -180,6 +183,12 @@ install-libs:
${MAKE} -C libs/network install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
install-with-src-libs:
${MAKE} -C libs/prelude install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/test install-with-src IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
.PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean

59
libs/base/Language/Reflection/TT.idr
View File

@ -4,6 +4,22 @@ import public Data.List
%default total
public export
data Namespace = MkNS (List String) -- namespace, stored in reverse order
public export
data ModuleIdent = MkMI (List String) -- module identifier, stored in reverse order
export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
export
Show Namespace where
show (MkNS ns) = showSep "." (reverse ns)
-- 'FilePos' represents the position of
-- the source information in the file (or REPL).
-- in the form of '(line-no, column-no)'.
@ -11,13 +27,31 @@ public export
FilePos : Type
FilePos = (Int, Int)
-- 'FC' represents the source location of the term.
-- The first 'FilePos' indicates the starting position.
-- the second 'FilePos' indicates the start of the next term.
public export
data FC : Type where
MkFC : String -> FilePos -> FilePos -> FC
EmptyFC : FC
data VirtualIdent : Type where
Interactive : VirtualIdent
public export
data OriginDesc : Type where
||| Anything that originates in physical Idris source files is assigned a
||| `PhysicalIdrSrc modIdent`,
||| where `modIdent` is the top-level module identifier of that file.
PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
||| where `fname` is path to the package file.
PhysicalPkgSrc : (fname : String) -> OriginDesc
Virtual : (ident : VirtualIdent) -> OriginDesc
||| A file context is a filename together with starting and ending positions.
||| It's often carried by AST nodes that might have been created from a source
||| file or by the compiler. That makes it useful to have the notion of
||| `EmptyFC` as part of the type.
public export
data FC = MkFC OriginDesc FilePos FilePos
| ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
||| errors, but we shouldn't attach semantic highlighting metadata to them.
MkVirtualFC OriginDesc FilePos FilePos
| EmptyFC
public export
emptyFC : FC
@ -54,19 +88,6 @@ data Constant
| DoubleType
| WorldType
public export
data Namespace = MkNS (List String) -- namespace, stored in reverse order
export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
export
Show Namespace where
show (MkNS ns) = showSep "." (reverse ns)
public export
data Name = UN String -- user defined name
| MN String Int -- machine generated name

3
libs/base/Makefile
View File

@ -4,6 +4,9 @@ all:
install:
${IDRIS2} --install base.ipkg
install-with-src:
${IDRIS2} --install-with-src base.ipkg
docs:
${IDRIS2} --mkdoc base.ipkg

3
libs/contrib/Makefile
View File

@ -4,6 +4,9 @@ all:
install:
${IDRIS2} --install contrib.ipkg
install-with-src:
${IDRIS2} --install-with-src contrib.ipkg
docs:
${IDRIS2} --mkdoc contrib.ipkg

3
libs/network/Makefile
View File

@ -4,6 +4,9 @@ all:
install:
${IDRIS2} --install network.ipkg
install-with-src:
${IDRIS2} --install-with-src network.ipkg
docs:
${IDRIS2} --mkdoc network.ipkg

3
libs/prelude/Makefile
View File

@ -4,6 +4,9 @@ all:
install:
${IDRIS2} --install prelude.ipkg
install-with-src:
${IDRIS2} --install-with-src prelude.ipkg
docs:
${IDRIS2} --mkdoc prelude.ipkg

3
libs/test/Makefile
View File

@ -4,6 +4,9 @@ all:
install:
${IDRIS2} --install test.ipkg
install-with-src:
${IDRIS2} --install-with-src test.ipkg
docs:
${IDRIS2} --mkdoc test.ipkg

72
src/Core/Directory.idr
View File

@ -18,7 +18,33 @@ import System.Info
%default total
public export
data IdrSrcExt = E_idr | E_lidr | E_yaff | E_org | E_md
public export
Eq IdrSrcExt where
E_idr == E_idr = True
E_lidr == E_lidr = True
E_yaff == E_yaff = True
E_org == E_org = True
E_md == E_md = True
_ == _ = False
public export
Show IdrSrcExt where
show E_idr = "idr"
show E_lidr = "lidr"
show E_yaff = "yaff"
show E_org = "org"
show E_md = "md"
public export
listOfExtensions : List IdrSrcExt
listOfExtensions = [E_idr, E_lidr, E_yaff, E_org, E_md]
-- Return the name of the first file available in the list
-- Used in LSP.
export
firstAvailable : {auto c : Ref Ctxt Defs} ->
List String -> Core (Maybe String)
firstAvailable [] = pure Nothing
@ -73,7 +99,7 @@ nsToPath : {auto c : Ref Ctxt Defs} ->
FC -> ModuleIdent -> Core (Either Error String)
nsToPath loc ns
= do d <- getDirs
let fnameBase = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
let fnameBase = ModuleIdent.toPath ns
let fs = map (\p => p </> fnameBase <.> "ttc")
((build_dir d </> "ttc") :: extra_dirs d)
Just f <- firstAvailable fs
@ -87,10 +113,9 @@ nsToSource : {auto c : Ref Ctxt Defs} ->
FC -> ModuleIdent -> Core String
nsToSource loc ns
= do d <- getDirs
let fnameOrig = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
let fnameOrig = ModuleIdent.toPath ns
let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
let fs = map (\ext => fnameBase <.> ext)
[".idr", ".lidr", ".yaff", ".org", ".md"]
let fs = map ((fnameBase <.>) . show) listOfExtensions
Just f <- firstAvailable fs
| Nothing => throw (ModuleNotFound loc ns)
pure f
@ -98,20 +123,32 @@ nsToSource loc ns
-- Given a filename in the working directory + source directory, return the correct
-- namespace for it
export
pathToNS : String -> Maybe String -> String -> Core ModuleIdent
pathToNS wdir sdir fname =
mbPathToNS : String -> Maybe String -> String -> Maybe ModuleIdent
mbPathToNS wdir sdir fname =
let
sdir = fromMaybe "" sdir
base = if isAbsolute fname then wdir </> sdir else sdir
in
case Path.dropBase base fname of
Nothing => throw (UserError (
unsafeFoldModuleIdent . reverse . splitPath . Path.dropExtension
<$> Path.dropBase base fname
export
corePathToNS : String -> Maybe String -> String -> Core ModuleIdent
corePathToNS wdir sdir fname = do
let err = UserError $
"Source file "
++ show fname
++ " is not in the source directory "
++ show (wdir </> sdir)))
Just relPath =>
pure $ unsafeFoldModuleIdent $ reverse $ splitPath $ Path.dropExtension relPath
++ show fname
++ " is not in the source directory "
++ show (wdir </> fromMaybe "" sdir)
maybe (throw err) pure (mbPathToNS wdir sdir fname)
export
ctxtPathToNS : {auto c : Ref Ctxt Defs} -> String -> Core ModuleIdent
ctxtPathToNS fname = do
defs <- get Ctxt
let wdir = defs.options.dirs.working_dir
let sdir = defs.options.dirs.source_dir
corePathToNS wdir sdir fname
dirExists : String -> IO Bool
dirExists dir = do Right d <- openDir dir
@ -162,12 +199,11 @@ export
getTTCFileName : {auto c : Ref Ctxt Defs} ->
String -> String -> Core String
getTTCFileName inp ext
= do ns <- getNS
d <- getDirs
-- Get its namespace from the file relative to the working directory
= do -- Get its namespace from the file relative to the working directory
-- and generate the ttc file from that
ns <- pathToNS (working_dir d) (source_dir d) inp
let fname = joinPath (reverse $ unsafeUnfoldModuleIdent ns) <.> ext
ns <- ctxtPathToNS inp
let fname = ModuleIdent.toPath ns <.> ext
d <- getDirs
let bdir = build_dir d
pure $ bdir </> "ttc" </> fname

75
src/Core/FC.idr
View File

@ -1,5 +1,7 @@
module Core.FC
import Core.Name.Namespace
import Data.Maybe
import Libraries.Text.Bounded
import Libraries.Text.PrettyPrint.Prettyprinter
@ -20,21 +22,61 @@ public export
FileName : Type
FileName = String
public export
data VirtualIdent : Type where
Interactive : VirtualIdent
public export
Eq VirtualIdent where
Interactive == Interactive = True
export
Show VirtualIdent where
show Interactive = "(Interactive)"
public export
data OriginDesc : Type where
||| Anything that originates in physical Idris source files is assigned a
||| `PhysicalIdrSrc modIdent`,
||| where `modIdent` is the top-level module identifier of that file.
PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
||| where `fname` is path to the package file.
PhysicalPkgSrc : (fname : FileName) -> OriginDesc
Virtual : (ident : VirtualIdent) -> OriginDesc
public export
Eq OriginDesc where
PhysicalIdrSrc ident == PhysicalIdrSrc ident' = ident == ident'
PhysicalPkgSrc fname == PhysicalPkgSrc fname' = fname == fname'
Virtual ident == Virtual ident' = ident == ident'
_ == _ = False
export
Show OriginDesc where
show (PhysicalIdrSrc ident) = show ident
show (PhysicalPkgSrc fname) = show fname
show (Virtual ident) = show ident
export
Pretty OriginDesc where
pretty = pretty . show
||| A file context is a filename together with starting and ending positions.
||| It's often carried by AST nodes that might have been created from a source
||| file or by the compiler. That makes it useful to have the notion of
||| `EmptyFC` as part of the type.
public export
data FC = MkFC FileName FilePos FilePos
data FC = MkFC OriginDesc FilePos FilePos
| ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
||| errors, but we shouldn't attach semantic highlighting metadata to them.
MkVirtualFC FileName FilePos FilePos
MkVirtualFC OriginDesc FilePos FilePos
| EmptyFC
||| A version of a file context that cannot be empty
public export
NonEmptyFC : Type
NonEmptyFC = (FileName, FilePos, FilePos)
NonEmptyFC = (OriginDesc, FilePos, FilePos)
------------------------------------------------------------------------
-- Conversion between NonEmptyFC and FC
@ -63,10 +105,13 @@ virtualiseFC : FC -> FC
virtualiseFC (MkFC fn start end) = MkVirtualFC fn start end
virtualiseFC fc = fc
export
defaultFC : NonEmptyFC
defaultFC = ("", (0, 0), (0, 0))
defaultFC = (Virtual Interactive, (0, 0), (0, 0))
export
replFC : FC
replFC = justFC defaultFC
export
toNonEmptyFC : FC -> NonEmptyFC
@ -76,8 +121,8 @@ toNonEmptyFC = fromMaybe defaultFC . isNonEmptyFC
-- Projections
export
file : NonEmptyFC -> FileName
file (fn, _, _) = fn
origin : NonEmptyFC -> OriginDesc
origin (fn, _, _) = fn
export
startPos : NonEmptyFC -> FilePos
@ -107,8 +152,8 @@ endCol = snd . endPos
-- Smart constructors
export
boundToFC : FileName -> WithBounds t -> FC
boundToFC fname b = MkFC fname (start b) (end b)
boundToFC : OriginDesc -> WithBounds t -> FC
boundToFC mbModIdent b = MkFC mbModIdent (start b) (end b)
------------------------------------------------------------------------
-- Predicates
@ -134,10 +179,6 @@ export
emptyFC : FC
emptyFC = EmptyFC
export
toplevelFC : FC
toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
------------------------------------------------------------------------
-- Basic operations
export
@ -164,10 +205,10 @@ Eq FC where
export
Show FC where
show EmptyFC = "EmptyFC"
show (MkFC file startPos endPos) = file ++ ":" ++
show (MkFC ident startPos endPos) = show ident ++ ":" ++
showPos startPos ++ "--" ++
showPos endPos
show (MkVirtualFC file startPos endPos) = file ++ ":" ++
show (MkVirtualFC ident startPos endPos) = show ident ++ ":" ++
showPos startPos ++ "--" ++
showPos endPos
@ -177,9 +218,9 @@ prettyPos (l, c) = pretty (l + 1) <+> colon <+> pretty (c + 1)
export
Pretty FC where
pretty EmptyFC = pretty "EmptyFC"
pretty (MkFC file startPos endPos) = pretty file <+> colon
pretty (MkFC ident startPos endPos) = pretty ident <+> colon
<+> prettyPos startPos <+> pretty "--"
<+> prettyPos endPos
pretty (MkVirtualFC file startPos endPos) = pretty file <+> colon
pretty (MkVirtualFC ident startPos endPos) = pretty ident <+> colon
<+> prettyPos startPos <+> pretty "--"
<+> prettyPos endPos

27
src/Core/Metadata.idr
View File

@ -4,9 +4,11 @@ import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Env
import Core.FC
import Core.Normalise
import Core.Options
import Core.TT
import Core.TTC
@ -96,7 +98,7 @@ record Metadata where
currentLHS : Maybe ClosedTerm
holeLHS : List (Name, ClosedTerm)
nameLocMap : PosMap (NonEmptyFC, Name)
sourcefile : String
sourceIdent : OriginDesc
-- Semantic Highlighting
-- Posmap of known semantic decorations
@ -116,21 +118,21 @@ Show Metadata where
" current LHS: " ++ show currentLHS ++ "\n" ++
" holes: " ++ show holeLHS ++ "\n" ++
" nameLocMap: " ++ show nameLocMap ++ "\n" ++
" sourcefile: " ++ fname ++
" sourceIdent: " ++ show fname ++
" semanticHighlighting: " ++ show semanticHighlighting ++
" semanticAliases: " ++ show semanticAliases ++
" semanticDefaults: " ++ show semanticDefaults
export
initMetadata : String -> Metadata
initMetadata fname = MkMetadata
initMetadata : OriginDesc -> Metadata
initMetadata finfo = MkMetadata
{ lhsApps = []
, names = []
, tydecls = []
, currentLHS = Nothing
, holeLHS = []
, nameLocMap = empty
, sourcefile = fname
, sourceIdent = finfo
, semanticHighlighting = empty
, semanticAliases = empty
, semanticDefaults = empty
@ -147,7 +149,7 @@ TTC Metadata where
toBuf b (tydecls m)
toBuf b (holeLHS m)
toBuf b (nameLocMap m)
toBuf b (sourcefile m)
toBuf b (sourceIdent m)
toBuf b (semanticHighlighting m)
toBuf b (semanticAliases m)
toBuf b (semanticDefaults m)
@ -312,14 +314,17 @@ addSemanticDecorations : {auto m : Ref MD Metadata} ->
SemanticDecorations -> Core ()
addSemanticDecorations decors
= do meta <- get MD
defs <- get Ctxt
let posmap = meta.semanticHighlighting
let (newDecors,droppedDecors) = span
((meta.sourcefile ==)
. (\((fn, _), _) => fn))
decors
let (newDecors,droppedDecors) =
span
( (meta.sourceIdent ==)
. Builtin.fst
. Builtin.fst )
decors
unless (isNil droppedDecors)
$ log "ide-mode.highlight" 19 $ "ignored adding decorations to "
++ meta.sourcefile ++ ": " ++ show droppedDecors
++ show meta.sourceIdent ++ ": " ++ show droppedDecors
put MD $ record {semanticHighlighting
= (fromList newDecors) `union` posmap} meta

7
src/Core/Name/Namespace.idr
View File

@ -6,6 +6,7 @@ import Data.Strings
import Decidable.Equality
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.Path
%default total
@ -114,6 +115,12 @@ export
unsafeFoldModuleIdent : List String -> ModuleIdent
unsafeFoldModuleIdent = MkMI
namespace ModuleIdent
||| A.B.C -> "A/B/C"
export
toPath : ModuleIdent -> String
toPath = joinPath . reverse . unsafeUnfoldModuleIdent
-------------------------------------------------------------------------------------
-- HIERARCHICAL STRUCTURE
-------------------------------------------------------------------------------------

58
src/Core/Reflect.idr
View File

@ -253,6 +253,22 @@ Reflect Namespace where
= do ns' <- reflect fc defs lhs env (unsafeUnfoldNamespace ns)
appCon fc defs (reflectiontt "MkNS") [ns']
export
Reify ModuleIdent where
reify defs val@(NDCon _ n _ _ [(_, ns)])
= case (!(full (gamma defs) n)) of
NS _ (UN "MkMI")
=> do ns' <- reify defs !(evalClosure defs ns)
pure (unsafeFoldModuleIdent ns')
_ => cantReify val "ModuleIdent"
reify defs val = cantReify val "ModuleIdent"
export
Reflect ModuleIdent where
reflect fc defs lhs env ns
= do ns' <- reflect fc defs lhs env (unsafeUnfoldModuleIdent ns)
appCon fc defs (reflectiontt "MkMI") [ns']
export
Reify Name where
reify defs val@(NDCon _ n _ _ args)
@ -573,6 +589,48 @@ Reflect LazyReason where
reflect fc defs lhs env LLazy = getCon fc defs (reflectiontt "LLazy")
reflect fc defs lhs env LUnknown = getCon fc defs (reflectiontt "LUnknown")
export
Reify VirtualIdent where
reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of
(NS _ (UN "Interactive"), [])
=> pure Interactive
_ => cantReify val "VirtualIdent"
reify defs val = cantReify val "VirtualIdent"
export
Reflect VirtualIdent where
reflect fc defs lhs env Interactive
= getCon fc defs (reflectiontt "Interactive")
export
Reify OriginDesc where
reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of
(NS _ (UN "PhysicalIdrSrc"), [(_, ident)])
=> do ident' <- reify defs !(evalClosure defs ident)
pure (PhysicalIdrSrc ident')
(NS _ (UN "PhysicalPkgSrc"), [(_, fname)])
=> do fname' <- reify defs !(evalClosure defs fname)
pure (PhysicalPkgSrc fname')
(NS _ (UN "Virtual"), [(_, ident)])
=> do ident' <- reify defs !(evalClosure defs ident)
pure (Virtual ident')
_ => cantReify val "OriginDesc"
reify defs val = cantReify val "OriginDesc"
export
Reflect OriginDesc where
reflect fc defs lhs env (PhysicalIdrSrc ident)
= do ident' <- reflect fc defs lhs env ident
appCon fc defs (reflectiontt "PhysicalIdrSrc") [ident']
reflect fc defs lhs env (PhysicalPkgSrc fname)
= do fname' <- reflect fc defs lhs env fname
appCon fc defs (reflectiontt "PhysicalPkgSrc") [fname']
reflect fc defs lhs env (Virtual ident)
= do ident' <- reflect fc defs lhs env ident
appCon fc defs (reflectiontt "Virtual") [ident']
export
Reify FC where
reify defs val@(NDCon _ n _ _ args)

41
src/Core/TTC.idr
View File

@ -18,6 +18,38 @@ import Libraries.Utils.Binary
%default covering
export
TTC Namespace where
toBuf b = toBuf b . unsafeUnfoldNamespace
fromBuf = Core.map unsafeFoldNamespace . fromBuf
export
TTC ModuleIdent where
toBuf b = toBuf b . unsafeUnfoldModuleIdent
fromBuf = Core.map unsafeFoldModuleIdent . fromBuf
export
TTC VirtualIdent where
toBuf b Interactive = tag 0
fromBuf b =
case !getTag of
0 => pure Interactive
_ => corrupt "VirtualIdent"
export
TTC OriginDesc where
toBuf b (PhysicalIdrSrc ident) = do tag 0; toBuf b ident
toBuf b (PhysicalPkgSrc fname) = do tag 1; toBuf b fname
toBuf b (Virtual ident) = do tag 2; toBuf b ident
fromBuf b =
case !getTag of
0 => [| PhysicalIdrSrc (fromBuf b) |]
1 => [| PhysicalPkgSrc (fromBuf b) |]
2 => [| Virtual (fromBuf b) |]
_ => corrupt "OriginDesc"
export
TTC FC where
toBuf b (MkFC file startPos endPos)
@ -36,15 +68,6 @@ TTC FC where
s <- fromBuf b; e <- fromBuf b
pure (MkVirtualFC f s e)
_ => corrupt "FC"
export
TTC Namespace where
toBuf b = toBuf b . unsafeUnfoldNamespace
fromBuf = Core.map unsafeFoldNamespace . fromBuf
export
TTC ModuleIdent where
toBuf b = toBuf b . unsafeUnfoldModuleIdent
fromBuf = Core.map unsafeFoldModuleIdent . fromBuf
export
TTC Name where

5
src/Idris/CommandLine.idr
View File

@ -22,6 +22,7 @@ public export
data PkgCommand
= Build
| Install
| InstallWithSrc
| MkDoc
| Typecheck
| Clean
@ -32,6 +33,7 @@ export
Show PkgCommand where
show Build = "--build"
show Install = "--install"
show InstallWithSrc = "--install-with-src"
show MkDoc = "--mkdoc"
show Typecheck = "--typecheck"
show Clean = "--clean"
@ -240,6 +242,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Build modules/executable for the given package"),
MkOpt ["--install"] [Required "package file"] (\f => [Package Install f])
(Just "Install the given package"),
MkOpt ["--install-with-src"] [Required "package file"]
(\f => [Package InstallWithSrc f])
(Just "Install the given package"),
MkOpt ["--mkdoc"] [Required "package file"] (\f => [Package MkDoc f])
(Just "Build documentation for the given package"),
MkOpt ["--typecheck"] [Required "package file"] (\f => [Package Typecheck f])

8
src/Idris/Driver.idr
View File

@ -4,6 +4,7 @@ import Compiler.Common
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.Unify
@ -178,7 +179,12 @@ stMain cgs opts
when (checkVerbose opts) $ -- override Quiet if implicitly set
setOutput (REPL False)
u <- newRef UST initUState
m <- newRef MD (initMetadata $ fromMaybe "(interactive)" fname)
origin <- maybe
(pure $ Virtual Interactive) (\fname => do
modIdent <- ctxtPathToNS fname
pure (PhysicalIdrSrc modIdent)
) fname
m <- newRef MD (initMetadata origin)
updateREPLOpts
session <- getSession
when (not $ nobanner session) $ do

10
src/Idris/IDEMode/Parser.idr
View File

@ -78,10 +78,10 @@ sexp
pure (SExpList xs)
ideParser : {e : _} ->
(fname : String) -> String -> Grammar SemanticDecorations Token e ty -> Either Error ty
ideParser fname str p
= do toks <- mapFst (fromLexError fname) $ idelex str
(decor, (parsed, _)) <- mapFst (fromParsingError fname) $ parseWith p toks
String -> Grammar SemanticDecorations Token e ty -> Either Error ty
ideParser str p
= do toks <- mapFst (fromLexError (Virtual Interactive)) $ idelex str
(decor, (parsed, _)) <- mapFst (fromParsingError (Virtual Interactive)) $ parseWith p toks
Right parsed
@ -89,4 +89,4 @@ export
covering
parseSExp : String -> Either Error SExp
parseSExp inp
= ideParser "(interactive)" inp (do c <- sexp; eoi; pure c)
= ideParser inp (do c <- sexp; eoi; pure c)

12
src/Idris/IDEMode/REPL.idr
View File

@ -397,10 +397,18 @@ displayIDEResult outf i (REPL $ ConsoleWidthSet mn)
displayIDEResult outf i (NameLocList dat)
= printIDEResult outf i $ SExpList !(traverse (constructSExp . map toNonEmptyFC) dat)
where
-- Can't recover the full path to the file, because
-- the name may come from an out-of-project location whereas we only store
-- module identifiers (source location is lost).
sexpOriginDesc : OriginDesc -> String
sexpOriginDesc (PhysicalIdrSrc mod) = show mod
sexpOriginDesc (PhysicalPkgSrc fname) = fname
sexpOriginDesc (Virtual Interactive) = "(Interactive)"
constructSExp : (Name, NonEmptyFC) -> Core SExp
constructSExp (name, fname, (startLine, startCol), (endLine, endCol)) = pure $
constructSExp (name, origin, (startLine, startCol), (endLine, endCol)) = pure $
SExpList [ StringAtom !(render $ pretty name)
, StringAtom fname
, StringAtom (sexpOriginDesc origin)
, IntegerAtom $ cast $ startLine
, IntegerAtom $ cast $ startCol
, IntegerAtom $ cast $ endLine

35
src/Idris/IDEMode/SyntaxHighlight.idr
View File

@ -2,6 +2,7 @@ module Idris.IDEMode.SyntaxHighlight
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.TT
@ -28,6 +29,7 @@ SExpable Decoration where
record Highlight where
constructor MkHighlight
location : NonEmptyFC
filename : String
name : String
isImplicit : Bool
key : String
@ -36,9 +38,9 @@ record Highlight where
typ : String
ns : String
SExpable FC where
toSExp fc = case isNonEmptyFC fc of
Just (fname , (startLine, startCol), (endLine, endCol)) =>
SExpable (FileName, FC) where
toSExp (fname, fc) = case isNonEmptyFC fc of
Just (origin, (startLine, startCol), (endLine, endCol)) =>
SExpList [ SExpList [ SymbolAtom "filename", StringAtom fname ]
, SExpList [ SymbolAtom "start"
, IntegerAtom (cast startLine + 1)
@ -52,8 +54,8 @@ SExpable FC where
Nothing => SExpList []
SExpable Highlight where
toSExp (MkHighlight loc nam impl k dec doc t ns)
= SExpList [ toSExp $ justFC loc
toSExp (MkHighlight loc fname nam impl k dec doc t ns)
= SExpList [ toSExp $ (fname, justFC loc)
, SExpList [ SExpList [ SymbolAtom "name", StringAtom nam ]
, SExpList [ SymbolAtom "namespace", StringAtom ns ]
, toSExp dec
@ -64,9 +66,6 @@ SExpable Highlight where
]
]
inFile : (s : String) -> (NonEmptyFC, a) -> Bool
inFile fname ((file, _, _), _) = file == fname
||| Output some data using current dialog index
export
printOutput : {auto c : Ref Ctxt Defs} ->
@ -97,12 +96,12 @@ outputHighlight h =
lwOutputHighlight :
{auto c : Ref Ctxt Defs} ->
{auto opts : Ref ROpts REPLOpts} ->
(NonEmptyFC, Decoration) -> Core ()
lwOutputHighlight (nfc,decor) =
(FileName, NonEmptyFC, Decoration) -> Core ()
lwOutputHighlight (fname, nfc, decor) =
printOutput $ SExpList [ SymbolAtom "ok"
, SExpList [ SymbolAtom "highlight-source"
, toSExp $ the (List _) [
SExpList [ toSExp $ justFC nfc
SExpList [ toSExp $ (fname, justFC nfc)
, SExpList [ toSExp decor]
]]]]
@ -111,8 +110,8 @@ lwOutputHighlight (nfc,decor) =
outputNameSyntax : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto opts : Ref ROpts REPLOpts} ->
(NonEmptyFC, Decoration, Name) -> Core ()
outputNameSyntax (nfc, decor, nm) = do
(FileName, NonEmptyFC, Decoration, Name) -> Core ()
outputNameSyntax (fname, nfc, decor, nm) = do
defs <- get Ctxt
log "ide-mode.highlight" 20 $ "highlighting at " ++ show nfc
++ ": " ++ show nm
@ -122,6 +121,7 @@ outputNameSyntax (nfc, decor, nm) = do
outputHighlight $ MkHighlight
{ location = nfc
, name
, filename = fname
, isImplicit = False
, key = ""
, decor
@ -142,7 +142,10 @@ outputSyntaxHighlighting fname loadResult = do
opts <- get ROpts
when (opts.synHighlightOn) $ do
meta <- get MD
let allNames = filter (inFile fname) $ toList meta.nameLocMap
modIdent <- ctxtPathToNS fname
let allNames = filter ((PhysicalIdrSrc modIdent ==) . fst . fst)
$ toList meta.nameLocMap
--decls <- filter (inFile fname) . tydecls <$> get MD
--_ <- traverse outputNameSyntax allNames -- ++ decls)
@ -168,8 +171,8 @@ outputSyntaxHighlighting fname loadResult = do
traverse_ {b = Unit}
(\(nfc, decor, mn) =>
case mn of
Nothing => lwOutputHighlight (nfc, decor)
Just n => outputNameSyntax (nfc, decor, n))
Nothing => lwOutputHighlight (fname, nfc, decor)
Just n => outputNameSyntax (fname, nfc, decor, n))
(defaults ++ aliases ++ toList semHigh)
pure loadResult

23
src/Idris/ModTree.idr
View File

@ -79,7 +79,7 @@ mkModTree loc done modFP mod
case lookup mod all of
Nothing =>
do file <- maybe (nsToSource loc mod) pure modFP
modInfo <- readHeader file
modInfo <- readHeader file mod
let imps = map path (imports modInfo)
ms <- traverse (mkModTree loc (mod :: done) Nothing) imps
let mt = MkModTree mod (Just file) ms
@ -123,6 +123,7 @@ mkBuildMods mod
-- Given a main file name, return the list of modules that need to be
-- built for that main file, in the order they need to be built
-- Return an empty list if it turns out it's in the 'done' list
export
getBuildMods : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
FC -> (done : List BuildMod) ->
@ -130,8 +131,7 @@ getBuildMods : {auto c : Ref Ctxt Defs} ->
Core (List BuildMod)
getBuildMods loc done fname
= do a <- newRef AllMods []
d <- getDirs
fname_ns <- pathToNS (working_dir d) (source_dir d) fname
fname_ns <- ctxtPathToNS fname
if fname_ns `elem` map buildNS done
then pure []
else
@ -163,6 +163,7 @@ buildMod loc num len mod
= do clearCtxt; addPrimitives
lazyActive True; setUnboundImplicits True
let src = buildFile mod
let ident = buildNS mod
mttc <- getTTCFileName src "ttc"
-- We'd expect any errors in nsToPath to have been caught by now
-- since the imports have been built! But we still have to check.
@ -178,7 +179,7 @@ buildMod loc num len mod
Left _ => True
Right t => any (\x => x > t) (srcTime :: map snd depTimes)
u <- newRef UST initUState
m <- newRef MD (initMetadata src)
m <- newRef MD (initMetadata (PhysicalIdrSrc ident))
put Syn initSyntax
errs <- if (not needsBuilding) then pure [] else
@ -188,7 +189,7 @@ buildMod loc num len mod
<+> slash <+> pretty len <+> colon
<++> pretty "Building" <++> pretty mod.buildNS
<++> parens (pretty src)
process {u} {m} msg src
process {u} {m} msg src ident
defs <- get Ctxt
ws <- emitWarningsAndErrors (if null errs then ferrs else errs)
@ -199,6 +200,7 @@ buildMod loc num len mod
(ModuleNotFound _ _) => True
_ => False
export
buildMods : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
@ -219,12 +221,13 @@ buildDeps : {auto c : Ref Ctxt Defs} ->
(mainFile : String) ->
Core (List Error)
buildDeps fname
= do mods <- getBuildMods toplevelFC [] fname
ok <- buildMods toplevelFC 1 (length mods) mods
= do mods <- getBuildMods EmptyFC [] fname
ok <- buildMods EmptyFC 1 (length mods) mods
case ok of
[] => do -- On success, reload the main ttc in a clean context
clearCtxt; addPrimitives
put MD (initMetadata fname)
modIdent <- ctxtPathToNS fname
put MD (initMetadata (PhysicalIdrSrc modIdent))
mainttc <- getTTCFileName fname "ttc"
log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname
readAsMain mainttc
@ -254,10 +257,10 @@ buildAll : {auto c : Ref Ctxt Defs} ->
(allFiles : List String) ->
Core (List Error)
buildAll allFiles
= do mods <- getAllBuildMods toplevelFC [] allFiles
= do mods <- getAllBuildMods EmptyFC [] allFiles
-- There'll be duplicates, so if something is already built, drop it
let mods' = dropLater mods
buildMods toplevelFC 1 (length mods') mods'
buildMods EmptyFC 1 (length mods') mods'
where
dropLater : List BuildMod -> List BuildMod
dropLater [] = []

93
src/Idris/Package.idr
View File

@ -7,6 +7,7 @@ import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Name.Namespace
import Core.Options
import Core.Unify
@ -108,14 +109,14 @@ field fname
equals
vs <- sepBy1 dot' integerLit
end <- location
pure (PVersion (MkFC fname start end)
pure (PVersion (MkFC (PhysicalPkgSrc fname) start end)
(MkPkgVersion (fromInteger <$> vs)))
<|> do start <- location
ignore $ exactProperty "version"
equals
v <- stringLit
end <- location
pure (PVersionDep (MkFC fname start end) v)
pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)
<|> do ignore $ exactProperty "depends"
equals
ds <- sep depends
@ -125,14 +126,14 @@ field fname
ms <- sep (do start <- location
m <- moduleIdent
end <- location
pure (MkFC fname start end, m))
pure (MkFC (PhysicalPkgSrc fname) start end, m))
pure (PModules ms)
<|> do ignore $ exactProperty "main"
equals
start <- location
m <- moduleIdent
end <- location
pure (PMainMod (MkFC fname start end) m)
pure (PMainMod (MkFC (PhysicalPkgSrc fname) start end) m)
<|> do ignore $ exactProperty "executable"
equals
e <- (stringLit <|> packageName)
@ -186,7 +187,7 @@ field fname
equals
str <- stringLit
end <- location
pure $ fieldConstructor (MkFC fname start end) str
pure $ fieldConstructor (MkFC (PhysicalPkgSrc fname) start end) str
parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
@ -284,10 +285,11 @@ compileMain : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
Name -> String -> String -> Core ()
compileMain mainn mmod exec
= do m <- newRef MD (initMetadata mmod)
compileMain mainn mfilename exec
= do modIdent <- ctxtPathToNS mfilename
m <- newRef MD (initMetadata (PhysicalIdrSrc modIdent))
u <- newRef UST initUState
ignore $ loadMainFile mmod
ignore $ loadMainFile mfilename
ignore $ compileExp (PRef replFC mainn) exec
prepareCompilation : {auto c : Ref Ctxt Defs} ->
@ -342,7 +344,7 @@ copyFile src dest
installFrom : {auto c : Ref Ctxt Defs} ->
String -> String -> ModuleIdent -> Core ()
installFrom builddir destdir ns
= do let ttcfile = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
= do let ttcfile = ModuleIdent.toPath ns
let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
let modPath = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
@ -361,6 +363,43 @@ installFrom builddir destdir ns
, show err ]
pure ()
installSrcFrom : {auto c : Ref Ctxt Defs} ->
String -> String -> (ModuleIdent, FileName) -> Core ()
installSrcFrom wdir destdir (ns, srcRelPath)
= do let srcfile = ModuleIdent.toPath ns
let srcPath = wdir </> srcRelPath
let Just ext = extension srcPath
| _ => throw (InternalError $
"Unexpected failure when installing source file:\n"
++ srcPath
++ "\n"
++ "Can't extract file extension.")
let modPath = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
let destNest = joinPath modPath
let destPath = destdir </> destNest
let destFile = destdir </> srcfile <.> ext
Right _ <- coreLift $ mkdirAll $ destNest
| Left err => throw $ InternalError $ unlines
[ "Can't make directories " ++ show modPath
, show err ]
coreLift $ putStrLn $ "Installing " ++ srcPath ++ " to " ++ destPath
when !(coreLift $ exists destFile) $ do
-- Grant read/write access to the file we are about to overwrite.
Right _ <- coreLift $ chmod destFile
(MkPermissions [Read, Write] [Read, Write] [Read, Write])
| Left err => throw $ UserError (show err)
pure ()
Right _ <- coreLift $ copyFile srcPath destFile
| Left err => throw $ InternalError $ unlines
[ "Can't copy file " ++ srcPath ++ " to " ++ destPath
, show err ]
-- Make the source read-only
Right _ <- coreLift $ chmod destFile (MkPermissions [Read] [Read] [Read])
| Left err => throw $ UserError (show err)
pure ()
-- Install all the built modules in prefix/package/
-- We've already built and checked for success, so if any don't exist that's
-- an internal error.
@ -368,15 +407,17 @@ install : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc ->
List CLOpt ->
(installSrc : Bool) ->
Core ()
install pkg opts -- not used but might be in the future
install pkg opts installSrc -- not used but might be in the future
= do defs <- get Ctxt
let build = build_dir (dirs (options defs))
let src = source_dir (dirs (options defs))
runScript (preinstall pkg)
let toInstall = maybe (map fst (modules pkg))
(\ m => fst m :: map fst (modules pkg))
let toInstall = maybe (modules pkg)
(:: modules pkg)
(mainmod pkg)
Just srcdir <- coreLift currentDir
Just wdir <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
-- Make the package installation directory
let installPrefix = prefix_dir (dirs (options defs)) </>
@ -391,10 +432,15 @@ install pkg opts -- not used but might be in the future
| False => throw $ InternalError $ "Can't change directory to " ++ installDir pkg
-- We're in that directory now, so copy the files from
-- srcdir/build into it
traverse_ (installFrom (srcdir </> build)
(installPrefix </> installDir pkg)) toInstall
coreLift_ $ changeDir srcdir
-- wdir/build into it
traverse_ (installFrom (wdir </> build)
(installPrefix </> installDir pkg))
(map fst toInstall)
when installSrc $ do
traverse_ (installSrcFrom wdir
(installPrefix </> installDir pkg))
toInstall
coreLift_ $ changeDir wdir
runScript (postinstall pkg)
-- Check package without compiling anything.
@ -559,7 +605,12 @@ runRepl : {auto c : Ref Ctxt Defs} ->
Core ()
runRepl fname = do
u <- newRef UST initUState
m <- newRef MD (initMetadata $ fromMaybe "(interactive)" fname)
origin <- maybe
(pure $ Virtual Interactive) (\fname => do
modIdent <- ctxtPathToNS fname
pure (PhysicalIdrSrc modIdent)
) fname
m <- newRef MD (initMetadata origin)
the (Core ()) $
case fname of
Nothing => pure ()
@ -618,7 +669,11 @@ processPackage opts (cmd, file)
pure ()
Install => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
install pkg opts
install pkg opts {installSrc = False}
InstallWithSrc =>
do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
install pkg opts {installSrc = True}
Typecheck => do
[] <- check pkg opts
| errs => coreLift (exitWith (ExitFailure 1))

222
src/Idris/Parser.idr
View File

@ -20,54 +20,54 @@ import Idris.Parser.Let
%default covering
decorate : FileName -> Decoration -> Rule a -> Rule a
decorate : OriginDesc -> Decoration -> Rule a -> Rule a
decorate fname decor rule = do
res <- bounds rule
act [((fname, (start res, end res)), decor, Nothing)]
pure res.val
decorationFromBounded : FileName -> Decoration -> WithBounds a -> ASemanticDecoration
decorationFromBounded : OriginDesc -> Decoration -> WithBounds a -> ASemanticDecoration
decorationFromBounded fname decor bnds
= ((fname, start bnds, end bnds), decor, Nothing)
boundedNameDecoration : FileName -> Decoration -> WithBounds Name -> ASemanticDecoration
boundedNameDecoration : OriginDesc -> Decoration -> WithBounds Name -> ASemanticDecoration
boundedNameDecoration fname decor bstr = ((fname, start bstr, end bstr)
, decor
, Just bstr.val)
decorateBoundedNames : FileName -> Decoration -> List (WithBounds Name) -> EmptyRule ()
decorateBoundedNames : OriginDesc -> Decoration -> List (WithBounds Name) -> EmptyRule ()
decorateBoundedNames fname decor bns = act $ map (boundedNameDecoration fname decor) bns
decorateBoundedName : FileName -> Decoration -> WithBounds Name -> EmptyRule ()
decorateBoundedName : OriginDesc -> Decoration -> WithBounds Name -> EmptyRule ()
decorateBoundedName fname decor bn = act [boundedNameDecoration fname decor bn]
decorateKeywords : FileName -> List (WithBounds a) -> EmptyRule ()
decorateKeywords : OriginDesc -> List (WithBounds a) -> EmptyRule ()
decorateKeywords fname = act . map (decorationFromBounded fname Keyword)
dependentDecorate : FileName -> Rule a -> (a -> Decoration) -> Rule a
dependentDecorate : OriginDesc -> Rule a -> (a -> Decoration) -> Rule a
dependentDecorate fname rule decor = do
res <- bounds rule
act [((fname, (start res, end res)), decor res.val, Nothing)]
pure res.val
decoratedKeyword : FileName -> String -> Rule ()
decoratedKeyword : OriginDesc -> String -> Rule ()
decoratedKeyword fname kwd = decorate fname Keyword (keyword kwd)
decoratedSymbol : FileName -> String -> Rule ()
decoratedSymbol : OriginDesc -> String -> Rule ()
decoratedSymbol fname smb = decorate fname Keyword (symbol smb)
decoratedDataTypeName : FileName -> Rule Name
decoratedDataTypeName : OriginDesc -> Rule Name
decoratedDataTypeName fname = decorate fname Typ dataTypeName
decoratedDataConstructorName : FileName -> Rule Name
decoratedDataConstructorName : OriginDesc -> Rule Name
decoratedDataConstructorName fname = decorate fname Data dataConstructorName
decoratedSimpleBinderName : FileName -> Rule String
decoratedSimpleBinderName : OriginDesc -> Rule String
decoratedSimpleBinderName fname = decorate fname Bound unqualifiedName
-- Forward declare since they're used in the parser
topDecl : FileName -> IndentInfo -> Rule (List PDecl)
topDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
collectDefs : List PDecl -> List PDecl
-- Some context for the parser
@ -103,7 +103,7 @@ plhs = MkParseOpts False False
%hide Prelude.(<*>)
%hide Core.Core.(<*>)
atom : FileName -> Rule PTerm
atom : OriginDesc -> Rule PTerm
atom fname
= do x <- bounds $ decorate fname Typ $ exactIdent "Type"
pure (PType (boundToFC fname x))
@ -127,14 +127,14 @@ atom fname
<|> do x <- bounds $ pragma "search"
pure (PSearch (boundToFC fname x) 50)
whereBlock : FileName -> Int -> Rule (List PDecl)
whereBlock : OriginDesc -> Int -> Rule (List PDecl)
whereBlock fname col
= do decoratedKeyword fname "where"
ds <- blockAfter col (topDecl fname)
pure (collectDefs (concat ds))
-- Expect a keyword, but if we get anything else it's a fatal error
commitKeyword : FileName -> IndentInfo -> String -> Rule ()
commitKeyword : OriginDesc -> IndentInfo -> String -> Rule ()
commitKeyword fname indents req
= do mustContinue indents (Just req)
decoratedKeyword fname req
@ -145,7 +145,7 @@ commitSymbol req
= symbol req
<|> fatalError ("Expected '" ++ req ++ "'")
continueWithDecorated : FileName -> IndentInfo -> String -> Rule ()
continueWithDecorated : OriginDesc -> IndentInfo -> String -> Rule ()
continueWithDecorated fname indents req
= mustContinue indents (Just req) *> decoratedSymbol fname req
@ -171,7 +171,7 @@ argTerm (NamedArg _ t) = t
argTerm (WithArg t) = t
mutual
appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
appExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
appExpr q fname indents
= case_ fname indents
<|> doBlock fname indents
@ -201,7 +201,7 @@ mutual
applyExpImp start end f (WithArg exp :: args)
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule (List ArgType)
argExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule (List ArgType)
argExpr q fname indents
= do continue indents
arg <- simpleExpr fname indents
@ -220,7 +220,7 @@ mutual
underscore : FC -> ArgType
underscore fc = NamedArg (UN "_") (PImplicit fc)
braceArgs : FileName -> IndentInfo -> Rule (List ArgType)
braceArgs : OriginDesc -> IndentInfo -> Rule (List ArgType)
braceArgs fname indents
= do start <- bounds (decoratedSymbol fname "{")
list <- sepBy (decoratedSymbol fname ",")
@ -247,7 +247,7 @@ mutual
decoratedSymbol fname "}"
pure [UnnamedAutoArg tm]
with_ : FileName -> IndentInfo -> Rule PTerm
with_ : OriginDesc -> IndentInfo -> Rule PTerm
with_ fname indents
= do b <- bounds (do decoratedKeyword fname "with"
commit
@ -271,7 +271,7 @@ mutual
decoratedSymbol fname "]"
pure (forget ns)
opExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
opExpr q fname indents
= do l <- bounds (appExpr q fname indents)
(if eqOK q
@ -289,7 +289,7 @@ mutual
pure (POp fc opFC op.val l.val r))
<|> pure l.val
dpairType : FileName -> WithBounds t -> IndentInfo -> Rule PTerm
dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
dpairType fname start indents
= do loc <- bounds (do x <- decoratedSimpleBinderName fname
decoratedSymbol fname ":"
@ -304,7 +304,7 @@ mutual
ty
rest.val)
nestedDpair : FileName -> WithBounds t -> IndentInfo -> Rule PTerm
nestedDpair : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
nestedDpair fname start indents
= dpairType fname start indents
<|> do l <- expr pdef fname indents
@ -316,7 +316,7 @@ mutual
(PImplicit (boundToFC fname (mergeBounds start rest)))
rest.val)
bracketedExpr : FileName -> WithBounds t -> IndentInfo -> Rule PTerm
bracketedExpr : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
bracketedExpr fname s indents
-- left section. This may also be a prefix operator, but we'll sort
-- that out when desugaring: if the operator is infix, treat it as a
@ -371,7 +371,7 @@ mutual
getInitRange [x,y] = pure (x.val, Just y.val)
getInitRange _ = fatalError "Invalid list range syntax"
listRange : FileName -> WithBounds t -> IndentInfo -> List (WithBounds PTerm) -> Rule PTerm
listRange : OriginDesc -> WithBounds t -> IndentInfo -> List (WithBounds PTerm) -> Rule PTerm
listRange fname s indents xs
= do b <- bounds (decoratedSymbol fname "]")
let fc = boundToFC fname (mergeBounds s b)
@ -384,7 +384,7 @@ mutual
decorateKeywords fname xs
pure (PRange fc (fst rstate) (snd rstate) y.val)
listExpr : FileName -> WithBounds () -> IndentInfo -> Rule PTerm
listExpr : OriginDesc -> WithBounds () -> IndentInfo -> Rule PTerm
listExpr fname s indents
= do b <- bounds (do ret <- expr pnowith fname indents
decoratedSymbol fname "|"
@ -407,7 +407,7 @@ mutual
nilFC = if null xs then fc else boundToFC fname b
in PList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs))
snocListExpr : FileName -> WithBounds () -> IndentInfo -> Rule PTerm
snocListExpr : OriginDesc -> WithBounds () -> IndentInfo -> Rule PTerm
snocListExpr fname s indents
= {- TODO: comprehension -}
do mHeadTail <- optional $ do
@ -427,7 +427,7 @@ mutual
nilFC = ifThenElse (null xs) fc (boundToFC fname s)
in PSnocList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs) --)
nonEmptyTuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
nonEmptyTuple : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
nonEmptyTuple fname s indents e
= do vals <- some $ do b <- bounds (symbol ",")
exp <- optional (expr pdef fname indents)
@ -463,14 +463,14 @@ mutual
(var ++ vars, PPair (fst exp) t ts)
-- A pair, dependent pair, or just a single expression
tuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
tuple : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
tuple fname s indents e
= nonEmptyTuple fname s indents e
<|> do end <- bounds (continueWithDecorated fname indents ")")
act [(toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)]
pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
simpleExpr : FileName -> IndentInfo -> Rule PTerm
simpleExpr : OriginDesc -> IndentInfo -> Rule PTerm
simpleExpr fname indents
= do -- x.y.z
b <- bounds (do root <- simplerExpr fname indents
@ -485,7 +485,7 @@ mutual
pure $ let projs = map (\ proj => (boundToFC fname proj, proj.val)) b.val in
PPostfixAppPartial (boundToFC fname b) projs
simplerExpr : FileName -> IndentInfo -> Rule PTerm
simplerExpr : OriginDesc -> IndentInfo -> Rule PTerm
simplerExpr fname indents
= do b <- bounds (do x <- bounds (decoratedSimpleBinderName fname)
decoratedSymbol fname "@"
@ -530,7 +530,7 @@ mutual
(lvl, e) <- pure b.val
pure (PUnifyLog (boundToFC fname b) lvl e)
multiplicity : FileName -> EmptyRule RigCount
multiplicity : OriginDesc -> EmptyRule RigCount
multiplicity fname
= case !(optional $ decorate fname Keyword intLit) of
(Just 0) => pure erased
@ -538,14 +538,14 @@ mutual
Nothing => pure top
_ => fail "Invalid multiplicity (must be 0 or 1)"
pibindAll : FileName -> PiInfo PTerm ->
pibindAll : OriginDesc -> PiInfo PTerm ->
List (RigCount, WithBounds (Maybe Name), PTerm) ->
PTerm -> PTerm
pibindAll fname p [] scope = scope
pibindAll fname p ((rig, n, ty) :: rest) scope
= PPi (boundToFC fname n) rig p (n.val) ty (pibindAll fname p rest scope)
bindList : FileName -> IndentInfo ->
bindList : OriginDesc -> IndentInfo ->
Rule (List (RigCount, WithBounds PTerm, PTerm))
bindList fname indents
= forget <$> sepBy1 (decoratedSymbol fname ",")
@ -556,7 +556,7 @@ mutual
(decoratedSymbol fname ":" *> opExpr pdef fname indents)
pure (rig, pat, ty))
pibindListName : FileName -> IndentInfo ->
pibindListName : OriginDesc -> IndentInfo ->
Rule (List (RigCount, WithBounds Name, PTerm))
pibindListName fname indents
= do rig <- multiplicity fname
@ -578,18 +578,18 @@ mutual
binderName : Rule String
binderName = unqualifiedName <|> (symbol "_" $> "_")
pibindList : FileName -> IndentInfo ->
pibindList : OriginDesc -> IndentInfo ->
Rule (List (RigCount, WithBounds (Maybe Name), PTerm))
pibindList fname indents
= do params <- pibindListName fname indents
pure $ map (\(rig, n, ty) => (rig, map Just n, ty)) params
bindSymbol : FileName -> Rule (PiInfo PTerm)
bindSymbol : OriginDesc -> Rule (PiInfo PTerm)
bindSymbol fname
= (decoratedSymbol fname "->" $> Explicit)
<|> (decoratedSymbol fname "=>" $> AutoImplicit)
explicitPi : FileName -> IndentInfo -> Rule PTerm
explicitPi : OriginDesc -> IndentInfo -> Rule PTerm
explicitPi fname indents
= do decoratedSymbol fname "("
binders <- pibindList fname indents
@ -598,7 +598,7 @@ mutual
scope <- mustWork $ typeExpr pdef fname indents
pure (pibindAll fname exp binders scope)
autoImplicitPi : FileName -> IndentInfo -> Rule PTerm
autoImplicitPi : OriginDesc -> IndentInfo -> Rule PTerm
autoImplicitPi fname indents
= do decoratedSymbol fname "{"
decoratedKeyword fname "auto"
@ -609,7 +609,7 @@ mutual
scope <- mustWork $ typeExpr pdef fname indents
pure (pibindAll fname AutoImplicit binders scope)
defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm
defaultImplicitPi : OriginDesc -> IndentInfo -> Rule PTerm
defaultImplicitPi fname indents
= do decoratedSymbol fname "{"
decoratedKeyword fname "default"
@ -621,7 +621,7 @@ mutual
scope <- mustWork $ typeExpr pdef fname indents
pure (pibindAll fname (DefImplicit t) binders scope)
forall_ : FileName -> IndentInfo -> Rule PTerm
forall_ : OriginDesc -> IndentInfo -> Rule PTerm
forall_ fname indents
= do decoratedKeyword fname "forall"
commit
@ -635,7 +635,7 @@ mutual
scope <- mustWork $ typeExpr pdef fname indents
pure (pibindAll fname Implicit binders scope)
implicitPi : FileName -> IndentInfo -> Rule PTerm
implicitPi : OriginDesc -> IndentInfo -> Rule PTerm
implicitPi fname indents
= do decoratedSymbol fname "{"
binders <- pibindList fname indents
@ -644,7 +644,7 @@ mutual
scope <- mustWork $ typeExpr pdef fname indents
pure (pibindAll fname Implicit binders scope)
lam : FileName -> IndentInfo -> Rule PTerm
lam : OriginDesc -> IndentInfo -> Rule PTerm
lam fname indents
= do decoratedSymbol fname "\\"
commit
@ -679,7 +679,7 @@ mutual
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
PCase (virtualiseFC fc) (PRef fcCase n) b.val)
letBlock : FileName -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
letBlock : OriginDesc -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
letBlock fname indents = bounds (letBinder <||> letDecl) where
letBinder : Rule LetBinder
@ -695,7 +695,7 @@ mutual
letDecl : Rule LetDecl
letDecl = collectDefs . concat <$> nonEmptyBlock (try . topDecl fname)
let_ : FileName -> IndentInfo -> Rule PTerm
let_ : OriginDesc -> IndentInfo -> Rule PTerm
let_ fname indents
= do decoratedKeyword fname "let"
commit
@ -704,7 +704,7 @@ mutual
scope <- typeExpr pdef fname indents
pure (mkLets fname res scope)
case_ : FileName -> IndentInfo -> Rule PTerm
case_ : OriginDesc -> IndentInfo -> Rule PTerm
case_ fname indents
= do b <- bounds (do decoratedKeyword fname "case"
scr <- expr pdef fname indents
@ -715,12 +715,12 @@ mutual
pure (PCase (virtualiseFC $ boundToFC fname b) scr alts)
caseAlt : FileName -> IndentInfo -> Rule PClause
caseAlt : OriginDesc -> IndentInfo -> Rule PClause
caseAlt fname indents
= do lhs <- bounds (opExpr plhs fname indents)
caseRHS fname lhs indents lhs.val
caseRHS : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PClause
caseRHS : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PClause
caseRHS fname start indents lhs
= do rhs <- bounds (decoratedSymbol fname "=>" *> mustContinue indents Nothing *> expr pdef fname indents)
atEnd indents
@ -730,7 +730,7 @@ mutual
atEnd indents
pure (MkImpossible (boundToFC fname (mergeBounds start end)) lhs)
if_ : FileName -> IndentInfo -> Rule PTerm
if_ : OriginDesc -> IndentInfo -> Rule PTerm
if_ fname indents
= do b <- bounds (do decoratedKeyword fname "if"
x <- expr pdef fname indents
@ -743,7 +743,7 @@ mutual
(x, t, e) <- pure b.val
pure (PIfThenElse (boundToFC fname b) x t e)
record_ : FileName -> IndentInfo -> Rule PTerm
record_ : OriginDesc -> IndentInfo -> Rule PTerm
record_ fname indents
= do b <- bounds (do kw <- option False
(decoratedKeyword fname "record"
@ -755,7 +755,7 @@ mutual
pure $ forget fs)
pure (PUpdate (boundToFC fname b) b.val)
field : Bool -> FileName -> IndentInfo -> Rule PFieldUpdate
field : Bool -> OriginDesc -> IndentInfo -> Rule PFieldUpdate
field kw fname indents
= do path <- map fieldName <$> [| decorate fname Function name :: many recFieldCompat |]
upd <- (ifThenElse kw (decoratedSymbol fname "=") (decoratedSymbol fname ":=") $> PSetField)
@ -776,7 +776,7 @@ mutual
<|> (decoratedSymbol fname "->"
*> decorate fname Function name)
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ : OriginDesc -> IndentInfo -> Rule PTerm
rewrite_ fname indents
= do b <- bounds (do decoratedKeyword fname "rewrite"
rule <- expr pdef fname indents
@ -786,7 +786,7 @@ mutual
(rule, tm) <- pure b.val
pure (PRewrite (boundToFC fname b) rule tm)
doBlock : FileName -> IndentInfo -> Rule PTerm
doBlock : OriginDesc -> IndentInfo -> Rule PTerm
doBlock fname indents
= do b <- bounds $ keyword "do" *> block (doAct fname)
commit
@ -808,7 +808,7 @@ mutual
else fail "Not a pattern variable"
validPatternVar _ = fail "Not a pattern variable"
doAct : FileName -> IndentInfo -> Rule (List PDo)
doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
doAct fname indents
= do b <- bounds (do n <- bounds name
-- If the name doesn't begin with a lower case letter, we should
@ -836,12 +836,12 @@ mutual
let fc = virtualiseFC $ boundToFC fname (mergeBounds e b)
pure [DoBindPat fc e.val v alts])
patAlt : FileName -> IndentInfo -> Rule PClause
patAlt : OriginDesc -> IndentInfo -> Rule PClause
patAlt fname indents
= do decoratedSymbol fname "|"
caseAlt fname indents
lazy : FileName -> IndentInfo -> Rule PTerm
lazy : OriginDesc -> IndentInfo -> Rule PTerm
lazy fname indents
= do tm <- bounds (decorate fname Typ (exactIdent "Lazy")
*> simpleExpr fname indents)
@ -856,7 +856,7 @@ mutual
*> simpleExpr fname indents)
pure (PForce (boundToFC fname tm) tm.val)
binder : FileName -> IndentInfo -> Rule PTerm
binder : OriginDesc -> IndentInfo -> Rule PTerm
binder fname indents
= let_ fname indents
<|> autoImplicitPi fname indents
@ -866,7 +866,7 @@ mutual
<|> explicitPi fname indents
<|> lam fname indents
typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
typeExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
typeExpr q fname indents
= do arg <- bounds (opExpr q fname indents)
(do continue indents
@ -881,14 +881,14 @@ mutual
(mkPi a as)
export
expr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
expr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
expr = typeExpr
interpBlock : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
interpBlock : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
interpBlock q fname idents = interpBegin *> (mustWork $ expr q fname idents) <* interpEnd
export
singlelineStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
singlelineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
singlelineStr q fname idents
= decorate fname Data $
do b <- bounds $ do begin <- bounds strBegin
@ -908,7 +908,7 @@ mutual
Left tm => Right $ StrInterp (boundToFC fname x) tm
export
multilineStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
multilineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
multilineStr q fname idents
= decorate fname Data $
do b <- bounds $ do multilineBegin
@ -930,18 +930,18 @@ mutual
((acc `snoc` (line `snoc` (StrLiteral (boundToFC fname x) str))) ++
((\str => [StrLiteral (boundToFC fname x) str]) <$> (init strs)))
visOption : FileName -> Rule Visibility
visOption : OriginDesc -> Rule Visibility
visOption fname
= (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public)
<|> (decoratedKeyword fname "export" $> Export)
<|> (decoratedKeyword fname "private" $> Private)
visibility : FileName -> EmptyRule Visibility
visibility : OriginDesc -> EmptyRule Visibility
visibility fname
= visOption fname
<|> pure Private
tyDecls : Rule Name -> String -> FileName -> IndentInfo -> Rule (List1 PTypeDecl)
tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule (List1 PTypeDecl)
tyDecls declName predoc fname indents
= do bs <- do docns <- sepBy1 (decoratedSymbol fname ",") [| (option "" documentation, bounds declName) |]
decoratedSymbol fname ":"
@ -959,7 +959,7 @@ withFlags
mutual
parseRHS : (withArgs : Nat) ->
FileName -> WithBounds t -> Int ->
OriginDesc -> WithBounds t -> Int ->
IndentInfo -> (lhs : PTerm) -> Rule PClause
parseRHS withArgs fname start col indents lhs
= do b <- bounds $ decoratedSymbol fname "=" *> mustWork [| (expr pdef fname indents, option [] $ whereBlock fname col) |]
@ -983,7 +983,7 @@ mutual
atEnd indents
pure (MkImpossible (boundToFC fname (mergeBounds start end)) lhs)
clause : Nat -> FileName -> IndentInfo -> Rule PClause
clause : Nat -> OriginDesc -> IndentInfo -> Rule PClause
clause withArgs fname indents
= do b <- bounds (do col <- column
lhs <- expr plhs fname indents
@ -1008,7 +1008,7 @@ mutual
tm <- bounds (expr plhs fname indents)
pure (boundToFC fname tm, tm.val)
mkTyConType : FileName -> FC -> List (WithBounds Name) -> PTerm
mkTyConType : OriginDesc -> FC -> List (WithBounds Name) -> PTerm
mkTyConType fname fc [] = PType (virtualiseFC fc)
mkTyConType fname fc (x :: xs)
= let bfc = boundToFC fname x in
@ -1024,7 +1024,7 @@ mkDataConType fc ret (UnnamedAutoArg x :: xs)
mkDataConType _ _ _ -- with and named applications not allowed in simple ADTs
= Nothing
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon : OriginDesc -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon fname ret indents
= do b <- bounds (do cdoc <- option "" documentation
cname <- bounds $ decoratedDataConstructorName fname
@ -1036,7 +1036,7 @@ simpleCon fname ret indents
fromMaybe (fatalError "Named arguments not allowed in ADT constructors")
(pure . MkPTy cfc cnameFC cname cdoc <$> mkDataConType cfc ret (concat params))
simpleData : FileName -> WithBounds t ->
simpleData : OriginDesc -> WithBounds t ->
WithBounds Name -> IndentInfo -> Rule PDataDecl
simpleData fname start tyName indents
= do b <- bounds (do params <- many (bounds $ decorate fname Bound name)
@ -1059,7 +1059,7 @@ dataOpt
<|> (exactIdent "external" $> External)
<|> (exactIdent "noNewtype" $> NoNewtype)
dataBody : FileName -> Int -> WithBounds t -> Name -> IndentInfo -> PTerm ->
dataBody : OriginDesc -> Int -> WithBounds t -> Name -> IndentInfo -> PTerm ->
EmptyRule PDataDecl
dataBody fname mincol start n indents ty
= do atEndIndent indents
@ -1071,7 +1071,7 @@ dataBody fname mincol start n indents ty
(opts, cs) <- pure b.val
pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs)
gadtData : FileName -> Int -> WithBounds t ->
gadtData : OriginDesc -> Int -> WithBounds t ->
WithBounds Name -> IndentInfo -> Rule PDataDecl
gadtData fname mincol start tyName indents
= do decoratedSymbol fname ":"
@ -1079,7 +1079,7 @@ gadtData fname mincol start tyName indents
ty <- expr pdef fname indents
dataBody fname mincol start tyName.val indents ty
dataDeclBody : FileName -> IndentInfo -> Rule PDataDecl
dataDeclBody : OriginDesc -> IndentInfo -> Rule PDataDecl
dataDeclBody fname indents
= do b <- bounds (do col <- column
decoratedKeyword fname "data"
@ -1088,7 +1088,7 @@ dataDeclBody fname indents
(col, n) <- pure b.val
simpleData fname b n indents <|> gadtData fname col b n indents
dataDecl : FileName -> IndentInfo -> Rule PDecl
dataDecl : OriginDesc -> IndentInfo -> Rule PDecl
dataDecl fname indents
= do b <- bounds (do doc <- option "" documentation
vis <- visibility fname
@ -1114,7 +1114,7 @@ extension
= (exactIdent "ElabReflection" $> ElabReflection)
<|> (exactIdent "Borrowing" $> Borrowing)
totalityOpt : FileName -> Rule TotalReq
totalityOpt : OriginDesc -> Rule TotalReq
totalityOpt fname
= (decoratedKeyword fname "partial" $> PartialOK)
<|> (decoratedKeyword fname "total" $> Total)
@ -1128,7 +1128,7 @@ logLevel
pure (Just (mkLogLevel' topic (fromInteger lvl)))
<|> fail "expected a log level"
directive : FileName -> IndentInfo -> Rule Directive
directive : OriginDesc -> IndentInfo -> Rule Directive
directive fname indents
= do decorate fname Keyword $ pragma "hide"
n <- name
@ -1226,7 +1226,7 @@ fix
namespaceHead : Rule Namespace
namespaceHead = keyword "namespace" *> mustWork namespaceId
namespaceDecl : FileName -> IndentInfo -> Rule PDecl
namespaceDecl : OriginDesc -> IndentInfo -> Rule PDecl
namespaceDecl fname indents
= do b <- bounds (do doc <- option "" documentation
col <- column
@ -1236,7 +1236,7 @@ namespaceDecl fname indents
(doc, ns, ds) <- pure b.val
pure (PNamespace (boundToFC fname b) ns (collectDefs $ concat ds))
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl : OriginDesc -> IndentInfo -> Rule PDecl
transformDecl fname indents
= do b <- bounds (do pragma "transform"
n <- simpleStr
@ -1247,17 +1247,17 @@ transformDecl fname indents
(n, lhs, rhs) <- pure b.val
pure (PTransform (boundToFC fname b) n lhs rhs)
runElabDecl : FileName -> IndentInfo -> Rule PDecl
runElabDecl : OriginDesc -> IndentInfo -> Rule PDecl
runElabDecl fname indents
= do tm <- bounds (pragma "runElab" *> expr pnowith fname indents)
pure (PRunElabDecl (boundToFC fname tm) tm.val)
mutualDecls : FileName -> IndentInfo -> Rule PDecl
mutualDecls : OriginDesc -> IndentInfo -> Rule PDecl
mutualDecls fname indents
= do ds <- bounds (decoratedKeyword fname "mutual" *> commit *> assert_total (nonEmptyBlock (topDecl fname)))
pure (PMutual (boundToFC fname ds) (concat ds.val))
usingDecls : FileName -> IndentInfo -> Rule PDecl
usingDecls : OriginDesc -> IndentInfo -> Rule PDecl
usingDecls fname indents
= do b <- bounds (do decoratedKeyword fname "using"
commit
@ -1275,12 +1275,12 @@ usingDecls fname indents
(us, ds) <- pure b.val
pure (PUsing (boundToFC fname b) us (collectDefs (concat ds)))
fnOpt : FileName -> Rule PFnOpt
fnOpt : OriginDesc -> Rule PFnOpt
fnOpt fname
= do x <- totalityOpt fname
pure $ IFnOpt (Totality x)
fnDirectOpt : FileName -> Rule PFnOpt
fnDirectOpt : OriginDesc -> Rule PFnOpt
fnDirectOpt fname
= do pragma "hint"
pure $ IFnOpt (Hint True)
@ -1305,7 +1305,7 @@ fnDirectOpt fname
cs <- block (expr pdef fname)
pure $ PForeign cs
builtinDecl : FileName -> IndentInfo -> Rule PDecl
builtinDecl : OriginDesc -> IndentInfo -> Rule PDecl
builtinDecl fname indents
= do b <- bounds (do pragma "builtin"
commit
@ -1315,7 +1315,7 @@ builtinDecl fname indents
(t, n) <- pure b.val
pure $ PBuiltin (boundToFC fname b) t n
visOpt : FileName -> Rule (Either Visibility PFnOpt)
visOpt : OriginDesc -> Rule (Either Visibility PFnOpt)
visOpt fname
= do vis <- visOption fname
pure (Left vis)
@ -1333,13 +1333,13 @@ getVisibility (Just vis) (Left x :: xs)
= fatalError "Multiple visibility modifiers"
getVisibility v (_ :: xs) = getVisibility v xs
recordConstructor : FileName -> Rule Name
recordConstructor : OriginDesc -> Rule Name
recordConstructor fname
= do exactIdent "constructor"
n <- mustWork $ decoratedDataConstructorName fname
pure n
constraints : FileName -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
constraints : OriginDesc -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
constraints fname indents
= do tm <- appExpr pdef fname indents
decoratedSymbol fname "=>"
@ -1355,7 +1355,7 @@ constraints fname indents
pure ((Just n, tm) :: more)
<|> pure []
implBinds : FileName -> IndentInfo -> EmptyRule (List (Name, RigCount, PTerm))
implBinds : OriginDesc -> IndentInfo -> EmptyRule (List (Name, RigCount, PTerm))
implBinds fname indents
= do decoratedSymbol fname "{"
rig <- multiplicity fname
@ -1368,7 +1368,7 @@ implBinds fname indents
pure ((n, rig, tm) :: more)
<|> pure []
ifaceParam : FileName -> IndentInfo -> Rule (List Name, (RigCount, PTerm))
ifaceParam : OriginDesc -> IndentInfo -> Rule (List Name, (RigCount, PTerm))
ifaceParam fname indents
= do decoratedSymbol fname "("
rig <- multiplicity fname
@ -1380,7 +1380,7 @@ ifaceParam fname indents
<|> do n <- bounds (decorate fname Bound name)
pure ([n.val], (erased, PInfer (boundToFC fname n)))
ifaceDecl : FileName -> IndentInfo -> Rule PDecl
ifaceDecl : OriginDesc -> IndentInfo -> Rule PDecl
ifaceDecl fname indents
= do b <- bounds (do doc <- option "" documentation
vis <- visibility fname
@ -1399,7 +1399,7 @@ ifaceDecl fname indents
vis cons n doc params det dc (collectDefs (concat body))))
pure (b.val (boundToFC fname b))
implDecl : FileName -> IndentInfo -> Rule PDecl
implDecl : OriginDesc -> IndentInfo -> Rule PDecl
implDecl fname indents
= do b <- bounds (do doc <- option "" documentation
visOpts <- many (visOpt fname)
@ -1423,7 +1423,7 @@ implDecl fname indents
atEnd indents
pure (b.val (boundToFC fname b))
fieldDecl : FileName -> IndentInfo -> Rule (List PField)
fieldDecl : OriginDesc -> IndentInfo -> Rule (List PField)
fieldDecl fname indents
= do doc <- option "" documentation
decoratedSymbol fname "{"
@ -1449,7 +1449,7 @@ fieldDecl fname indents
pure (\fc : FC => map (\n => MkField fc doc rig p n ty) (forget ns)))
pure (b.val (boundToFC fname b))
typedArg : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
typedArg : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
typedArg fname indents
= do decoratedSymbol fname "("
params <- pibindListName fname indents
@ -1465,13 +1465,13 @@ typedArg fname indents
decoratedSymbol fname "}"
pure $ map (\(c, n, tm) => (n.val, c, info, tm)) params
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam fname indents
= typedArg fname indents
<|> do n <- bounds name
pure [(n.val, top, Explicit, PInfer (boundToFC fname n))]
recordDecl : FileName -> IndentInfo -> Rule PDecl
recordDecl : OriginDesc -> IndentInfo -> Rule PDecl
recordDecl fname indents
= do b <- bounds (do doc <- option "" documentation
vis <- visibility fname
@ -1487,7 +1487,7 @@ recordDecl fname indents
pure (\fc : FC => PRecord fc doc vis n params (fst dcflds) (concat (snd dcflds))))
pure (b.val (boundToFC fname b))
paramDecls : FileName -> IndentInfo -> Rule PDecl
paramDecls : OriginDesc -> IndentInfo -> Rule PDecl
paramDecls fname indents
= do b1 <- bounds (decoratedKeyword fname "parameters")
commit
@ -1498,7 +1498,7 @@ paramDecls fname indents
pure (PParameters (boundToFC fname mergedBounds) args.val (collectDefs (concat declarations.val)))
where
oldParamDecls : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
oldParamDecls : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
oldParamDecls fname indents
= do decoratedSymbol fname "("
ps <- sepBy (decoratedSymbol fname ",")
@ -1509,12 +1509,12 @@ paramDecls fname indents
decoratedSymbol fname ")"
pure ps
newParamDecls : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
newParamDecls : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
newParamDecls fname indents
= map concat (some $ typedArg fname indents)
claims : FileName -> IndentInfo -> Rule (List1 PDecl)
claims : OriginDesc -> IndentInfo -> Rule (List1 PDecl)
claims fname indents
= do bs <- bounds (do
doc <- option "" documentation
@ -1529,12 +1529,12 @@ claims fname indents
PClaim (boundToFC fname bs) rig vis opts cl)
bs.val
definition : FileName -> IndentInfo -> Rule PDecl
definition : OriginDesc -> IndentInfo -> Rule PDecl
definition fname indents
= do nd <- bounds (clause 0 fname indents)
pure (PDef (boundToFC fname nd) [nd.val])
fixDecl : FileName -> IndentInfo -> Rule (List PDecl)
fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
fixDecl fname indents
= do b <- bounds (do fixity <- decorate fname Keyword $ fix
commit
@ -1544,7 +1544,7 @@ fixDecl fname indents
(fixity, prec, ops) <- pure b.val
pure (map (PFixity (boundToFC fname b) fixity (fromInteger prec)) (forget ops))
directiveDecl : FileName -> IndentInfo -> Rule PDecl
directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl
directiveDecl fname indents
= do b <- bounds ((do d <- directive fname indents
pure (\fc : FC => PDirective fc d))
@ -1556,7 +1556,7 @@ directiveDecl fname indents
pure (b.val (boundToFC fname b))
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> Rule (List PDecl)
-- topDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
topDecl fname indents
= do d <- dataDecl fname indents
pure [d]
@ -1621,7 +1621,7 @@ collectDefs (d :: ds)
= d :: collectDefs ds
export
import_ : FileName -> IndentInfo -> Rule Import
import_ : OriginDesc -> IndentInfo -> Rule Import
import_ fname indents
= do b <- bounds (do decoratedKeyword fname "import"
reexp <- option False (decoratedKeyword fname "public" $> True)
@ -1635,7 +1635,7 @@ import_ fname indents
pure (MkImport (boundToFC fname b) reexp ns nsAs)
export
prog : FileName -> EmptyRule Module
prog : OriginDesc -> EmptyRule Module
prog fname
= do b <- bounds (do doc <- option "" documentation
nspace <- option (nsAsModuleIdent mainNS)
@ -1649,7 +1649,7 @@ prog fname
nspace imports doc (collectDefs (concat ds)))
export
progHdr : FileName -> EmptyRule Module
progHdr : OriginDesc -> EmptyRule Module
progHdr fname
= do b <- bounds (do doc <- option "" documentation
nspace <- option (nsAsModuleIdent mainNS)
@ -1894,7 +1894,7 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
parse = do
symbol ":"
runParseCmd parseCmd
tm <- mustWork $ expr pdef "(interactive)" init
tm <- mustWork $ expr pdef (Virtual Interactive) init
pure (command tm)
declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition
@ -1906,7 +1906,7 @@ declsArgCmd parseCmd command doc = (names, DeclsArg, doc, parse)
parse = do
symbol ":"
runParseCmd parseCmd
tm <- mustWork $ topDecl "(interactive)" init
tm <- mustWork $ topDecl (Virtual Interactive) init
pure (command tm)
optArgCmd : ParseCmd -> (REPLOpt -> REPLCmd) -> Bool -> String -> CommandDefinition
@ -1977,7 +1977,7 @@ compileArgsCmd parseCmd command doc
symbol ":"
runParseCmd parseCmd
n <- mustWork unqualifiedName
tm <- mustWork $ expr pdef "(interactive)" init
tm <- mustWork $ expr pdef (Virtual Interactive) init
pure (command tm n)
loggingArgCmd : ParseCmd -> (Maybe LogLevel -> REPLCmd) -> String -> CommandDefinition
@ -2041,7 +2041,7 @@ nonEmptyCommand =
eval : Rule REPLCmd
eval = do
tm <- expr pdef "(interactive)" init
tm <- expr pdef (Virtual Interactive) init
pure (Eval tm)
export

16
src/Idris/Parser/Let.idr
View File

@ -52,11 +52,11 @@ letFactory letBind letDeclare blocks scope = foldr mkLet scope groups where
in letDeclare (concatMap val letDecls <$ bounds)
export
mkLets : FileName ->
mkLets : OriginDesc ->
List1 (WithBounds (Either LetBinder LetDecl)) ->
PTerm -> PTerm
mkLets fname = letFactory buildLets
(\ decls, scope => PLocal (virtualiseFC $ boundToFC fname decls) decls.val scope)
mkLets origin = letFactory buildLets
(\ decls, scope => PLocal (virtualiseFC $ boundToFC origin decls) decls.val scope)
where
@ -64,16 +64,16 @@ mkLets fname = letFactory buildLets
buildLets [] sc = sc
buildLets (b :: rest) sc
= let (MkLetBinder rig pat ty val alts) = b.val
fc = virtualiseFC $ boundToFC fname b
fc = virtualiseFC $ boundToFC origin b
in PLet fc rig pat ty val (buildLets rest sc) alts
export
mkDoLets : FileName ->
mkDoLets : OriginDesc ->
List1 (WithBounds (Either LetBinder LetDecl)) ->
List PDo
mkDoLets fname lets = letFactory
mkDoLets origin lets = letFactory
(\ binds, rest => buildDoLets binds ++ rest)
(\ decls, rest => DoLetLocal (boundToFC fname decls) decls.val :: rest)
(\ decls, rest => DoLetLocal (boundToFC origin decls) decls.val :: rest)
lets
[]
@ -81,7 +81,7 @@ mkDoLets fname lets = letFactory
buildDoLets : List (WithBounds LetBinder) -> List PDo
buildDoLets [] = []
buildDoLets (b :: rest) = let fc = boundToFC fname b in case b.val of
buildDoLets (b :: rest) = let fc = boundToFC origin b in case b.val of
(MkLetBinder rig (PRef fc' (UN n)) ty val []) =>
(if lowerFirst n
then DoLet fc fc' (UN n) rig ty val

36
src/Idris/ProcessIdr.idr
View File

@ -128,7 +128,7 @@ readHash imp
pure (reexport imp, (nameAs imp, h))
prelude : Import
prelude = MkImport (MkFC "(implicit)" (0, 0) (0, 0)) False
prelude = MkImport (MkFC (Virtual Interactive) (0, 0) (0, 0)) False
(nsAsModuleIdent preludeNS) preludeNS
export
@ -148,7 +148,7 @@ readAsMain : {auto c : Ref Ctxt Defs} ->
(fname : String) -> Core ()
readAsMain fname
= do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
True toplevelFC True fname (nsAsModuleIdent emptyNS) emptyNS
True EmptyFC True fname (nsAsModuleIdent emptyNS) emptyNS
| Nothing => throw (InternalError "Already loaded")
replNS <- getNS
replNestedNS <- getNestedNS
@ -200,14 +200,14 @@ modTime fname
export
readHeader : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
(path : String) -> Core Module
readHeader path
(path : String) -> (origin : ModuleIdent) -> Core Module
readHeader path origin
= do Right res <- coreLift (readFile path)
| Left err => throw (FileErr path err)
-- Stop at the first :, that's definitely not part of the header, to
-- save lexing the whole file unnecessarily
setCurrentElabSource res -- for error printing purposes
let Right (decor, mod) = runParserTo path (isLitFile path) (is ':') res (progHdr path)
let Right (decor, mod) = runParserTo (PhysicalIdrSrc origin) (isLitFile path) (is ':') res (progHdr (PhysicalIdrSrc origin))
| Left err => throw err
pure mod
@ -232,14 +232,14 @@ processMod : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
(srcf : String) -> (ttcf : String) -> (msg : Doc IdrisAnn) ->
(sourcecode : String) ->
(sourcecode : String) -> (origin : ModuleIdent) ->
Core (Maybe (List Error))
processMod srcf ttcf msg sourcecode
processMod srcf ttcf msg sourcecode origin
= catch (do
setCurrentElabSource sourcecode
-- Just read the header to start with (this is to get the imports and
-- see if we can avoid rebuilding if none have changed)
modh <- readHeader srcf
modh <- readHeader srcf origin
-- Add an implicit prelude import
let imps =
if (noprelude !getSession || moduleNS modh == nsAsModuleIdent preludeNS)
@ -270,21 +270,17 @@ processMod srcf ttcf msg sourcecode
else -- needs rebuilding
do iputStrLn msg
Right (decor, mod) <- logTime ("++ Parsing " ++ srcf) $
pure (runParser srcf (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
pure (runParser (PhysicalIdrSrc origin) (isLitFile srcf) sourcecode (do p <- prog (PhysicalIdrSrc origin); eoi; pure p))
| Left err => pure (Just [err])
addSemanticDecorations decor
initHash
traverse_ addPublicHash (sort hs)
resetNextVar
when (ns /= nsAsModuleIdent mainNS) $
do let Just fname = map file (isNonEmptyFC $ headerloc mod)
| Nothing => throw (InternalError "No file name")
d <- getDirs
ns' <- pathToNS (working_dir d) (source_dir d) fname
when (ns /= ns') $
throw (GenericMsg (headerloc mod)
when (ns /= origin) $
throw (GenericMsg mod.headerLoc
("Module name " ++ show ns ++
" does not match file name " ++ fname))
" does not match file name " ++ show srcf))
-- read import ttcs in full here
-- Note: We should only import .ttc - assumption is that there's
@ -322,19 +318,19 @@ process : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
Doc IdrisAnn -> FileName ->
(moduleIdent : ModuleIdent) ->
Core (List Error)
process buildmsg file
process buildmsg file ident
= do Right res <- coreLift (readFile file)
| Left err => pure [FileErr file err]
catch (do ttcf <- getTTCFileName file "ttc"
Just errs <- logTime ("+ Elaborating " ++ file) $
processMod file ttcf buildmsg res
processMod file ttcf buildmsg res ident
| Nothing => pure [] -- skipped it
if isNil errs
then
do defs <- get Ctxt
d <- getDirs
ns <- pathToNS (working_dir d) (source_dir d) file
ns <- ctxtPathToNS file
makeBuildDirectory ns
writeToTTC !(get Syn) ttcf
ttmf <- getTTCFileName file "ttm"

10
src/Idris/REPL.idr
View File

@ -15,15 +15,16 @@ import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Env
import Core.FC
import Core.InitPrimitives
import Core.LinearCheck
import Core.Metadata
import Core.FC
import Core.Normalise
import Core.Options
import Core.Termination
import Core.TT
import Core.Termination
import Core.Unify
import Parser.Unlit
@ -641,7 +642,8 @@ loadMainFile : {auto c : Ref Ctxt Defs} ->
loadMainFile f
= do opts <- get ROpts
put ROpts (record { evalResultName = Nothing } opts)
resetContext f
modIdent <- ctxtPathToNS f
resetContext (PhysicalIdrSrc modIdent)
Right res <- coreLift (readFile f)
| Left err => do setSource ""
pure (ErrorLoadingFile f err)
@ -982,7 +984,7 @@ parseCmd = do c <- command; eoi; pure $ Just c
export
parseRepl : String -> Either Error (Maybe REPLCmd)
parseRepl inp
= case runParser "(interactive)" Nothing inp (parseEmptyCmd <|> parseCmd) of
= case runParser (Virtual Interactive) Nothing inp (parseEmptyCmd <|> parseCmd) of
Left err => Left err
Right (decor, result) => Right result

10
src/Idris/REPL/Common.idr
View File

@ -82,7 +82,7 @@ emitProblem a replDocCreator idemodeDocCreator getFC
Nothing => iputStrLn msg
Just (file, startPos, endPos) =>
send f (SExpList [SymbolAtom "warning",
SExpList [toSExp file,
SExpList [toSExp (show file),
toSExp (addOne startPos),
toSExp (addOne endPos),
toSExp !(renderWithoutColor msg),
@ -150,15 +150,15 @@ resetContext : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
(source : String) ->
(origin : OriginDesc) ->
Core ()
resetContext fname
resetContext origin
= do defs <- get Ctxt
put Ctxt (record { options = clearNames (options defs) } !initDefs)
addPrimitives
put UST initUState
put Syn initSyntax
put MD (initMetadata fname)
put MD (initMetadata origin)
public export
data EditResult : Type where
@ -240,7 +240,7 @@ equivTypes ty1 ty2 =
| False => pure False
_ <- newRef UST initUState
b <- catch
(do res <- unify inTerm replFC [] ty1 ty2
(do res <- unify inTerm EmptyFC [] ty1 ty2
case res of
(MkUnifyResult [] _ [] NoLazy) => pure True
_ => pure False)

2
src/Idris/REPL/FuzzySearch.idr
View File

@ -88,7 +88,7 @@ fuzzySearch expr = do
allDefs <- traverse (resolved ctxt) defs
filterM (\def => fuzzyMatch neg pos def.type) allDefs
put Ctxt defs
doc <- traverse (docsOrSignature replFC) $ fullname <$> filteredDefs
doc <- traverse (docsOrSignature EmptyFC) $ fullname <$> filteredDefs
pure $ Printed $ vsep $ pretty <$> (intersperse "\n" $ join doc)
where

4
src/Idris/REPL/Opts.idr
View File

@ -83,10 +83,6 @@ export
withROpts : {auto o : Ref ROpts REPLOpts} -> Core a -> Core a
withROpts = wrapRef ROpts (\_ => pure ())
export
replFC : FC
replFC = MkFC "(interactive)" (0, 0) (0, 0)
export
setOutput : {auto o : Ref ROpts REPLOpts} ->
OutputMode -> Core ()

4
src/Idris/SetOptions.idr
View File

@ -369,11 +369,11 @@ postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest)
= do ignore $ postOptions res rest
pure False
postOptions res (OutputFile outfile :: rest)
= do ignore $ compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile
= do ignore $ compileExp (PRef EmptyFC (UN "main")) outfile
ignore $ postOptions res rest
pure False
postOptions res (ExecFn str :: rest)
= do ignore $ execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
= do ignore $ execExp (PRef EmptyFC (UN str))
ignore $ postOptions res rest
pure False
postOptions res (CheckOnly :: rest)

4
src/Idris/Syntax.idr
View File

@ -500,7 +500,7 @@ record Import where
public export
record Module where
constructor MkModule
headerloc : FC
headerLoc : FC
moduleNS : ModuleIdent
imports : List Import
documentation : String
@ -835,7 +835,7 @@ initSyntax
initSaveDocStrings
[]
[]
(IVar (MkFC "(default)" (0, 0) (0, 0)) (UN "main"))
(IVar EmptyFC (UN "main"))
where

4
src/Libraries/Data/PosMap.idr
View File

@ -6,8 +6,10 @@
||| [1] https://www.staff.city.ac.uk/~ross/papers/FingerTree.pdf
module Libraries.Data.PosMap
import Data.List
import Core.FC
import Core.Name.Namespace
import Data.List
%default total

10
src/Parser/Package.idr
View File

@ -7,16 +7,18 @@ import public Libraries.Text.Parser
import public Parser.Support
import Core.Core
import Core.FC
import Core.Name.Namespace
import System.File
%default total
export
runParser : (fname : String) -> String -> Rule ty -> Either Error ty
runParser : (fname : String) -> (str : String) -> Rule ty -> Either Error ty
runParser fname str p
= do toks <- mapFst (\err => fromLexError fname (NoRuleApply, err)) $ lex str
parsed <- mapFst (fromParsingError fname) $ parse p toks
= do toks <- mapFst (\err => fromLexError
(PhysicalPkgSrc fname) (NoRuleApply, err)) $ lex str
parsed <- mapFst (fromParsingError (PhysicalPkgSrc fname)) $ parse p toks
Right (fst parsed)
export

23
src/Parser/Source.idr
View File

@ -15,24 +15,27 @@ import System.File
export
runParserTo : {e : _} ->
(fname : String) ->
(origin : OriginDesc) ->
Maybe LiterateStyle -> Lexer ->
String -> Grammar SemanticDecorations Token e ty -> Either Error (SemanticDecorations, ty)
runParserTo fname lit reject str p
= do str <- mapFst (fromLitError fname) $ unlit lit str
toks <- mapFst (fromLexError fname) $ lexTo reject str
(decs, (parsed, _)) <- mapFst (fromParsingError fname) $ parseWith p toks
runParserTo origin lit reject str p
= do str <- mapFst (fromLitError origin) $ unlit lit str
toks <- mapFst (fromLexError origin) $ lexTo reject str
(decs, (parsed, _)) <- mapFst (fromParsingError origin) $ parseWith p toks
Right (decs, parsed)
export
runParser : {e : _} ->
(fname : String) -> Maybe LiterateStyle -> String ->
(origin : OriginDesc) -> Maybe LiterateStyle -> String ->
Grammar SemanticDecorations Token e ty -> Either Error (SemanticDecorations, ty)
runParser fname lit = runParserTo fname lit (pred $ const False)
runParser origin lit = runParserTo origin lit (pred $ const False)
export covering
parseFile : (fname : String) -> Rule ty -> IO (Either Error (SemanticDecorations, ty))
parseFile fname p
parseFile : (fname : String)
-> (origin : OriginDesc)
-> Rule ty
-> IO (Either Error (SemanticDecorations, ty))
parseFile fname origin p
= do Right str <- readFile fname
| Left err => pure (Left (FileErr fname err))
pure (runParser fname (isLitFile fname) str p)
pure (runParser origin (isLitFile fname) str p)

24
src/Parser/Support.idr
View File

@ -18,25 +18,25 @@ import System.File
%default total
export
fromLitError : String -> LiterateError -> Error
fromLitError fname (MkLitErr l c _) = LitFail (MkFC fname (l, c) (l, c + 1))
fromLitError : OriginDesc -> LiterateError -> Error
fromLitError origin (MkLitErr l c _) = LitFail (MkFC origin (l, c) (l, c + 1))
export
fromLexError : String -> (StopReason, Int, Int, String) -> Error
fromLexError fname (ComposeNotClosing begin end, _, _, _)
= LexFail (MkFC fname begin end) "Bracket is not properly closed."
fromLexError fname (_, l, c, _)
= LexFail (MkFC fname (l, c) (l, c + 1)) "Can't recognise token."
fromLexError : OriginDesc -> (StopReason, Int, Int, String) -> Error
fromLexError origin (ComposeNotClosing begin end, _, _, _)
= LexFail (MkFC origin begin end) "Bracket is not properly closed."
fromLexError origin (_, l, c, _)
= LexFail (MkFC origin (l, c) (l, c + 1)) "Can't recognise token."
export
fromParsingError : (Show token, Pretty token) =>
String -> ParsingError token -> Error
fromParsingError fname (Error msg Nothing)
= ParseFail (MkFC fname (0, 0) (0, 0)) (msg +> '.')
fromParsingError fname (Error msg (Just t))
OriginDesc -> ParsingError token -> Error
fromParsingError origin (Error msg Nothing)
= ParseFail (MkFC origin (0, 0) (0, 0)) (msg +> '.')
fromParsingError origin (Error msg (Just t))
= let l = t.startLine
c = t.startCol in
ParseFail (MkFC fname (l, c) (l, c + 1)) (msg +> '.')
ParseFail (MkFC origin (l, c) (l, c + 1)) (msg +> '.')
export
hex : Char -> Maybe Int

2
src/TTImp/Interactive/CaseSplit.idr
View File

@ -330,7 +330,7 @@ mkCase : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Int -> RawImp -> RawImp -> Core ClauseUpdate
mkCase {c} {u} fn orig lhs_raw
= do m <- newRef MD (initMetadata "(interactive)")
= do m <- newRef MD (initMetadata $ Virtual Interactive)
defs <- get Ctxt
ust <- get UST
catch

78
src/TTImp/Parser.idr
View File

@ -15,7 +15,7 @@ import Data.List1
import Data.Maybe
import Data.Strings
topDecl : FileName -> IndentInfo -> Rule ImpDecl
topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
-- All the clauses get parsed as one-clause definitions. Collect any
-- neighbouring clauses with the same function name into one definition.
export
@ -32,7 +32,7 @@ collectDefs : List ImpDecl -> List ImpDecl
%hide Lexer.Core.(<|>)
%hide Prelude.(<|>)
atom : FileName -> Rule RawImp
atom : OriginDesc -> Rule RawImp
atom fname
= do start <- location
x <- constant
@ -145,7 +145,7 @@ bindSymbol
pure AutoImplicit
mutual
appExpr : FileName -> IndentInfo -> Rule RawImp
appExpr : OriginDesc -> IndentInfo -> Rule RawImp
appExpr fname indents
= case_ fname indents
<|> lazy fname indents
@ -166,7 +166,7 @@ mutual
applyExpImp start end f (Right (Nothing, imp) :: args)
= applyExpImp start end (IAutoApp (MkFC fname start end) f imp) args
argExpr : FileName -> IndentInfo ->
argExpr : OriginDesc -> IndentInfo ->
Rule (Either RawImp (Maybe Name, RawImp))
argExpr fname indents
= do continue indents
@ -176,7 +176,7 @@ mutual
arg <- implicitArg fname indents
pure (Right arg)
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, RawImp)
implicitArg : OriginDesc -> IndentInfo -> Rule (Maybe Name, RawImp)
implicitArg fname indents
= do start <- location
symbol "{"
@ -195,7 +195,7 @@ mutual
symbol "}"
pure (Nothing, tm)
as : FileName -> IndentInfo -> Rule RawImp
as : OriginDesc -> IndentInfo -> Rule RawImp
as fname indents
= do start <- location
x <- unqualifiedName
@ -205,7 +205,7 @@ mutual
end <- location
pure (IAs (MkFC fname start end) (MkFC fname start nameEnd) UseRight (UN x) pat)
simpleExpr : FileName -> IndentInfo -> Rule RawImp
simpleExpr : OriginDesc -> IndentInfo -> Rule RawImp
simpleExpr fname indents
= as fname indents
<|> atom fname
@ -235,7 +235,7 @@ mutual
pibindAll fc p ((rig, n, ty) :: rest) scope
= IPi fc rig p n ty (pibindAll fc p rest scope)
bindList : FileName -> FilePos -> IndentInfo ->
bindList : OriginDesc -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, RawImp))
bindList fname start indents
= forget <$> sepBy1 (symbol ",")
@ -250,7 +250,7 @@ mutual
pure (rig, UN n, ty))
pibindListName : FileName -> FilePos -> IndentInfo ->
pibindListName : OriginDesc -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, RawImp))
pibindListName fname start indents
= do rigc <- multiplicity
@ -268,14 +268,14 @@ mutual
rig <- getMult rigc
pure (rig, n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
pibindList : OriginDesc -> FilePos -> IndentInfo ->
Rule (List (RigCount, Maybe Name, RawImp))
pibindList fname start indents
= do params <- pibindListName fname start indents
pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
autoImplicitPi : FileName -> IndentInfo -> Rule RawImp
autoImplicitPi : OriginDesc -> IndentInfo -> Rule RawImp
autoImplicitPi fname indents
= do start <- location
symbol "{"
@ -288,7 +288,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
forall_ : FileName -> IndentInfo -> Rule RawImp
forall_ : OriginDesc -> IndentInfo -> Rule RawImp
forall_ fname indents
= do start <- location
keyword "forall"
@ -303,7 +303,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> Rule RawImp
implicitPi : OriginDesc -> IndentInfo -> Rule RawImp
implicitPi fname indents
= do start <- location
symbol "{"
@ -314,7 +314,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
explicitPi : FileName -> IndentInfo -> Rule RawImp
explicitPi : OriginDesc -> IndentInfo -> Rule RawImp
explicitPi fname indents
= do start <- location
symbol "("
@ -325,7 +325,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) exp binders scope)
lam : FileName -> IndentInfo -> Rule RawImp
lam : OriginDesc -> IndentInfo -> Rule RawImp
lam fname indents
= do start <- location
symbol "\\"
@ -341,7 +341,7 @@ mutual
bindAll fc ((rig, n, ty) :: rest) scope
= ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)
let_ : FileName -> IndentInfo -> Rule RawImp
let_ : OriginDesc -> IndentInfo -> Rule RawImp
let_ fname indents
= do start <- location
keyword "let"
@ -366,7 +366,7 @@ mutual
end <- location
pure (ILocal (MkFC fname start end) (collectDefs ds) scope)
case_ : FileName -> IndentInfo -> Rule RawImp
case_ : OriginDesc -> IndentInfo -> Rule RawImp
case_ fname indents
= do start <- location
keyword "case"
@ -377,13 +377,13 @@ mutual
pure (let fc = MkFC fname start end in
ICase fc scr (Implicit fc False) alts)
caseAlt : FileName -> IndentInfo -> Rule ImpClause
caseAlt : OriginDesc -> IndentInfo -> Rule ImpClause
caseAlt fname indents
= do start <- location
lhs <- appExpr fname indents
caseRHS fname indents start lhs
caseRHS : FileName -> IndentInfo -> (Int, Int) -> RawImp ->
caseRHS : OriginDesc -> IndentInfo -> (Int, Int) -> RawImp ->
Rule ImpClause
caseRHS fname indents start lhs
= do symbol "=>"
@ -397,7 +397,7 @@ mutual
end <- location
pure (ImpossibleClause (MkFC fname start end) lhs)
record_ : FileName -> IndentInfo -> Rule RawImp
record_ : OriginDesc -> IndentInfo -> Rule RawImp
record_ fname indents
= do start <- location
keyword "record"
@ -409,7 +409,7 @@ mutual
end <- location
pure (IUpdate (MkFC fname start end) (forget fs) sc)
field : FileName -> IndentInfo -> Rule IFieldUpdate
field : OriginDesc -> IndentInfo -> Rule IFieldUpdate
field fname indents
= do path <- sepBy1 (symbol "->") unqualifiedName
upd <- (do symbol "="; pure ISetField)
@ -418,7 +418,7 @@ mutual
val <- appExpr fname indents
pure (upd (forget path) val)
rewrite_ : FileName -> IndentInfo -> Rule RawImp
rewrite_ : OriginDesc -> IndentInfo -> Rule RawImp
rewrite_ fname indents
= do start <- location
keyword "rewrite"
@ -428,7 +428,7 @@ mutual
end <- location
pure (IRewrite (MkFC fname start end) rule tm)
lazy : FileName -> IndentInfo -> Rule RawImp
lazy : OriginDesc -> IndentInfo -> Rule RawImp
lazy fname indents
= do start <- location
exactIdent "Lazy"
@ -452,7 +452,7 @@ mutual
pure (IForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> Rule RawImp
binder : OriginDesc -> IndentInfo -> Rule RawImp
binder fname indents
= autoImplicitPi fname indents
<|> forall_ fname indents
@ -461,7 +461,7 @@ mutual
<|> lam fname indents
<|> let_ fname indents
typeExpr : FileName -> IndentInfo -> Rule RawImp
typeExpr : OriginDesc -> IndentInfo -> Rule RawImp
typeExpr fname indents
= do start <- location
arg <- appExpr fname indents
@ -480,10 +480,10 @@ mutual
(mkPi start end a as)
export
expr : FileName -> IndentInfo -> Rule RawImp
expr : OriginDesc -> IndentInfo -> Rule RawImp
expr = typeExpr
tyDecl : FileName -> IndentInfo -> Rule ImpTy
tyDecl : OriginDesc -> IndentInfo -> Rule ImpTy
tyDecl fname indents
= do start <- location
n <- name
@ -496,7 +496,7 @@ tyDecl fname indents
mutual
parseRHS : (withArgs : Nat) ->
FileName -> IndentInfo -> (Int, Int) -> RawImp ->
OriginDesc -> IndentInfo -> (Int, Int) -> RawImp ->
Rule (Name, ImpClause)
parseRHS withArgs fname indents start lhs
= do symbol "="
@ -530,7 +530,7 @@ mutual
getFn (INamedApp _ f _ a) = getFn f
getFn _ = fail "Not a function application"
clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause)
clause : Nat -> OriginDesc -> IndentInfo -> Rule (Name, ImpClause)
clause withArgs fname indents
= do start <- location
lhs <- expr fname indents
@ -551,7 +551,7 @@ mutual
end <- location
pure (MkFC fname start end, tm)
definition : FileName -> IndentInfo -> Rule ImpDecl
definition : OriginDesc -> IndentInfo -> Rule ImpDecl
definition fname indents
= do start <- location
nd <- clause 0 fname indents
@ -568,7 +568,7 @@ dataOpt
ns <- forget <$> some name
pure (SearchBy ns)
dataDecl : FileName -> IndentInfo -> Rule ImpData
dataDecl : OriginDesc -> IndentInfo -> Rule ImpData
dataDecl fname indents
= do start <- location
keyword "data"
@ -584,7 +584,7 @@ dataDecl fname indents
end <- location
pure (MkImpData (MkFC fname start end) n ty opts cs)
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam fname indents
= do symbol "("
start <- location
@ -609,7 +609,7 @@ recordParam fname indents
end <- location
pure [(n, top, Explicit, Implicit (MkFC fname start end) False)]
fieldDecl : FileName -> IndentInfo -> Rule (List IField)
fieldDecl : OriginDesc -> IndentInfo -> Rule (List IField)
fieldDecl fname indents
= do symbol "{"
commit
@ -631,7 +631,7 @@ fieldDecl fname indents
pure (map (\n => MkIField (MkFC fname start end)
linear p (UN n) ty) (forget ns))
recordDecl : FileName -> IndentInfo -> Rule ImpDecl
recordDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
recordDecl fname indents
= do start <- location
vis <- visibility
@ -663,7 +663,7 @@ logLevel
lvl <- intLit
pure (Just (topic, fromInteger lvl))
directive : FileName -> IndentInfo -> Rule ImpDecl
directive : OriginDesc -> IndentInfo -> Rule ImpDecl
directive fname indents
= do pragma "logging"
commit
@ -698,7 +698,7 @@ directive fname indents
IPragma (\c, nest, env => setRewrite {c} fc eq rw))
-}
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> Rule ImpDecl
-- topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
topDecl fname indents
= do start <- location
vis <- visibility
@ -748,7 +748,7 @@ collectDefs (d :: ds)
-- full programs
export
prog : FileName -> Rule (List ImpDecl)
prog : OriginDesc -> Rule (List ImpDecl)
prog fname
= do ds <- nonEmptyBlock (topDecl fname)
pure (collectDefs $ forget ds)
@ -758,7 +758,7 @@ export
command : Rule ImpREPL
command
= do symbol ":"; exactIdent "t"
tm <- expr "(repl)" init
tm <- expr (Virtual Interactive) init
pure (Check tm)
<|> do symbol ":"; exactIdent "s"
n <- name
@ -781,5 +781,5 @@ command
pure (DebugInfo n)
<|> do symbol ":"; exactIdent "q"
pure Quit
<|> do tm <- expr "(repl)" init
<|> do tm <- expr (Virtual Interactive) init
pure (Eval tm)

8
src/TTImp/ProcessDecls.idr
View File

@ -3,8 +3,10 @@ module TTImp.ProcessDecls
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Options
import Core.Termination
import Core.UnifyState
@ -167,8 +169,10 @@ processTTImpFile : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
String -> Core Bool
processTTImpFile fname
= do Right (decor, tti) <- logTime "Parsing" $ coreLift $ parseFile fname
(do decls <- prog fname
= do modIdent <- ctxtPathToNS fname
Right (decor, tti) <- logTime "Parsing" $
coreLift $ parseFile fname (PhysicalIdrSrc modIdent)
(do decls <- prog (PhysicalIdrSrc modIdent)
eoi
pure decls)
| Left err => do coreLift (putStrLn (show err))

9
src/Yaffle/Main.idr
View File

@ -47,10 +47,10 @@ yaffleMain : String -> List String -> Core ()
yaffleMain fname args
= do defs <- initDefs
c <- newRef Ctxt defs
m <- newRef MD (initMetadata fname)
u <- newRef UST initUState
d <- getDirs
t <- processArgs args
modIdent <- ctxtPathToNS fname
m <- newRef MD (initMetadata (PhysicalIdrSrc modIdent))
u <- newRef UST initUState
setLogTimings t
addPrimitives
case extension fname of
@ -60,8 +60,7 @@ yaffleMain fname args
_ => do coreLift_ $ putStrLn "Processing as TTImp"
ok <- processTTImpFile fname
when ok $
do ns <- pathToNS (working_dir d) (source_dir d) fname
makeBuildDirectory ns
do makeBuildDirectory modIdent
writeToTTC () !(getTTCFileName fname "ttc")
coreLift_ $ putStrLn "Written TTC"
ust <- get UST

14
src/Yaffle/REPL.idr
View File

@ -65,9 +65,9 @@ process (Check ttimp)
process (ProofSearch n_in)
= do defs <- get Ctxt
[(n, i, ty)] <- lookupTyName n_in (gamma defs)
| [] => undefinedName toplevelFC n_in
| ns => throw (AmbiguousName toplevelFC (map fst ns))
def <- search toplevelFC top False 1000 n ty []
| [] => undefinedName (justFC defaultFC) n_in
| ns => throw (AmbiguousName (justFC defaultFC) (map fst ns))
def <- search (justFC defaultFC) top False 1000 n ty []
defs <- get Ctxt
defnf <- normaliseHoles defs [] def
coreLift_ (printLn !(toFullNames defnf))
@ -75,9 +75,9 @@ process (ProofSearch n_in)
process (ExprSearch n_in)
= do defs <- get Ctxt
[(n, i, ty)] <- lookupTyName n_in (gamma defs)
| [] => undefinedName toplevelFC n_in
| ns => throw (AmbiguousName toplevelFC (map fst ns))
results <- exprSearchN toplevelFC 1 n []
| [] => undefinedName (justFC defaultFC) n_in
| ns => throw (AmbiguousName (justFC defaultFC) (map fst ns))
results <- exprSearchN (justFC defaultFC) 1 n []
traverse_ (\d => coreLift (printLn d)) results
pure True
process (GenerateDef line name)
@ -150,7 +150,7 @@ repl : {auto c : Ref Ctxt Defs} ->
repl
= do coreLift_ (putStr "Yaffle> ")
inp <- coreLift getLine
case runParser "(interactive)" Nothing inp command of
case runParser (Virtual Interactive) Nothing inp command of
Left err => do coreLift_ (printLn err)
repl
Right (decor, cmd) => when !(processCatch cmd) repl

4
tests/chez/chez006/expected
View File

@ -16,7 +16,7 @@ Main> Bye for now!
1/1: Building TypeCase2 (TypeCase2.idr)
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).
TypeCase2.idr:5:14--5:17
TypeCase2:5:14--5:17
1 | data Bar = MkBar
2 | data Baz = MkBaz
3 |
@ -26,7 +26,7 @@ TypeCase2.idr:5:14--5:17
Error: While processing left hand side of foo. Can't match on Nat (Erased argument).
TypeCase2.idr:9:5--9:8
TypeCase2:9:5--9:8
5 | strangeId {a=Nat} x = x+1
6 | strangeId x = x
7 |

6
tests/chez/chez019/expected
View File

@ -1,6 +1,6 @@
1/1: Building partial (partial.idr)
Main> ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17
Main> ERROR: Unhandled input for Main.foo at partial:4:1--4:17
Main> 2
Main> ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
Main> ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
Main> ERROR: Unhandled input for Main.lookup' at partial:19:1--19:40
Main> ERROR: Unhandled input for Main.lookup' at partial:19:1--19:40
Main> Bye for now!

8
tests/chez/chez031/expected
View File

@ -2,7 +2,7 @@ Error: The given specifier was not accepted by any backend. Available backends:
chez, chez-sep, racket, node, javascript, refc, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:29:1--30:35
Specifiers:29:1--30:35
29 | %foreign "scheme,racket:+"
30 | plusRacketFail : Int -> Int -> Int
@ -10,7 +10,7 @@ Error: The given specifier was not accepted by any backend. Available backends:
chez, chez-sep, racket, node, javascript, refc, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:29:1--30:35
Specifiers:29:1--30:35
29 | %foreign "scheme,racket:+"
30 | plusRacketFail : Int -> Int -> Int
@ -19,13 +19,13 @@ Specifiers> Error: The given specifier was not accepted by any backend. Availabl
chez, chez-sep, racket, node, javascript, refc, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:29:1--30:35
Specifiers:29:1--30:35
Specifiers> [exec] Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
chez, chez-sep, racket, node, javascript, refc, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:29:1--30:35
Specifiers:29:1--30:35
[exec] Specifiers>
Bye for now!

2
tests/idris2/basic001/expected
View File

@ -3,7 +3,7 @@ Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
Main> Error: When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat.
Mismatch between: S Z and Z.
(interactive):1:28--1:51
(Interactive):1:28--1:51
1 | zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
^^^^^^^^^^^^^^^^^^^^^^^

2
tests/idris2/basic003/expected
View File

@ -5,7 +5,7 @@ Error: While processing right hand side of keepUnique. Ambiguous elaboration. Po
Main.Set.toList ?arg
Main.Vect.toList ?arg
Ambig2.idr:26:21--26:27
Ambig2:26:21--26:27
22 | export
23 | fromList : List a -> Set a
24 |

2
tests/idris2/basic005/expected
View File

@ -1,7 +1,7 @@
1/1: Building NoInfer (NoInfer.idr)
Error: Unsolved holes:
Main.{_:1} introduced at:
NoInfer.idr:1:7--1:8
NoInfer:1:7--1:8
1 | foo : ? -> Int
^

4
tests/idris2/basic011/expected
View File

@ -2,7 +2,7 @@
1/1: Building Dots2 (Dots2.idr)
Error: While processing left hand side of foo. Can't match on ?x [no locals in scope] (Non linear pattern variable).
Dots2.idr:2:7--2:8
Dots2:2:7--2:8
1 | foo : Int -> Int -> Int
2 | foo x x = x + x
^
@ -10,7 +10,7 @@ Dots2.idr:2:7--2:8
1/1: Building Dots3 (Dots3.idr)
Error: While processing left hand side of addBaz. Pattern variable z unifies with: ?y [no locals in scope].
Dots3.idr:5:13--5:30
Dots3:5:13--5:30
|
5 | addBaz (x + y) (AddThings x z) = x + y
| ^ ^

4
tests/idris2/basic014/expected
View File

@ -1,7 +1,7 @@
1/1: Building Rewrite (Rewrite.idr)
Error: While processing right hand side of wrongCommutes. Rewriting by m + k = k + m did not change type S k + m = m + S k.
Rewrite.idr:15:25--15:57
Rewrite:15:25--15:57
11 | plusCommutes (S k) m = rewrite plusCommutes k m in sym (plusnSm m k)
12 |
13 | wrongCommutes : (n, m : Nat) -> n + m = m + n
@ -11,7 +11,7 @@ Rewrite.idr:15:25--15:57
Error: While processing right hand side of wrongCommutes2. Nat is not a rewrite rule type.
Rewrite.idr:19:26--19:43
Rewrite:19:26--19:43
15 | wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar
16 |
17 | wrongCommutes2 : (n, m : Nat) -> n + m = m + n

6
tests/idris2/basic016/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of etaBad. When unifying \x, y => MkTest x y = \x, y => MkTest x y and MkTest = \x, y => MkTest x y.
Mismatch between: Nat and Integer.
Eta.idr:14:10--14:14
Eta:14:10--14:14
10 | etaGood3: (f : a -> b) -> f = (\x => f x)
11 | etaGood3 f = Refl
12 |
@ -14,7 +14,7 @@ Eta.idr:14:10--14:14
Error: While processing right hand side of test. When unifying \x => S x = \x => S x and S = \x => S x.
Mismatch between: a and Nat.
Eta2.idr:2:8--2:12
Eta2:2:8--2:12
1 | test : Builtin.Equal S (\x : a => S ?)
2 | test = Refl
^^^^
@ -22,7 +22,7 @@ Eta2.idr:2:8--2:12
Error: While processing right hand side of test2. When unifying \x => S x = \x => S x and S = \x => S x.
Mismatch between: a and Nat.
Eta2.idr:5:44--5:48
Eta2:5:44--5:48
1 | test : Builtin.Equal S (\x : a => S ?)
2 | test = Refl
3 |

2
tests/idris2/basic018/expected
View File

@ -1,7 +1,7 @@
1/1: Building Fin (Fin.idr)
Error: While processing right hand side of bar. Can't find an implementation for IsJust (integerToFin 8 5).
Fin.idr:34:7--34:8
Fin:34:7--34:8
30 | foo : Fin 5
31 | foo = 3
32 |

4
tests/idris2/basic022/expected
View File

@ -1,7 +1,7 @@
1/1: Building Erase (Erase.idr)
Error: While processing left hand side of bad. Can't match on False (Erased argument).
Erase.idr:5:5--5:10
Erase:5:5--5:10
1 | myReplace : forall p . (0 rule : x = y) -> (1 val : p y) -> p x
2 | myReplace Refl prf = prf
3 |
@ -11,7 +11,7 @@ Erase.idr:5:5--5:10
Error: While processing left hand side of minusBad. Can't match on LeZ (Erased argument).
Erase.idr:19:18--19:21
Erase:19:18--19:21
15 | minus (S k) (S j) (LeS p) = minus k j p
16 |
17 | -- y is used in the run time case tree, so erasure not okay

4
tests/idris2/basic025/expected
View File

@ -8,13 +8,13 @@ Main> [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
Main> [100, 99, 98, 97, 96, 95, 94, 93, 92, 91]
Main> Invalid list range syntax.
(interactive):1:12--1:13
(Interactive):1:12--1:13
1 | [1,3,5..10]
^
Main> Invalid list range syntax.
(interactive):1:7--1:8
(Interactive):1:7--1:8
1 | [..10]
^

2
tests/idris2/basic030/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of foo. When unifying Nat -> MyN and MyN.
Mismatch between: Nat -> MyN and MyN.
arity.idr:4:16--4:21
arity:4:16--4:21
1 | data MyN = MkN Nat Nat
2 |
3 | foo : Nat -> Nat -> Nat

2
tests/idris2/basic031/expected
View File

@ -1,7 +1,7 @@
1/1: Building erased (erased.idr)
Error: While processing left hand side of nameOf. Can't match on Bool (Erased argument).
erased.idr:7:17--7:21
erased:7:17--7:21
3 | MyJust : a -> MyMaybe a
4 |
5 | -- Should fail since type argument is deleted

4
tests/idris2/basic033/expected
View File

@ -1,7 +1,7 @@
1/1: Building unboundimps (unboundimps.idr)
Error: While processing type of len'. Undefined name xs.
unboundimps.idr:18:11--18:13
unboundimps:18:11--18:13
14 | -- xs and its indices
15 | len : forall xs . Env xs -> Nat
16 |
@ -11,7 +11,7 @@ unboundimps.idr:18:11--18:13
Error: While processing type of append'. Undefined name n.
unboundimps.idr:19:16--19:17
unboundimps:19:16--19:17
15 | len : forall xs . Env xs -> Nat
16 |
17 | -- neither of these are fine

2
tests/idris2/basic034/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of dolet2. When unifying Maybe Int and Maybe String.
Mismatch between: Int and String.
lets.idr:22:39--22:40
lets:22:39--22:40
18 | pure (x' + y')
19 |
20 | dolet2 : Maybe Int -> Maybe Int -> Maybe Int

2
tests/idris2/basic041/expected
View File

@ -1,7 +1,7 @@
1/1: Building QDo (QDo.idr)
Error: While processing right hand side of test. Undefined name B.A.>>.
QDo.idr:27:10--27:11
QDo:27:10--27:11
23 | a >> f = a >>= const f
24 |
25 | test : Nat

4
tests/idris2/basic042/expected
View File

@ -5,7 +5,7 @@ Main> True
Main> False
Main> Error: Can't find an implementation for IsJust Nothing.
(interactive):1:10--1:14
(Interactive):1:10--1:14
1 | the Bool "42"
^^^^
@ -17,7 +17,7 @@ Main> Omega
Main> FS (FS FZ)
Main> Error: Can't find an implementation for IsJust (integerToFin 6 3).
(interactive):1:13--1:14
(Interactive):1:13--1:14
1 | the (Fin 3) 6
^

54
tests/idris2/basic044/expected
View File

@ -21,11 +21,11 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Chk
@ -33,14 +33,14 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:n:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:n:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Syn
@ -48,16 +48,16 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term.idr:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
@ -98,60 +98,60 @@ Term> Bye for now!
LOG declare.type:1: Processing Vec.Vec
LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1])
LOG declare.type:1: Processing Vec.Nil
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data/Fin.idr:L:C--L:C)
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data.Fin:L:C--L:C)
LOG declare.type:1: Processing Vec.::
LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
{ Data.Fin.FZ {e:N} => [0] {arg:N}[3]
| Data.Fin.FS {e:N} {e:N} => [1] ({arg:N}[5] {e:N}[1])
}
LOG declare.type:1: Processing Vec.test
LOG elab.ambiguous:5: Ambiguous elaboration at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 2)
($resolvedN 2)
With default. Target type : Prelude.Types.Nat
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
Target type : ({arg:N} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Basics.List Prelude.Types.Nat))
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
Target type : ({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
With default. Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : ({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
With default. Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : ({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
Target type : (Prelude.Basics.List Prelude.Types.Nat)
LOG elab.ambiguous:5: Ambiguous elaboration at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
With default. Target type : Prelude.Types.Nat
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec.idr:L:C--L:C:
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:L:C--L:C:
$resolvedN
Target type : (Prelude.Basics.List Prelude.Types.Nat)
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))

2
tests/idris2/basic049/expected
View File

@ -44,7 +44,7 @@ Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous ela
Main.R2.MkR
Main.R1.MkR Type
Fld.idr:72:26--72:29
Fld:72:26--72:29
68 | r1 : R1 -- explicit fields access
69 | r1 = MkR {field = "string"}
70 |

2
tests/idris2/builtin002/expected
View File

@ -1,7 +1,7 @@
1/1: Building Test (Test.idr)
Error: Constructor Main.S doesn't match any pattern for Natural.
Test.idr:6:1--6:23
Test:6:1--6:23
2 | data MyNat
3 | = S MyNat MyNat
4 | | Z

2
tests/idris2/builtin004/expected
View File

@ -1,7 +1,7 @@
1/1: Building Test (Test.idr)
Error: Natural builtin does not support lazy types.
Test.idr:6:1--6:23
Test:6:1--6:23
2 | data MyNat
3 | = S (Inf MyNat)
4 | | Z

2
tests/idris2/builtin006/expected
View File

@ -1,7 +1,7 @@
1/1: Building Test (Test.idr)
Error: Non-erased argument is not a 'Nat'-like type.
Test.idr:9:1--9:35
Test:9:1--9:35
5 | natToInt : MyNat -> Integer
6 | natToInt Z = 0
7 | natToInt (S k) = 1 + natToInt k

2
tests/idris2/builtin008/expected
View File

@ -1,7 +1,7 @@
1/1: Building Test (Test.idr)
Error: More than 1 non-erased arguments found for Main.finToInteger.
Test.idr:11:1--11:39
Test:11:1--11:39
07 | finToInteger : {k : _} -> Fin k -> Integer
08 | finToInteger FZ = 0
09 | finToInteger (FS k) = 1 + finToInteger k

4
tests/idris2/builtin010/expected
View File

@ -1,7 +1,7 @@
1/1: Building Test (Test.idr)
Error: No unrestricted arguments of type `Integer` found for Main.natToMyNat.
Test.idr:20:1--20:37
Test:20:1--20:37
16 | natToMyNat : Nat -> MyNat
17 | natToMyNat Z = Z
18 | natToMyNat (S k) = S $ natToMyNat k
@ -11,7 +11,7 @@ Test.idr:20:1--20:37
Error: Return type is not a 'Nat'-like type
Test.idr:25:1--25:42
Test:25:1--25:42
21 |
22 | integerToNotNat : Integer -> Maybe String
23 | integerToNotNat x = Just "Boo"

2
tests/idris2/casetree001/expected
View File

@ -2,7 +2,7 @@
1/1: Building IsS (IsS.idr)
Error: While processing left hand side of fail. Can't match on S (Under-applied constructor).
IsS.idr:31:14--31:15
IsS:31:14--31:15
27 | -- ^ forced by Refl
28 |
29 | -- If you don't: too bad!

2
tests/idris2/coverage003/expected
View File

@ -1,7 +1,7 @@
1/1: Building Cover (Cover.idr)
Error: While processing left hand side of badBar. Can't match on 0 as it has a polymorphic type.
Cover.idr:16:1--16:7
Cover:16:1--16:7
12 | cty Nat (S _) = S Z
13 | cty _ x = S (S Z)
14 |

2
tests/idris2/coverage004/expected
View File

@ -1,7 +1,7 @@
1/1: Building Cover (Cover.idr)
Error: While processing left hand side of bad. Can't match on Just (fromInteger 0) as it has a polymorphic type.
Cover.idr:14:1--14:4
Cover:14:1--14:4
10 |
11 | bad : a -> Foo a -> Bool
12 | bad Z IsNat = False

4
tests/idris2/coverage007/expected
View File

@ -1,7 +1,7 @@
1/1: Building eq (eq.idr)
Error: badeq x y p is not a valid impossible case.
eq.idr:27:1--27:23
eq:27:1--27:23
23 | eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat
24 | eqL2 xs p impossible
25 |
@ -11,7 +11,7 @@ eq.idr:27:1--27:23
Error: badeqL xs ys p is not a valid impossible case.
eq.idr:30:1--30:26
eq:30:1--30:26
26 | badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
27 | badeq x y p impossible
28 |

4
tests/idris2/coverage009/expected
View File

@ -1,7 +1,7 @@
1/1: Building unreachable (unreachable.idr)
Warning: Unreachable clause: foo Nothing True
unreachable.idr:3:1--3:17
unreachable:3:1--3:17
1 | foo : Maybe Int -> Bool -> Int
2 | foo Nothing _ = 42
3 | foo Nothing True = 94
@ -9,7 +9,7 @@ unreachable.idr:3:1--3:17
Warning: Unreachable clause: foo Nothing False
unreachable.idr:5:1--5:18
unreachable:5:1--5:18
1 | foo : Maybe Int -> Bool -> Int
2 | foo Nothing _ = 42
3 | foo Nothing True = 94

2
tests/idris2/coverage010/expected
View File

@ -1,7 +1,7 @@
1/1: Building casetot (casetot.idr)
Error: main is not covering.
casetot.idr:12:1--12:13
casetot:12:1--12:13
08 |
09 | ints : Vect 4 Int
10 | ints = [1, 2, 3, 4]

4
tests/idris2/coverage012/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue899 (Issue899.idr)
Error: zeroImpossible is not covering.
Issue899.idr:3:1--3:46
Issue899:3:1--3:46
1 | %default total
2 |
3 | zeroImpossible : (k : Nat) -> k === Z -> Void
@ -13,7 +13,7 @@ Missing cases:
1/1: Building Issue484 (Issue484.idr)
Error: swap is not covering.
Issue484.idr:10:1--10:41
Issue484:10:1--10:41
06 | getType Vrai = Unit
07 | getType Faux = Unit
08 | getType Indef = Void

16
tests/idris2/coverage013/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue1022 (Issue1022.idr)
Error: test8 eq is not a valid impossible case.
Issue1022.idr:25:1--25:20
Issue1022:25:1--25:20
21 |
22 | -- The following ones are actually possible
23 |
@ -11,7 +11,7 @@ Issue1022.idr:25:1--25:20
Error: test9 eq is not a valid impossible case.
Issue1022.idr:28:1--28:20
Issue1022:28:1--28:20
24 | test8 : Not (a = Type)
25 | test8 eq impossible
26 |
@ -21,7 +21,7 @@ Issue1022.idr:28:1--28:20
Error: test10 eq is not a valid impossible case.
Issue1022.idr:31:1--31:21
Issue1022:31:1--31:21
27 | test9 : Not (a = 'a')
28 | test9 eq impossible
29 |
@ -31,7 +31,7 @@ Issue1022.idr:31:1--31:21
Error: test11 eq is not a valid impossible case.
Issue1022.idr:34:1--34:21
Issue1022:34:1--34:21
30 | test10 : Not (a = Nat)
31 | test10 eq impossible
32 |
@ -42,7 +42,7 @@ Issue1022.idr:34:1--34:21
1/1: Building Issue1022-Refl (Issue1022-Refl.idr)
Error: test8 Refl is not a valid impossible case.
Issue1022-Refl.idr:25:1--25:22
Issue1022-Refl:25:1--25:22
21 |
22 | -- The following ones are actually possible
23 |
@ -52,7 +52,7 @@ Issue1022-Refl.idr:25:1--25:22
Error: test9 Refl is not a valid impossible case.
Issue1022-Refl.idr:28:1--28:22
Issue1022-Refl:28:1--28:22
24 | test8 : Not (a = Type)
25 | test8 Refl impossible
26 |
@ -62,7 +62,7 @@ Issue1022-Refl.idr:28:1--28:22
Error: test10 Refl is not a valid impossible case.
Issue1022-Refl.idr:31:1--31:23
Issue1022-Refl:31:1--31:23
27 | test9 : Not (a = 'a')
28 | test9 Refl impossible
29 |
@ -72,7 +72,7 @@ Issue1022-Refl.idr:31:1--31:23
Error: test11 Refl is not a valid impossible case.
Issue1022-Refl.idr:34:1--34:23
Issue1022-Refl:34:1--34:23
30 | test10 : Not (a = Nat)
31 | test10 Refl impossible
32 |

4
tests/idris2/coverage014/expected
View File

@ -2,7 +2,7 @@
Error: Impossible pattern gives an error:
Can't solve constraint between: ?_ ++ [?_] and ?x :: ?xs.
Issue794.idr:15:7--15:17
Issue794:15:7--15:17
11 | empty Empty impossible
12 |
13 |
@ -12,7 +12,7 @@ Issue794.idr:15:7--15:17
Error: empty is not covering.
Issue794.idr:10:1--10:32
Issue794:10:1--10:32
06 | Empty : SnocList []
07 | Snoc : (x : a) -> (xs : List a) ->
08 | (rec : SnocList xs) -> SnocList (xs ++ [x])

8
tests/idris2/coverage015/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue1169 (Issue1169.idr)
Error: test is not covering.
Issue1169.idr:3:1--3:26
Issue1169:3:1--3:26
1 | %default total
2 |
3 | test : (String, ()) -> ()
@ -12,7 +12,7 @@ Missing cases:
Error: test' is not covering.
Issue1169.idr:6:1--6:24
Issue1169:6:1--6:24
2 |
3 | test : (String, ()) -> ()
4 | test ("a", ()) = ()
@ -25,7 +25,7 @@ Missing cases:
Error: test'' is not covering.
Issue1169.idr:9:1--9:22
Issue1169:9:1--9:22
5 |
6 | test' : (Int, ()) -> ()
7 | test' (1, ()) = ()
@ -48,7 +48,7 @@ You may be unintentionally shadowing the associated global definitions:
f is shadowing Main.f
Error: decode is not covering.
Issue1366.idr:33:1--33:45
Issue1366:33:1--33:45
29 | data Funny : (a : Type) -> (f : Type -> Type) -> Type where
30 | A : List a -> f a -> Funny a f
31 | B : Funny a f

2
tests/idris2/coverage016/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue633 (Issue633.idr)
Error: While processing left hand side of test. Can't match on \x => True (Not a constructor application or primitive).
Issue633.idr:4:1--4:18
Issue633:4:1--4:18
1 | %default total
2 |
3 | test : (f : () -> Bool) -> f () = True

2
tests/idris2/error001/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of wrong. When unifying a and Vect ?k ?a.
Mismatch between: a and Vect ?k ?a.
Error.idr:6:19--6:20
Error:6:19--6:20
2 | Nil : Vect Z a
3 | (::) : a -> Vect k a -> Vect (S k) a
4 |

2
tests/idris2/error002/expected
View File

@ -1,7 +1,7 @@
1/1: Building Error (Error.idr)
Error: While processing right hand side of wrong. Undefined name ys.
Error.idr:6:17--6:19
Error:6:17--6:19
2 | Nil : Vect Z a
3 | (::) : a -> Vect k a -> Vect (S k) a
4 |

6
tests/idris2/error003/expected
View File

@ -3,7 +3,7 @@ Error: While processing right hand side of wrong. Sorry, I can't find any elabor
If Main.length: When unifying Nat and Vect ?n ?a.
Mismatch between: Nat and Vect ?n ?a.
Error.idr:12:18--12:19
Error:12:18--12:19
08 | length [] = Z
09 | length (x :: xs) = S (length xs)
10 |
@ -14,7 +14,7 @@ Error.idr:12:18--12:19
If Prelude.List.length: When unifying Nat and List ?a.
Mismatch between: Nat and List ?a.
Error.idr:12:18--12:19
Error:12:18--12:19
08 | length [] = Z
09 | length (x :: xs) = S (length xs)
10 |
@ -25,7 +25,7 @@ Error.idr:12:18--12:19
If Prelude.String.length: When unifying Nat and String.
Mismatch between: Nat and String.
Error.idr:12:18--12:19
Error:12:18--12:19
08 | length [] = Z
09 | length (x :: xs) = S (length xs)
10 |

14
tests/idris2/error004/expected
View File

@ -1,7 +1,7 @@
1/1: Building Error1 (Error1.idr)
Error: While processing right hand side of wrong. Can't find an implementation for Show (Vect 4 Integer).
Error1.idr:8:9--8:40
Error1:8:9--8:40
4 | Nil : Vect Z a
5 | (::) : a -> Vect k a -> Vect (S k) a
6 |
@ -13,7 +13,7 @@ Error1.idr:8:9--8:40
Error: While processing right hand side of show. Multiple solutions found in search of:
Show (Vect k Integer)
Error2.idr:13:38--13:45
Error2:13:38--13:45
09 | show (x :: xs) = show x ++ ", " ++ show xs
10 |
11 | Show (Vect n Integer) where
@ -22,12 +22,12 @@ Error2.idr:13:38--13:45
^^^^^^^
Possible correct results:
Show implementation at Error2.idr:11:1--13:45
Show implementation at Error2.idr:7:1--9:45
Show implementation at Error2:11:1--13:45
Show implementation at Error2:7:1--9:45
Error: While processing right hand side of wrong. Multiple solutions found in search of:
Show (Vect 1 Integer)
Error2.idr:16:9--16:34
Error2:16:9--16:34
12 | show [] = "END"
13 | show (x :: xs) = show x ++ ", " ++ show xs
14 |
@ -36,5 +36,5 @@ Error2.idr:16:9--16:34
^^^^^^^^^^^^^^^^^^^^^^^^^
Possible correct results:
Show implementation at Error2.idr:11:1--13:45
Show implementation at Error2.idr:7:1--9:45
Show implementation at Error2:11:1--13:45
Show implementation at Error2:7:1--9:45

4
tests/idris2/error005/expected
View File

@ -1,7 +1,7 @@
1/1: Building IfErr (IfErr.idr)
Error: While processing right hand side of foo. Can't find an implementation for Eq a.
IfErr.idr:4:11--4:17
IfErr:4:11--4:17
1 | data Wibble = Wobble
2 |
3 | foo : a -> a -> Bool
@ -10,7 +10,7 @@ IfErr.idr:4:11--4:17
Error: While processing right hand side of bar. Can't find an implementation for Eq Wibble.
IfErr.idr:7:11--7:17
IfErr:7:11--7:17
3 | foo : a -> a -> Bool
4 | foo x y = x == y
5 |

4
tests/idris2/error006/expected
View File

@ -1,7 +1,7 @@
1/1: Building IfErr (IfErr.idr)
Error: While processing right hand side of test. Can't find an implementation for Eq Foo.
IfErr.idr:15:10--15:30
IfErr:15:10--15:30
11 | -- hard to achieve and this way is better than displaying the whole
12 | -- top level search when only part of it is relevant)
13 |
@ -11,7 +11,7 @@ IfErr.idr:15:10--15:30
Error: While processing right hand side of test2. Can't find an implementation for Show Foo.
IfErr.idr:23:9--23:29
IfErr:23:9--23:29
19 | MkBar == MkBar = True
20 | _ == _ = False
21 |

2
tests/idris2/error007/expected
View File

@ -1,7 +1,7 @@
1/1: Building CongErr (CongErr.idr)
Error: While processing right hand side of fsprf. Can't solve constraint between: ?_ x and FS x.
CongErr.idr:4:11--4:19
CongErr:4:11--4:19
1 | import Data.Fin
2 |
3 | fsprf : x === y -> Fin.FS x = FS y

2
tests/idris2/error009/expected
View File

@ -1,6 +1,6 @@
Error: Module DoesntExist not found
Exists.idr:1:1--1:19
Exists:1:1--1:19
1 | import DoesntExist
^^^^^^^^^^^^^^^^^^

2
tests/idris2/error010/expected
View File

@ -1,7 +1,7 @@
1/1: Building Loop (Loop.idr)
Error: While processing right hand side of example. Main.example is already defined.
Loop.idr:2:11--2:19
Loop:2:11--2:19
1 | example : String
2 | example = ?example
^^^^^^^^

4
tests/idris2/error011/expected
View File

@ -1,13 +1,13 @@
1/1: Building ConstructorDuplicate (ConstructorDuplicate.idr)
Error: Main.B is already defined.
ConstructorDuplicate.idr:1:14--1:15
ConstructorDuplicate:1:14--1:15
1 | data A = B | B
^
Error: Main.D is already defined.
ConstructorDuplicate.idr:5:3--5:4
ConstructorDuplicate:5:3--5:4
1 | data A = B | B
2 |
3 | data C : Type -> Type where

8
tests/idris2/error013/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue361 (Issue361.idr)
Error: main is not total, possibly not terminating due to call to Main./=
Issue361.idr:7:1--7:13
Issue361:7:1--7:13
3 | data S = T | F
4 |
5 | Eq S where
@ -9,9 +9,9 @@ Issue361.idr:7:1--7:13
7 | main : IO ()
^^^^^^^^^^^^
Error: /= is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--5:11 -> Main.== -> Main./= -> Main.==
Error: /= is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361:5:1--5:11 -> Main.== -> Main./= -> Main.==
Issue361.idr:5:1--5:11
Issue361:5:1--5:11
1 | %default total
2 |
3 | data S = T | F
@ -21,7 +21,7 @@ Issue361.idr:5:1--5:11
Error: == is not total, possibly not terminating due to call to Main./=
Issue361.idr:5:1--5:11
Issue361:5:1--5:11
1 | %default total
2 |
3 | data S = T | F

4
tests/idris2/error014/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue735 (Issue735.idr)
Error: While processing left hand side of isCons. Can't match on :: (Under-applied constructor).
Issue735.idr:5:8--5:12
Issue735:5:8--5:12
1 | module Issue735
2 |
3 | -- Not allowed to pattern-match on under-applied constructors
@ -11,7 +11,7 @@ Issue735.idr:5:8--5:12
Error: While processing left hand side of test. Can't match on A (Under-applied constructor).
Issue735.idr:12:6--12:7
Issue735:12:6--12:7
08 | interface A a where
09 |
10 | -- Not allowed to pattern-match on under-applied type constructors

2
tests/idris2/error015/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue110 (Issue110.idr)
Error: Declaration name (f) shadowed by a pattern variable.
Issue110.idr:8:1--8:14
Issue110:8:1--8:14
4 | data Tup : (a,b : Type) -> Type where
5 | MkTup : (1 f : a) -> (1 s : b) -> Tup a b
6 |

6
tests/idris2/error016/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue1230 (Issue1230.idr)
Error: No type declaration for Main.myRec2.
Issue1230.idr:9:1--9:15
Issue1230:9:1--9:15
5 | myRec1 : R
6 | myRec1 = MkR 3
7 |
@ -11,13 +11,13 @@ Issue1230.idr:9:1--9:15
Did you mean any of: mkRec2, or myRec1?
Main> Error: Undefined name nap.
(interactive):1:4--1:7
(Interactive):1:4--1:7
1 | :t nap
^^^
Did you mean: map?
Main> Error: Undefined name lentgh.
(interactive):1:4--1:10
(Interactive):1:4--1:10
1 | :t lentgh
^^^^^^
Did you mean: length?

2
tests/idris2/error017/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue962 (Issue962.idr)
Error: While processing right hand side of foo. Can't find an implementation for FromString (List Char).
Issue962.idr:3:3--3:8
Issue962:3:3--3:8
1 | foo : List Char -> ()
2 | foo cs = case cs of
3 | "bar" => ()

8
tests/idris2/error018/expected
View File

@ -1,7 +1,7 @@
1/1: Building Issue1031 (Issue1031.idr)
Error: ? is not a valid pattern
Issue1031.idr:4:13--4:14
Issue1031:4:13--4:14
1 | %default total
2 |
3 | ohNo : Void
@ -11,7 +11,7 @@ Issue1031.idr:4:13--4:14
1/1: Building Issue1031-2 (Issue1031-2.idr)
Error: ? is not a valid pattern
Issue1031-2.idr:4:9--4:10
Issue1031-2:4:9--4:10
1 | %default total
2 |
3 | foo : (x : Bool) -> x === True
@ -21,7 +21,7 @@ Issue1031-2.idr:4:9--4:10
1/1: Building Issue1031-3 (Issue1031-3.idr)
Error: ? is not a valid pattern
Issue1031-3.idr:4:6--4:7
Issue1031-3:4:6--4:7
1 | %default total
2 |
3 | cool : (x : Bool) -> x === True
@ -31,7 +31,7 @@ Issue1031-3.idr:4:6--4:7
1/1: Building Issue1031-4 (Issue1031-4.idr)
Error: While processing left hand side of nice. Unsolved holes:
Main.{dotTm:308} introduced at:
Issue1031-4.idr:4:6--4:10
Issue1031-4:4:6--4:10
1 | %default total
2 |
3 | nice : (x : Bool) -> x === True

4
tests/idris2/error019/expected
View File

@ -1,7 +1,7 @@
1/1: Building Error (Error.idr)
Error: Unreachable clause: some False
Error.idr:4:1--4:11
Error:4:1--4:11
1 | some : Bool -> Bool
2 | some True = True
3 | some False = True
@ -10,7 +10,7 @@ Error.idr:4:1--4:11
Error: Unreachable clause: some False
Error.idr:5:1--5:11
Error:5:1--5:11
1 | some : Bool -> Bool
2 | some True = True
3 | some False = True

4
tests/idris2/import002/expected
View File

@ -3,7 +3,7 @@
3/3: Building Test (Test.idr)
Error: While processing type of thing. Undefined name Nat.
Test.idr:5:9--5:12
Test:5:9--5:12
1 | module Test
2 |
3 | import Mult
@ -13,7 +13,7 @@ Test.idr:5:9--5:12
Error: No type declaration for Test.thing.
Test.idr:6:1--6:28
Test:6:1--6:28
2 |
3 | import Mult
4 |

6
tests/idris2/interactive028/expected
View File

@ -1,18 +1,18 @@
Main> Expected 'case', 'if', 'do', application or operator expression.
(interactive):1:4--1:5
(Interactive):1:4--1:5
1 | :t (3 : Nat)
^
Main> Expected string begin.
(interactive):1:5--1:6
(Interactive):1:5--1:6
1 | :cd ..
^
Main> Expected string begin.
(interactive):1:7--1:8
(Interactive):1:7--1:8
1 | :load expected
^

2
tests/idris2/interface008/expected
View File

@ -4,7 +4,7 @@ You may be unintentionally shadowing the associated global definitions:
card is shadowing Main.card
Error: While processing right hand side of badcard. k is not accessible in this context.
Deps.idr:18:13--18:14
Deps:18:13--18:14
14 | badcard : Nat
15 | badto : t -> Fin card
16 |

2
tests/idris2/interface013/expected
View File

@ -1,7 +1,7 @@
1/1: Building TypeInt (TypeInt.idr)
Error: While processing constructor MkRecord. Can't find an implementation for Interface ?s.
TypeInt.idr:14:25--14:49
TypeInt:14:25--14:49
10 | 0 DependentValue : Interface s => Value s -> Type
11 | DependentValue v = concrete (specifier v)
12 |

6
tests/idris2/interface015/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of TestSurprise1. Multiple solutions found in search of:
Gnu
gnu.idr:47:27--47:32
gnu:47:27--47:32
43 |
44 | ||| This is the meat. I'd expect this function to raise an error
45 | ||| because it is ambiguous which local/local function to use.
@ -16,7 +16,7 @@ Possible correct results:
Error: While processing right hand side of TestSurprise2. Multiple solutions found in search of:
Gnu
gnu.idr:50:21--50:26
gnu:50:21--50:26
46 | TestSurprise1 : (gnu1, gnu2 : Gnu) -> String
47 | TestSurprise1 gnu1 gnu2 = Guess
48 |
@ -29,7 +29,7 @@ Possible correct results:
g ()
Error: While processing right hand side of TestSurprise3. Can't find an implementation for Gnu.
gnu.idr:53:19--53:24
gnu:53:19--53:24
49 | TestSurprise2 : (f,g : Unit -> Gnu) -> String
50 | TestSurprise2 f g = Guess
51 |

6
tests/idris2/interface016/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of f. While processing right hand side of f,g. Multiple solutions found in search of:
Num a
TwoNum.idr:4:7--4:8
TwoNum:4:7--4:8
1 | f : Num a => a
2 | f = g where
3 | g : Num a => a
@ -10,5 +10,5 @@ TwoNum.idr:4:7--4:8
^
Possible correct results:
conArg (implicitly bound at TwoNum.idr:4:3--4:8)
conArg (implicitly bound at TwoNum.idr:2:1--4:8)
conArg (implicitly bound at TwoNum:4:3--4:8)
conArg (implicitly bound at TwoNum:2:1--4:8)

2
tests/idris2/interface019/expected
View File

@ -1,7 +1,7 @@
1/1: Building LocalHints (LocalHints.idr)
Error: While processing right hand side of bug. Can't find an implementation for Gnu.
LocalHints.idr:48:17--48:22
LocalHints:48:17--48:22
44 | bug {a} x = let M : More
45 | M = MkMore a
46 | %hint arg : Gnat (Ty M)

2
tests/idris2/interpreter003/expected
View File

@ -1,6 +1,6 @@
Main> Error: Undefined name fromMaybe.
(interactive):1:1--1:10
(Interactive):1:1--1:10
1 | fromMaybe "test" Nothing
^^^^^^^^^

2
tests/idris2/linear006/expected
View File

@ -1,7 +1,7 @@
1/1: Building ZFun (ZFun.idr)
Error: While processing right hand side of bar. Main.test is not accessible in this context.
ZFun.idr:13:7--13:11
ZFun:13:7--13:11
09 | 0 baz : Nat
10 | baz = test foo -- fine!
11 |

Some files were not shown because too many files have changed in this diff Show More