edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-28 23:33:27 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/edwinb/Idris2 into better-ide-mode

Browse Source
This commit is contained in:
Arnaud Bailly 2020-01-11 08:54:12 +01:00
commit 432cc7ca5c
31 changed files with 302 additions and 145 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
src/Compiler/Common.idr
View File

@ -4,7 +4,10 @@ import Compiler.CompileExpr
import Compiler.Inline
import Core.Context
import Core.Directory
import Core.Options
import Core.TT
import Utils.Binary
import Data.NameMap
@ -29,7 +32,14 @@ export
compile : {auto c : Ref Ctxt Defs} ->
Codegen ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile {c} cg = compileExpr cg c
compile {c} cg tm out
= do makeExecDirectory
cwd <- coreLift $ currentDir
d <- getDirs
coreLift $ changeDir (exec_dir d)
fn <- compileExpr cg c tm out
coreLift $ changeDir cwd
pure fn
||| execute
||| As with `compile`, produce a functon that executes
@ -153,3 +163,41 @@ dylib_suffix
= cond [(os `elem` ["windows", "mingw32", "cygwin32"], "dll"),
(os == "darwin", "dylib")]
"so"
export
locate : {auto c : Ref Ctxt Defs} ->
String -> Core (String, String)
locate libspec
= do -- Attempt to turn libspec into an appropriate filename for the system
let fname
= case words libspec of
[] => ""
[fn] => if '.' `elem` unpack fn
then fn -- full filename given
else -- add system extension
fn ++ "." ++ dylib_suffix
(fn :: ver :: _) =>
-- library and version given, build path name as
-- appropriate for the system
cond [(dylib_suffix == "dll",
fn ++ "-" ++ ver ++ ".dll"),
(dylib_suffix == "dylib",
fn ++ "." ++ ver ++ ".dylib")]
(fn ++ "." ++ dylib_suffix ++ "." ++ ver)
fullname <- catch (findLibraryFile fname)
(\err => -- assume a system library so not
-- in our library path
pure fname)
pure (fname, fullname)
export
copyLib : (String, String) -> Core ()
copyLib (lib, fullname)
= if lib == fullname
then pure ()
else do Right bin <- coreLift $ readFromFile fullname
| Left err => throw (FileErr fullname err)
Right _ <- coreLift $ writeToFile lib bin
| Left err => throw (FileErr lib err)
pure ()

30
src/Compiler/Scheme/Chez.idr
View File

@ -25,35 +25,9 @@ findChez
case env of
Just n => pure n
Nothing => do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"],
x <- ["scheme", "chez", "chezscheme9.5"]]
x <- ["chez", "chezscheme9.5", "scheme"]]
pure $ fromMaybe "/usr/bin/env -S scheme" e
locate : {auto c : Ref Ctxt Defs} ->
String -> Core (String, String)
locate libspec
= do -- Attempt to turn libspec into an appropriate filename for the system
let fname
= case words libspec of
[] => ""
[fn] => if '.' `elem` unpack fn
then fn -- full filename given
else -- add system extension
fn ++ "." ++ dylib_suffix
(fn :: ver :: _) =>
-- library and version given, build path name as
-- appropriate for the system
cond [(dylib_suffix == "dll",
fn ++ "-" ++ ver ++ ".dll"),
(dylib_suffix == "dylib",
fn ++ "." ++ ver ++ ".dylib")]
(fn ++ "." ++ dylib_suffix ++ "." ++ ver)
fullname <- catch (findLibraryFile fname)
(\err => -- assume a system library so not
-- in our library path
pure fname)
pure (fname, fullname)
-- Given the chez compiler directives, return a list of pairs of:
-- - the library file name
-- - the full absolute path of the library file name, if it's in one
@ -176,6 +150,7 @@ cCall fc cfn clib args ret
lib <- if clib `elem` loaded
then pure ""
else do (fname, fullname) <- locate clib
copyLib (fname, fullname)
put Loaded (clib :: loaded)
pure $ "(load-shared-object \""
++ escapeQuotes fullname
@ -297,6 +272,7 @@ compileToSS : Ref Ctxt Defs ->
compileToSS c tm outfile
= do ds <- getDirectives Chez
libs <- findLibs ds
traverse_ copyLib libs
(ns, tags) <- findUsedNames tm
defs <- get Ctxt
l <- newRef {t = List String} Loaded ["libc", "libc 6"]

2
src/Compiler/Scheme/Racket.idr
View File

@ -130,6 +130,8 @@ cCall fc cfn libspec args ret
lib <- if libn `elem` loaded
then pure ""
else do put Loaded (libn :: loaded)
ldata <- locate libspec
copyLib ldata
pure (loadlib libn vers)
argTypes <- traverse (\a => do s <- cftySpec fc (snd a)

6
src/Core/Context.idr
View File

@ -1692,6 +1692,12 @@ setBuildDir dir
= do defs <- get Ctxt
put Ctxt (record { options->dirs->build_dir = dir } defs)
export
setExecDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
setExecDir dir
= do defs <- get Ctxt
put Ctxt (record { options->dirs->exec_dir = dir } defs)
export
setSourceDir : {auto c : Ref Ctxt Defs} -> Maybe String -> Core ()
setSourceDir mdir

38
src/Core/Directory.idr
View File

@ -10,20 +10,6 @@ import System.Info
%default total
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
sep : Char
sep = '/'
export
dirSep : String
dirSep = cast sep
export
pathSep : Char
pathSep = if isWindows then ';' else ':'
fullPath : String -> List String
fullPath fp = filter (/="") $ split (==sep) fp
@ -130,6 +116,8 @@ pathToNS wdir sdir fname
export
mkdirs : List String -> IO (Either FileError ())
mkdirs [] = pure (Right ())
mkdirs ("." :: ds) = mkdirs ds
mkdirs ("" :: ds) = mkdirs ds
mkdirs (d :: ds)
= do ok <- changeDir d
if ok
@ -143,6 +131,12 @@ mkdirs (d :: ds)
changeDir ".."
pure (Right ())
isDirSep : Char -> Bool
isDirSep c = cast c == dirSep
splitDir : String -> List String
splitDir = split isDirSep
-- Given a namespace (i.e. a module name), make the build directory for the
-- corresponding ttc file
export
@ -150,13 +144,23 @@ makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
List String -> Core ()
makeBuildDirectory ns
= do d <- getDirs
let bdir = build_dir d
let bdir = splitDir $ build_dir d
let ndirs = case ns of
[] => []
(n :: ns) => ns -- first item is file name
let fname = showSep dirSep (reverse ndirs)
Right _ <- coreLift $ mkdirs (build_dir d :: "ttc" :: reverse ndirs)
| Left err => throw (FileErr (bdir ++ dirSep ++ fname) err)
Right _ <- coreLift $ mkdirs (bdir ++ "ttc" :: reverse ndirs)
| Left err => throw (FileErr (build_dir d ++ dirSep ++ fname) err)
pure ()
export
makeExecDirectory : {auto c : Ref Ctxt Defs} ->
Core ()
makeExecDirectory
= do d <- getDirs
let edir = splitDir $ exec_dir d
Right _ <- coreLift $ mkdirs edir
| Left err => throw (FileErr (exec_dir d) err)
pure ()
-- Given a source file, return the name of the ttc file to generate

118
src/Core/LinearCheck.idr
View File

@ -50,11 +50,12 @@ mutual
updateHoleUsageArgs : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> List (Term vars) -> Core Bool
updateHoleUsageArgs useInHole var [] = pure False
updateHoleUsageArgs useInHole var (a :: as)
= do h <- updateHoleUsage useInHole var a
h' <- updateHoleUsageArgs useInHole var as
Var vars -> List (Var vars) ->
List (Term vars) -> Core Bool
updateHoleUsageArgs useInHole var zs [] = pure False
updateHoleUsageArgs useInHole var zs (a :: as)
= do h <- updateHoleUsage useInHole var zs a
h' <- updateHoleUsageArgs useInHole var zs as
pure (h || h')
-- The assumption here is that hole types are abstracted over the entire
@ -63,24 +64,28 @@ mutual
updateHoleType : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> Term vs -> List (Term vars) ->
Var vars -> List (Var vars) ->
Term vs -> List (Term vars) ->
Core (Term vs)
updateHoleType useInHole var (Bind bfc nm (Pi c e ty) sc) (Local _ r v _ :: as)
updateHoleType useInHole var zs (Bind bfc nm (Pi c e ty) sc) (Local _ r v _ :: as)
-- if the argument to the hole type is the variable of interest,
-- and the variable should be used in the hole, set it to Rig1,
-- otherwise set it to Rig0
= if varIdx var == v
then do scty <- updateHoleType False var sc as
then do scty <- updateHoleType False var zs sc as
let c' = if useInHole then c else Rig0
pure (Bind bfc nm (Pi c' e ty) scty)
else do scty <- updateHoleType useInHole var sc as
pure (Bind bfc nm (Pi c e ty) scty)
updateHoleType useInHole var (Bind bfc nm (Pi c e ty) sc) (a :: as)
= do updateHoleUsage False var a
scty <- updateHoleType useInHole var sc as
else if elem v (map varIdx zs)
then do scty <- updateHoleType useInHole var zs sc as
pure (Bind bfc nm (Pi Rig0 e ty) scty)
else do scty <- updateHoleType useInHole var zs sc as
pure (Bind bfc nm (Pi c e ty) scty)
updateHoleType useInHole var zs (Bind bfc nm (Pi c e ty) sc) (a :: as)
= do updateHoleUsage False var zs a
scty <- updateHoleType useInHole var zs sc as
pure (Bind bfc nm (Pi c e ty) scty)
updateHoleType useInHole var ty as
= do updateHoleUsageArgs False var as
updateHoleType useInHole var zs ty as
= do updateHoleUsageArgs False var zs as
pure ty
updateHoleUsagePats : {auto c : Ref Ctxt Defs} ->
@ -95,7 +100,7 @@ mutual
log 10 $ "At positions " ++ show argpos
-- Find what it's position is in env by looking at the lhs args
let vars = mapMaybe (findLocal (getArgs lhs)) argpos
hs <- traverse (\vsel => updateHoleUsage useInHole vsel rhs)
hs <- traverse (\vsel => updateHoleUsage useInHole vsel [] rhs)
vars
pure (or (map Delay hs))
where
@ -115,39 +120,40 @@ mutual
updateHoleUsage : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
(useInHole : Bool) ->
Var vars -> Term vars -> Core Bool
updateHoleUsage useInHole (MkVar var) (Bind _ n (Let c val ty) sc)
= do h <- updateHoleUsage useInHole (MkVar var) val
h' <- updateHoleUsage useInHole (MkVar (Later var)) sc
Var vars -> List (Var vars) ->
Term vars -> Core Bool
updateHoleUsage useInHole (MkVar var) zs (Bind _ n (Let c val ty) sc)
= do h <- updateHoleUsage useInHole (MkVar var) zs val
h' <- updateHoleUsage useInHole (MkVar (Later var)) (map weaken zs) sc
pure (h || h')
updateHoleUsage useInHole (MkVar var) (Bind _ n b sc)
= updateHoleUsage useInHole (MkVar (Later var)) sc
updateHoleUsage useInHole var (Meta fc n i args)
updateHoleUsage useInHole (MkVar var) zs (Bind _ n b sc)
= updateHoleUsage useInHole (MkVar (Later var)) (map weaken zs) sc
updateHoleUsage useInHole var zs (Meta fc n i args)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => updateHoleUsageArgs useInHole var args
| Nothing => updateHoleUsageArgs useInHole var zs args
-- only update for holes with no definition yet
case definition gdef of
Hole _ _ =>
do let ty = type gdef
ty' <- updateHoleType useInHole var ty args
ty' <- updateHoleType useInHole var zs ty args
updateTy i ty'
pure True
_ => updateHoleUsageArgs useInHole var args
updateHoleUsage useInHole var (As _ a p)
= do h <- updateHoleUsage useInHole var a
h' <- updateHoleUsage useInHole var a
_ => updateHoleUsageArgs useInHole var zs args
updateHoleUsage useInHole var zs (As _ a p)
= do h <- updateHoleUsage useInHole var zs a
h' <- updateHoleUsage useInHole var zs a
pure (h || h')
updateHoleUsage useInHole var (TDelayed _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TDelay _ _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var (TForce _ _ t)
= updateHoleUsage useInHole var t
updateHoleUsage useInHole var tm
updateHoleUsage useInHole var zs (TDelayed _ _ t)
= updateHoleUsage useInHole var zs t
updateHoleUsage useInHole var zs (TDelay _ _ _ t)
= updateHoleUsage useInHole var zs t
updateHoleUsage useInHole var zs (TForce _ _ t)
= updateHoleUsage useInHole var zs t
updateHoleUsage useInHole var zs tm
= case getFnArgs tm of
(Ref _ _ fn, args) =>
do aup <- updateHoleUsageArgs useInHole var args
do aup <- updateHoleUsageArgs useInHole var zs args
defs <- get Ctxt
Just (NS _ (CaseBlock _ _), PMDef _ _ _ _ pats) <-
lookupExactBy (\d => (fullname d, definition d))
@ -156,7 +162,7 @@ mutual
hs <- traverse (updateHoleUsagePats useInHole var args) pats
pure (or (aup :: map Delay hs))
(f, []) => pure False
(f, args) => updateHoleUsageArgs useInHole var (f :: args)
(f, args) => updateHoleUsageArgs useInHole var zs (f :: args)
-- Linearity checking of an already checked term. This serves two purposes:
-- + Checking correct usage of linear bindings
@ -226,12 +232,20 @@ mutual
lcheck rig_in erase env (Bind fc nm b sc)
= do (b', bt, usedb) <- lcheckBinder rig erase env b
(sc', sct, usedsc) <- lcheck rig erase (b' :: env) sc
-- Anything linear can't be used in the scope of a lambda, if we're
-- checking in general context
let env' = case (rig_in, b) of
(RigW, Lam _ _ _) => eraseLinear env
_ => env
(sc', sct, usedsc) <- lcheck rig erase (b' :: env') sc
defs <- get Ctxt
let used_in = count 0 usedsc
holeFound <- if not erase && isLinear (multiplicity b)
then updateHoleUsage (used_in == 0) (MkVar First) sc'
then updateHoleUsage (used_in == 0)
(MkVar First)
(map weaken (getZeroes env'))
sc'
else pure False
-- if there's a hole, assume it will contain the missing usage
@ -250,7 +264,23 @@ mutual
rig : RigCount
rig = case b of
Pi _ _ _ => Rig0
_ => rig_in
_ => case rig_in of
Rig0 => Rig0
_ => Rig1
getZeroes : Env Term vs -> List (Var vs)
getZeroes [] = []
getZeroes (b :: bs)
= case multiplicity b of
Rig0 => MkVar First :: map weaken (getZeroes bs)
_ => map weaken (getZeroes bs)
eraseLinear : Env Term vs -> Env Term vs
eraseLinear [] = []
eraseLinear (b :: bs)
= case multiplicity b of
Rig1 => setMultiplicity b Rig0 :: eraseLinear bs
_ => b :: eraseLinear bs
checkUsageOK : Nat -> RigCount -> Core ()
checkUsageOK used Rig0 = pure ()
@ -405,7 +435,7 @@ mutual
getCaseUsage (Bind _ n (Pi Rig1 e ty) sc) env (Local _ _ idx p :: args) used rhs
= do rest <- getCaseUsage sc env args used rhs
let used_in = count idx used
holeFound <- updateHoleUsage (used_in == 0) (MkVar p) rhs
holeFound <- updateHoleUsage (used_in == 0) (MkVar p) [] rhs
let ause
= if holeFound && used_in == 0
then UseUnknown
@ -458,7 +488,7 @@ mutual
let used_in = count (varIdx pos) usage
holeFound <- if isLinear (multiplicity b)
then updateHoleUsage (used_in == 0) pos tm
then updateHoleUsage (used_in == 0) pos [] tm
else pure False
let used = case rigMult (multiplicity b) rig of
Rig1 => if holeFound && used_in == 0
@ -620,7 +650,7 @@ checkEnvUsage fc rig {done} {vars = nm :: xs} (b :: env) usage tm
let used_in = count (varIdx pos) usage
holeFound <- if isLinear (multiplicity b)
then updateHoleUsage (used_in == 0) pos tm
then updateHoleUsage (used_in == 0) pos [] tm
else pure False
let used = case rigMult (multiplicity b) rig of
Rig1 => if holeFound && used_in == 0

25
src/Core/Options.idr
View File

@ -4,12 +4,15 @@ import Core.Core
import Core.Name
import Utils.Binary
import System.Info
public export
record Dirs where
constructor MkDirs
working_dir : String
source_dir : Maybe String -- source directory, relative to working directory
build_dir : String -- build directory, relative to working directory
exec_dir : String -- executable directory, relative to working directory
dir_prefix : String -- installation prefix, for finding data files (e.g. run time support)
extra_dirs : List String -- places to look for import files
lib_dirs : List String -- places to look for libraries (for code generation)
@ -17,10 +20,11 @@ record Dirs where
public export
toString : Dirs -> String
toString (MkDirs wdir sdir bdir dfix edirs ldirs ddirs) =
toString (MkDirs wdir sdir bdir edir dfix edirs ldirs ddirs) =
unlines [ "+ Working Directory :: " ++ show wdir
, "+ Source Directory :: " ++ show sdir
, "+ Build Directory :: " ++ show bdir
, "+ Executable Directory :: " ++ show edir
, "+ Installation Prefix :: " ++ show dfix
, "+ Extra Directories :: " ++ show edirs
, "+ CG Library Directories :: " ++ show ldirs
@ -110,8 +114,25 @@ record Options where
primnames : PrimNames
extensions : List LangExt
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
export
sep : Char
sep = '/'
export
dirSep : String
dirSep = cast sep
export
pathSep : Char
pathSep = if isWindows then ';' else ':'
defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build" "/usr/local" ["."] ["."] []
defaultDirs = MkDirs "." Nothing "build"
("build" ++ dirSep ++ "exec")
"/usr/local" ["."] ["."] []
defaultPPrint : PPrinter
defaultPPrint = MkPPOpts False True False

2
src/Core/Primitives.idr
View File

@ -113,7 +113,7 @@ sub : Constant -> Constant -> Maybe Constant
sub (BI x) (BI y) = pure $ BI (x - y)
sub (I x) (I y) = pure $ I (x - y)
sub (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x - cast y))
sub (Db x) (Db y) = pure $ Db (x + y)
sub (Db x) (Db y) = pure $ Db (x - y)
sub _ _ = Nothing
mul : Constant -> Constant -> Maybe Constant

2
src/Core/TT.idr
View File

@ -1122,7 +1122,7 @@ export Show (Term vars) where
= "{" ++ showCount c ++ show x ++ " : " ++ show ty ++
"} -> " ++ show sc
showApp (Bind _ x (Pi c AutoImplicit ty) sc) []
= "{auto" ++ showCount c ++ show x ++ " : " ++ show ty ++
= "{auto " ++ showCount c ++ show x ++ " : " ++ show ty ++
"} -> " ++ show sc
showApp (Bind _ x (PVar c Explicit ty) sc) []
= "pat " ++ showCount c ++ show x ++ " : " ++ show ty ++

4
src/Core/TTC.idr
View File

@ -178,7 +178,7 @@ TTC (Var vars) where
mutual
export
TTC (Binder (Term vars)) where
toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; -- toBuf b ty
toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; toBuf b ty
toBuf b (Let c val ty) = do tag 1; toBuf b c; toBuf b val -- ; toBuf b ty
toBuf b (Pi c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty
toBuf b (PVar c p ty) = do tag 3; toBuf b c; toBuf b p; toBuf b ty
@ -187,7 +187,7 @@ mutual
fromBuf b
= case !getTag of
0 => do c <- fromBuf b; x <- fromBuf b; pure (Lam c x (Erased emptyFC))
0 => do c <- fromBuf b; x <- fromBuf b; ty <- fromBuf b; pure (Lam c x ty)
1 => do c <- fromBuf b; x <- fromBuf b; pure (Let c x (Erased emptyFC))
2 => do c <- fromBuf b; x <- fromBuf b; y <- fromBuf b; pure (Pi c x y)
3 => do c <- fromBuf b; p <- fromBuf b; ty <- fromBuf b; pure (PVar c p ty)

4
src/Core/Unify.idr
View File

@ -1097,7 +1097,7 @@ retryGuess mode smode (hid, (loc, hname))
(do tm <- search loc rig (smode == Defaults) depth defining
(type def) []
let gdef = record { definition = PMDef False [] (STerm tm) (STerm tm) [] } def
logTerm 5 ("Solved " ++ show hname) tm
logTermNF 5 ("Solved " ++ show hname) [] tm
addDef (Resolved hid) gdef
removeGuess hid
pure True)
@ -1161,7 +1161,7 @@ solveConstraints umode smode
= do ust <- get UST
progress <- traverse (retryGuess umode smode) (toList (guesses ust))
when (or (map Delay progress)) $
solveConstraints umode smode
solveConstraints umode Normal
-- Replace any 'BySearch' with 'Hole', so that we don't keep searching
-- fruitlessly while elaborating the rest of a source file

2
src/Core/UnifyState.idr
View File

@ -429,7 +429,7 @@ newSearch : {auto c : Ref Ctxt Defs} ->
newSearch {vars} fc rig depth def env n ty
= do let hty = abstractEnvType fc env ty
let hole = newDef fc n rig [] hty Public (BySearch rig depth def)
log 10 $ "Adding new search " ++ show n
log 10 $ "Adding new search " ++ show fc ++ " " ++ show n
idx <- addDef n hole
addGuessName fc n idx
pure (idx, Meta fc n idx envArgs)

16
src/Idris/Desugar.idr
View File

@ -489,6 +489,17 @@ mutual
getDecl Single d = Just d
export
desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} ->
List Name -> PFnOpt -> Core FnOpt
desugarFnOpt ps (IFnOpt f) = pure f
desugarFnOpt ps (PForeign tms)
= do tms' <- traverse (desugar AnyExpr ps) tms
pure (ForeignFn tms')
-- Given a high level declaration, return a list of TTImp declarations
-- which process it, and update any necessary state on the way.
export
@ -497,8 +508,9 @@ mutual
{auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} ->
List Name -> PDecl -> Core (List ImpDecl)
desugarDecl ps (PClaim fc rig vis opts ty)
= pure [IClaim fc rig vis opts !(desugarType ps ty)]
desugarDecl ps (PClaim fc rig vis fnopts ty)
= do opts <- traverse (desugarFnOpt ps) fnopts
pure [IClaim fc rig vis opts !(desugarType ps ty)]
desugarDecl ps (PDef fc clauses)
-- The clauses won't necessarily all be from the same function, so split
-- after desugaring, by function name, using collectDefs from RawImp

3
src/Idris/Elab/Implementation.idr
View File

@ -243,7 +243,7 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln mbody
applyTo fc tm ((x, c, Explicit) :: xs)
= applyTo fc (IApp fc tm (IVar fc x)) xs
applyTo fc tm ((x, c, AutoImplicit) :: xs)
= applyTo fc (IImplicitApp fc tm Nothing (IVar fc x)) xs
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
applyTo fc tm ((x, c, Implicit) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
@ -318,6 +318,7 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln mbody
log 3 $ "Method " ++ show mn ++ " ==> " ++
show n ++ " : " ++ show mty
log 3 $ " (initially " ++ show mty_in ++ ")"
log 5 $ "Updates " ++ show methupds
log 5 $ "From " ++ show mbase
log 3 $ "Name updates " ++ show upds

20
src/Idris/Elab/Interface.idr
View File

@ -62,6 +62,18 @@ mkIfaceData {vars} fc vis env constraints n conName ps dets meths
mkTy imp ((n, c, argty) :: args) ret
= IPi fc c imp n argty (mkTy imp args ret)
-- Give implicit Pi bindings explicit names, if they don't have one already,
-- because we need them to be consistent everywhere we refer to them
namePis : Int -> RawImp -> RawImp
namePis i (IPi fc r AutoImplicit Nothing ty sc)
= IPi fc r AutoImplicit (Just (MN "i_con" i)) ty (namePis (i + 1) sc)
namePis i (IPi fc r Implicit Nothing ty sc)
= IPi fc r Implicit (Just (MN "i_imp" i)) ty (namePis (i + 1) sc)
namePis i (IPi fc r p n ty sc)
= IPi fc r p n ty (namePis i sc)
namePis i (IBindHere fc m ty) = IBindHere fc m (namePis i ty)
namePis i ty = ty
-- Get the implicit arguments for a method declaration or constraint hint
-- to allow us to build the data declaration
getMethDecl : {auto c : Ref Ctxt Defs} ->
@ -184,8 +196,10 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
constName n = UN (bindName n)
getSig : ImpDecl -> Maybe (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
getSig (IClaim _ c _ opts (MkImpTy fc n ty)) = Just (fc, c, opts, n, (False, ty))
getSig (IData _ _ (MkImpLater fc n ty)) = Just (fc, Rig0, [Invertible], n, (True, ty))
getSig (IClaim _ c _ opts (MkImpTy fc n ty))
= Just (fc, c, opts, n, (False, namePis 0 ty))
getSig (IData _ _ (MkImpLater fc n ty))
= Just (fc, Rig0, [Invertible], n, (True, namePis 0 ty))
getSig _ = Nothing
getDefault : ImpDecl -> Maybe (FC, List FnOpt, Name, List ImpClause)
@ -227,7 +241,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
-- Machine generated names need to be qualified when looking them up
conName <- inCurrentNS conName_in
let meth_sigs = mapMaybe getSig body -- (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
let meth_decls = map (\ (f, c, o, n, ty) => (n, c, ty)) meth_sigs
let meth_decls = map (\ (f, c, o, n, b, ty) => (n, c, b, ty)) meth_sigs
let meth_names = map fst meth_decls
let defaults = mapMaybe getDefault body

2
src/Idris/Error.idr
View File

@ -80,6 +80,8 @@ perror (NotTotal fc n r)
= pure $ show n ++ " is not total"
perror (LinearUsed fc count n)
= pure $ "There are " ++ show count ++ " uses of linear name " ++ sugarName n
perror (LinearMisuse fc n Rig0 ctx)
= pure $ show n ++ " is not accessible in this context"
perror (LinearMisuse fc n exp ctx)
= pure $ "Trying to use " ++ showRig exp ++ " name " ++ sugarName n ++
" in " ++ showRel ctx ++ " context"

38
src/Idris/Parser.idr
View File

@ -1006,44 +1006,44 @@ paramDecls fname indents
end <- location
pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds)))
fnOpt : Rule FnOpt
fnOpt : Rule PFnOpt
fnOpt
= do keyword "partial"
pure PartialOK
pure $ IFnOpt PartialOK
<|> do keyword "total"
pure Total
pure $ IFnOpt Total
<|> do keyword "covering"
pure Covering
pure $ IFnOpt Covering
fnDirectOpt : Rule FnOpt
fnDirectOpt
fnDirectOpt : FileName -> Rule PFnOpt
fnDirectOpt fname
= do exactIdent "hint"
pure (Hint True)
pure $ IFnOpt (Hint True)
<|> do exactIdent "globalhint"
pure (GlobalHint False)
pure $ IFnOpt (GlobalHint False)
<|> do exactIdent "defaulthint"
pure (GlobalHint True)
pure $ IFnOpt (GlobalHint True)
<|> do exactIdent "inline"
pure Inline
pure $ IFnOpt Inline
<|> do exactIdent "extern"
pure ExternFn
pure $ IFnOpt ExternFn
<|> do exactIdent "macro"
pure Macro
pure $ IFnOpt Macro
<|> do exactIdent "foreign"
cs <- many strLit
pure (ForeignFn cs)
cs <- block (expr pdef fname)
pure $ PForeign cs
visOpt : Rule (Either Visibility FnOpt)
visOpt
visOpt : FileName -> Rule (Either Visibility PFnOpt)
visOpt fname
= do vis <- visOption
pure (Left vis)
<|> do tot <- fnOpt
pure (Right tot)
<|> do symbol "%"
opt <- fnDirectOpt
opt <- fnDirectOpt fname
pure (Right opt)
getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->
getVisibility : Maybe Visibility -> List (Either Visibility PFnOpt) ->
EmptyRule Visibility
getVisibility Nothing [] = pure Private
getVisibility (Just vis) [] = pure vis
@ -1193,7 +1193,7 @@ recordDecl fname indents
claim : FileName -> IndentInfo -> Rule PDecl
claim fname indents
= do start <- location
visOpts <- many visOpt
visOpts <- many (visOpt fname)
vis <- getVisibility Nothing visOpts
let opts = mapMaybe getRight visOpts
m <- multiplicity

10
src/Idris/REPL.idr
View File

@ -670,12 +670,12 @@ mutual
opts <- get ROpts
coreLift (putStr (prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> "))
inp <- coreLift getLine
repeat <- interpret inp
end <- coreLift $ fEOF stdin
if repeat && not end
then repl
else do iputStrLn "Bye for now!"
pure ()
if end
then do
-- start a new line in REPL mode (not relevant in IDE mode)
coreLift $ putStrLn ""
iputStrLn "Bye for now!"
else do res <- interpret inp
handleResult res

10
src/Idris/Resugar.idr
View File

@ -323,12 +323,20 @@ mutual
fs' <- traverse toPField fs
pure (n, ps', con, fs')
toPFnOpt : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
FnOpt -> Core PFnOpt
toPFnOpt (ForeignFn cs)
= do cs' <- traverse (toPTerm startPrec) cs
pure (PForeign cs')
toPFnOpt o = pure $ IFnOpt o
toPDecl : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
ImpDecl -> Core (Maybe PDecl)
toPDecl (IClaim fc rig vis opts ty)
= pure (Just (PClaim fc rig vis opts !(toPTypeDecl ty)))
= do opts' <- traverse toPFnOpt opts
pure (Just (PClaim fc rig vis opts' !(toPTypeDecl ty)))
toPDecl (IData fc vis d)
= pure (Just (PData fc vis !(toPData d)))
toPDecl (IDef fc n cs)

7
src/Idris/Syntax.idr
View File

@ -181,9 +181,14 @@ mutual
defPass : Pass -> Bool
defPass p = p == Single || p == AsDef
public export
data PFnOpt : Type where
IFnOpt : FnOpt -> PFnOpt
PForeign : List PTerm -> PFnOpt
public export
data PDecl : Type where
PClaim : FC -> RigCount -> Visibility -> List FnOpt -> PTypeDecl -> PDecl
PClaim : FC -> RigCount -> Visibility -> List PFnOpt -> PTypeDecl -> PDecl
PDef : FC -> List PClause -> PDecl
PData : FC -> Visibility -> PDataDecl -> PDecl
PParameters : FC -> List (Name, PTerm) -> List PDecl -> PDecl

2
src/TTImp/Elab.idr
View File

@ -109,7 +109,7 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
solveConstraints solvemode Normal
logTerm 5 "Looking for delayed in " chktm
ust <- get UST
catch (retryDelayed (delayedElab ust))
catch (retryDelayed (reverse (delayedElab ust)))
(\err =>
do ust <- get UST
put UST (record { delayedElab = olddelayed } ust)

23
src/TTImp/ProcessType.idr
View File

@ -55,11 +55,29 @@ processFnOpt fc ndef PartialOK
processFnOpt fc ndef Macro
= setFlag fc ndef Macro
getFnString : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
RawImp -> Core String
getFnString (IPrimVal _ (Str st)) = pure st
getFnString tm
= do inidx <- resolveName (UN "[foreign]")
let fc = getFC tm
let gstr = gnf [] (PrimVal fc StringType)
etm <- checkTerm inidx InExpr [] (MkNested []) [] tm gstr
defs <- get Ctxt
case !(nf defs [] etm) of
NPrimVal fc (Str st) => pure st
_ => throw (GenericMsg fc "%foreign calling convention must evaluate to a String")
-- If it's declared as externally defined, set the definition to
-- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
-- not dependent on any of the arguments)
-- Similarly set foreign definitions. Possibly combine these?
initDef : {auto c : Ref Ctxt Defs} ->
initDef : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def
initDef n env ty []
= do addUserHole n
@ -71,7 +89,8 @@ initDef n env ty (ExternFn :: opts)
initDef n env ty (ForeignFn cs :: opts)
= do defs <- get Ctxt
a <- getArity defs env ty
pure (ForeignDef a cs)
cs' <- traverse getFnString cs
pure (ForeignDef a cs')
initDef n env ty (_ :: opts) = initDef n env ty opts
export

6
src/TTImp/TTImp.idr
View File

@ -139,7 +139,7 @@ mutual
= "(|" ++ showSep "," (map show alts) ++ "|)"
show (IRewrite _ rule tm)
= "(%rewrite (" ++ show rule ++ ") (" ++ show tm ++ "))"
show (ICoerced _ tm) = show tm
show (ICoerced _ tm) = "(%coerced " ++ show tm ++ ")"
show (IBindHere fc b sc)
= "(%bindhere " ++ show sc ++ ")"
@ -174,7 +174,7 @@ mutual
GlobalHint : Bool -> FnOpt
ExternFn : FnOpt
-- Defined externally, list calling conventions
ForeignFn : List String -> FnOpt
ForeignFn : List RawImp -> FnOpt
-- assume safe to cancel arguments in unification
Invertible : FnOpt
Total : FnOpt
@ -201,7 +201,7 @@ mutual
(Hint x) == (Hint y) = x == y
(GlobalHint x) == (GlobalHint y) = x == y
ExternFn == ExternFn = True
(ForeignFn xs) == (ForeignFn ys) = xs == ys
(ForeignFn xs) == (ForeignFn ys) = True -- xs == ys
Invertible == Invertible = True
Total == Total = True
Covering == Covering = True

3
tests/Main.idr
View File

@ -40,6 +40,7 @@ idrisTests
"interface005", "interface006", "interface007", "interface008",
"interface009", "interface010", "interface011", "interface012",
"interface013", "interface014",
"interpreter001",
"lazy001",
"linear001", "linear002", "linear003", "linear004", "linear005",
"linear006", "linear007",
@ -125,7 +126,7 @@ findChez
case env of
Just n => pure $ Just n
Nothing => firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"],
x <- ["scheme", "chez", "chezscheme9.5"]]
x <- ["chez", "chezscheme9.5", "scheme"]]
runChezTests : String -> List String -> IO (List Bool)
runChezTests prog tests

11
tests/chez/chez010/CB.idr
View File

@ -1,13 +1,16 @@
%foreign "C:add, libcb.so"
libcb : String -> String
libcb f = "C:" ++ f ++", libcb"
%foreign libcb "add"
add : Int -> Int -> Int
%foreign "C:applyIntFn, libcb.so"
%foreign libcb "applyIntFn"
prim_applyIntFn : Int -> Int -> (Int -> Int -> PrimIO Int) -> PrimIO Int
%foreign "C:applyCharFn, libcb.so"
%foreign libcb "applyCharFn"
prim_applyCharFn : Char -> Int -> (Char -> Int -> PrimIO Char) -> PrimIO Char
%foreign "C:applyIntFnPure, libcb.so"
%foreign libcb "applyIntFnPure"
applyIntFnPure : Int -> Int -> (Int -> Int -> Int) -> Int
applyIntFn : Int -> Int -> (Int -> Int -> IO Int) -> IO Int

2
tests/idris2/interface008/expected
View File

@ -1,3 +1,3 @@
1/1: Building Deps (Deps.idr)
Deps.idr:18:13--19:3:While processing right hand side of Main.badcard at Deps.idr:18:3--19:3:
Trying to use irrelevant name k in relevant context
k is not accessible in this context

2
tests/idris2/interpreter001/expected Normal file
View File

@ -0,0 +1,2 @@
Main> 1.5
Main> Bye for now!

2
tests/idris2/interpreter001/input Normal file
View File

@ -0,0 +1,2 @@
3.5 - 2.0
:q

1
tests/idris2/interpreter001/run Executable file
View File

@ -0,0 +1 @@
$1 --no-banner < input

4
tests/idris2/linear004/expected
View File

@ -3,7 +3,7 @@
Main> S Z
Main> S (S Z)
Main> S Z
Main> (interactive):1:15--1:16:Trying to use irrelevant name x in relevant context
Main> (interactive):1:15--1:16:x is not accessible in this context
Main> (interactive):1:5--1:31:When unifying Nat -> Nat -> Nat and (0 x : Nat) -> Nat -> Nat
Mismatch between:
Nat -> Nat -> Nat
@ -14,7 +14,7 @@ Mismatch between:
(1 x : Nat) -> Nat -> Nat
and
(0 x : Nat) -> Nat -> Nat
Main> (interactive):1:20--1:22:Trying to use irrelevant name x in non-linear context
Main> (interactive):1:20--1:22:x is not accessible in this context
Main> S (S Z)
Main> S (S Z)
Main> (interactive):1:6--1:31:When unifying (0 x : Nat) -> Nat -> Nat and Nat -> Nat -> Nat

2
tests/idris2/linear006/expected
View File

@ -1,5 +1,5 @@
1/1: Building ZFun (ZFun.idr)
ZFun.idr:13:7--15:1:While processing right hand side of Main.bar at ZFun.idr:13:1--15:1:
Trying to use irrelevant name Main.test in relevant context
Main.test is not accessible in this context
Main> [tc] Main> S (S (S (S (S (S (S (S (S (S Z)))))))))
[tc] Main> Bye for now!