edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-20 04:17:38 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/edwinb/Idris2 into network-lib

Browse Source
This commit is contained in:
Arnaud Bailly 2019-07-27 17:27:49 +02:00
commit 02978c81fc
No known key found for this signature in database
GPG Key ID: 389CC2BC5448321E
39 changed files with 308 additions and 302 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -1,5 +1,7 @@
*~
*.ibc
*.ttc
*.ttm
idris2
runtests

10
Makefile
View File

@ -1,14 +1,20 @@
PREFIX ?= ${HOME}/.idris2
IDRIS_VERSION := $(shell idris --version)
VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"
export IDRIS2_PATH = ${CURDIR}/libs/prelude/build:${CURDIR}/libs/base/build
export IDRIS2_DATA = ${CURDIR}/support
-include custom.mk
.PHONY: ttimp idris2 prelude test base clean lib_clean
.PHONY: ttimp idris2 prelude test base clean lib_clean check_version
all: idris2 libs test
idris2: src/YafflePaths.idr
check_version:
@echo "Using idris version: $(IDRIS_VERSION)"
@if [ $(shell expr $(IDRIS_VERSION) : $(VALID_IDRIS_VERSION_REGEXP)) -eq 0 ]; then echo "Wrong idris version, expected version matching $(VALID_IDRIS_VERSION_REGEXP)"; exit 1; fi
idris2: src/YafflePaths.idr check_version
idris --build idris2.ipkg
src/YafflePaths.idr:

22
libs/base/Data/List.idr
View File

@ -109,6 +109,16 @@ export
reverse : List a -> List a
reverse = reverseOnto []
||| Compute the intersect of two lists by user-supplied equality predicate.
export
intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
||| Compute the intersect of two lists according to the `Eq` implementation for the elements.
export
intersect : Eq a => List a -> List a -> List a
intersect = intersectBy (==)
public export
data NonEmpty : (xs : List a) -> Type where
IsNonEmpty : NonEmpty (x :: xs)
@ -197,11 +207,13 @@ sort = sortBy compare
-- Properties
--------------------------------------------------------------------------------
-- Uninhabited ([] = _ :: _) where
-- uninhabited Refl impossible
--
-- Uninhabited (_ :: _ = []) where
-- uninhabited Refl impossible
export
Uninhabited ([] = Prelude.(::) x xs) where
uninhabited Refl impossible
export
Uninhabited (Prelude.(::) x xs = []) where
uninhabited Refl impossible
--
-- ||| (::) is injective
-- consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->

76
libs/base/Data/List/Elem.idr Normal file
View File

@ -0,0 +1,76 @@
module Data.List.Elem
import Decidable.Equality
--------------------------------------------------------------------------------
-- List membership proof
--------------------------------------------------------------------------------
||| A proof that some element is found in a list.
public export
data Elem : a -> List a -> Type where
||| A proof that the element is at the head of the list
Here : Elem x (x :: xs)
||| A proof that the element is in the tail of the list
There : Elem x xs -> Elem x (y :: xs)
export
Uninhabited (Here = There e) where
uninhabited Refl impossible
export
Uninhabited (There e = Here) where
uninhabited Refl impossible
export
thereInjective : {0 e1, e2 : Elem x xs} -> There e1 = There e2 -> e1 = e2
thereInjective Refl = Refl
export
DecEq (Elem x xs) where
decEq Here Here = Yes Refl
decEq Here (There later) = No absurd
decEq (There later) Here = No absurd
decEq (There this) (There that) with (decEq this that)
decEq (There this) (There this) | Yes Refl = Yes Refl
decEq (There this) (There that) | No contra = No (contra . thereInjective)
export
Uninhabited (Elem {a} x []) where
uninhabited Here impossible
uninhabited (There p) impossible
||| An item not in the head and not in the tail is not in the list at all.
export
neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
neitherHereNorThere xny xnxs Here = xny Refl
neitherHereNorThere xny xnxs (There xxs) = xnxs xxs
||| Check whether the given element is a member of the given list.
export
isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
isElem x [] = No absurd
isElem x (y :: xs) with (decEq x y)
isElem x (x :: xs) | Yes Refl = Yes Here
isElem x (y :: xs) | No xny with (isElem x xs)
isElem x (y :: xs) | No xny | Yes xxs = Yes (There xxs)
isElem x (y :: xs) | No xny | No xnxs = No (neitherHereNorThere xny xnxs)
||| Remove the element at the given position.
export
dropElem : (xs : List a) -> (p : Elem x xs) -> List a
dropElem (x :: ys) Here = ys
dropElem (x :: ys) (There p) = x :: dropElem ys p
||| Erase the indices, returning the numeric position of the element
export
elemToNat : Elem x xs -> Nat
elemToNat Here = Z
elemToNat (There p) = S (elemToNat p)
||| Find the element with a proof at a given position, if it is valid
export
indexElem : Nat -> (xs : List a) -> Maybe (x ** Elem x xs)
indexElem _ [] = Nothing
indexElem Z (y :: ys) = Just (y ** Here)
indexElem (S n) (y :: ys) = map (\(x ** p) => (x ** There p)) (indexElem n ys)

1
libs/base/base.ipkg
View File

@ -10,6 +10,7 @@ modules = Control.Monad.Identity,
Data.Fin,
Data.IORef,
Data.List,
Data.List.Elem,
Data.List.Views,
Data.Maybe,
Data.Morphisms,

2
src/Compiler/CompileExpr.idr
View File

@ -304,7 +304,7 @@ toCDef tags n (TCon tag arity _ _ _ _)
_ => pure $ MkCon tag arity
-- We do want to be able to compile these, but also report an error at run time
-- (and, TODO: warn at compile time)
toCDef tags n (Hole _ _ _)
toCDef tags n (Hole _ _)
= pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++
show !(getFullName n))
toCDef tags n (Guess _ _)

24
src/Core/AutoSearch.idr
View File

@ -44,8 +44,8 @@ mkArgs fc rigc env (NBind nfc x (Pi c p ty) sc)
argTy <- quote empty env ty
let argRig = rigMult rigc c
(idx, arg) <- newMeta fc argRig env nm argTy
(Hole (length env) False False) False
setInvertible fc idx
(Hole (length env) False) False
setInvertible fc (Resolved idx)
(rest, restTy) <- mkArgs fc rigc env
!(sc defs (toClosure defaultOpts env arg))
pure (MkArgInfo idx argRig p arg argTy :: rest, restTy)
@ -68,7 +68,7 @@ searchIfHole fc defaults trying ispair (S depth) def top env arg
defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
| Nothing => throw (CantSolveGoal fc [] top)
let Hole _ _ inv = definition gdef
let Hole _ _ = definition gdef
| _ => pure () -- already solved
top' <- if ispair
then normaliseScope defs [] (type gdef)
@ -146,12 +146,13 @@ exactlyOne {vars} fc env top all
-- search happens before linearity checking and we can't guarantee that just
-- because something is apparently available now, it will be available by the
-- time we get to linearity checking.
getAllEnv : FC -> (done : List Name) ->
-- It's also fine to use anything if we're working at multiplicity 0
getAllEnv : FC -> RigCount -> (done : List Name) ->
Env Term vars -> List (Term (done ++ vars), Term (done ++ vars))
getAllEnv fc done [] = []
getAllEnv {vars = v :: vs} fc done (b :: env)
= let rest = getAllEnv fc (done ++ [v]) env in
if multiplicity b == RigW
getAllEnv fc rigc done [] = []
getAllEnv {vars = v :: vs} fc rigc done (b :: env)
= let rest = getAllEnv fc rigc (done ++ [v]) env in
if multiplicity b == RigW || rigc == Rig0
then let MkVar p = weakenVar {name=v} {inner=v :: vs} done First in
(Local fc Nothing _ p,
rewrite appendAssociative done [v] vs in
@ -301,7 +302,8 @@ searchLocal : {auto c : Ref Ctxt Defs} ->
Env Term vars ->
(target : NF vars) -> Core (Term vars)
searchLocal fc rig defaults trying depth def top env target
= searchLocalWith fc rig defaults trying depth def top env (getAllEnv fc [] env) target
= searchLocalWith fc rig defaults trying depth def top env
(getAllEnv fc rig [] env) target
isPairNF : {auto c : Ref Ctxt Defs} ->
Env Term vars -> NF vars -> Defs -> Core Bool
@ -406,11 +408,11 @@ concreteDets {vars} fc defaults env top pos dets (arg :: args)
concrete defs argnf False) args
pure ()
concrete defs (NApp _ (NMeta n i _) _) True
= do Just (Hole _ True _) <- lookupDefExact n (gamma defs)
= do Just (Hole _ True) <- lookupDefExact n (gamma defs)
| _ => throw (DeterminingArg fc n i [] top)
pure ()
concrete defs (NApp _ (NMeta n i _) _) False
= do Just (Hole _ True _) <- lookupDefExact n (gamma defs)
= do Just (Hole _ True) <- lookupDefExact n (gamma defs)
| def => throw (CantSolveGoal fc [] top)
pure ()
concrete defs tm top = pure ()

3
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 4
ttcVersion = 5
export
checkTTCVersion : Int -> Int -> Core ()
@ -226,6 +226,7 @@ readTTCFile modns as b
[] [] [] defs -- holes guesses constraints defs
autohs typehs imp nextv cns nns
pns rws prims nds cgds ex)
-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : List Name -> List (Name, Binary) -> Defs ->
Core (List (Name, Binary))

9
src/Core/Context.idr
View File

@ -45,7 +45,6 @@ data Def : Type where
Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point
-- (mostly to help display)
(implbind : Bool) -> -- Does this stand for an implicitly bound name
(invertible : Bool) -> -- Can we invert it during unification?
Def
BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def
-- Constraints are integer references into the current map of
@ -68,8 +67,7 @@ Show Def where
" mutual with: " ++ show ms
show (ExternDef arity) = "<external def with arith " ++ show arity ++ ">"
show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
show (Hole _ p inv) = "Hole" ++ if p then " [impl]" else ""
++ if inv then " [invertible]" else ""
show (Hole _ p) = "Hole" ++ if p then " [impl]" else ""
show (BySearch c depth def) = "Search in " ++ show def
show (Guess tm cs) = "Guess " ++ show tm ++ " when " ++ show cs
show ImpBind = "Bound name"
@ -164,6 +162,7 @@ record GlobalDef where
totality : Totality
flags : List DefFlag
refersToM : Maybe (NameMap Bool)
invertible : Bool -- for an ordinary definition, is it invertible in unification
noCycles : Bool -- for metavariables, whether they can be cyclic (this
-- would only be allowed when using a metavariable as a
-- placeholder for a yet to be elaborated arguments, but
@ -417,7 +416,7 @@ export
newDef : FC -> Name -> RigCount -> List Name ->
ClosedTerm -> Visibility -> Def -> GlobalDef
newDef fc n rig vars ty vis def
= MkGlobalDef fc n ty rig vars vis unchecked [] empty False False def
= MkGlobalDef fc n ty rig vars vis unchecked [] empty False False False def
Nothing []
public export
@ -788,7 +787,7 @@ addBuiltin : {auto x : Ref Ctxt Defs} ->
PrimFn arity -> Core ()
addBuiltin n ty tot op
= do addDef n (MkGlobalDef emptyFC n ty RigW [] Public tot
[Inline] empty False True (Builtin op)
[Inline] empty False False True (Builtin op)
Nothing [])
pure ()

4
src/Core/LinearCheck.idr
View File

@ -128,7 +128,7 @@ mutual
| Nothing => updateHoleUsageArgs useInHole var args
-- only update for holes with no definition yet
case definition gdef of
Hole _ _ _ =>
Hole _ _ =>
do let ty = type gdef
ty' <- updateHoleType useInHole var ty args
updateTy i ty'
@ -212,7 +212,7 @@ mutual
then expandMeta rig erase env n idx (definition gdef) args
else do let ty : ClosedTerm
= case definition gdef of
Hole _ _ _ => unusedHoleArgs args (type gdef)
Hole _ _ => unusedHoleArgs args (type gdef)
_ => type gdef
nty <- nf defs env (embed ty)
lcheckMeta rig erase env fc n idx args [] nty

12
src/Core/TTC.idr
View File

@ -714,9 +714,8 @@ TTC Def where
toBuf b (TCon t arity parampos detpos ms datacons)
= do tag 4; toBuf b t; toBuf b arity; toBuf b parampos
toBuf b detpos; toBuf b ms; toBuf b datacons
toBuf b (Hole locs p invertible)
toBuf b (Hole locs p)
= do tag 5; toBuf b locs; toBuf b p
toBuf b invertible
toBuf b (BySearch c depth def)
= do tag 6; toBuf b c; toBuf b depth; toBuf b def
toBuf b (Guess guess constraints) = do tag 7; toBuf b guess; toBuf b constraints
@ -741,8 +740,7 @@ TTC Def where
pure (TCon t a ps dets ms cs)
5 => do l <- fromBuf b
p <- fromBuf b
i <- fromBuf b
pure (Hole l p i)
pure (Hole l p)
6 => do c <- fromBuf b; depth <- fromBuf b
def <- fromBuf b
pure (BySearch c depth def)
@ -820,6 +818,7 @@ TTC GlobalDef where
toBuf b (visibility gdef)
toBuf b (totality gdef)
toBuf b (flags gdef)
toBuf b (invertible gdef)
toBuf b (noCycles gdef)
toBuf b (sizeChange gdef)
@ -835,14 +834,15 @@ TTC GlobalDef where
vars <- fromBuf b
vis <- fromBuf b; tot <- fromBuf b
fl <- fromBuf b
inv <- fromBuf b
c <- fromBuf b
sc <- fromBuf b
pure (MkGlobalDef loc name ty mul vars vis
tot fl refs c True def cdef sc)
tot fl refs inv c True def cdef sc)
else do let fc = emptyFC
pure (MkGlobalDef fc name (Erased fc)
RigW [] Public unchecked [] refs
False True def cdef [])
False False True def cdef [])
-- decode : Context -> Int -> ContextEntry -> Core GlobalDef
Core.Context.decode gam idx (Coded bin)

70
src/Core/Unify.idr
View File

@ -404,7 +404,7 @@ solveIfUndefined : {vars : _} ->
Env Term vars -> Term vars -> Term vars -> Core Bool
solveIfUndefined env (Meta fc mname idx args) soln
= do defs <- get Ctxt
Just (Hole _ _ _) <- lookupDefExact (Resolved idx) (gamma defs)
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
| pure False
case !(patternEnvTm env args) of
Nothing => pure False
@ -423,9 +423,9 @@ isDefInvertible : {auto c : Ref Ctxt Defs} ->
Int -> Core Bool
isDefInvertible i
= do defs <- get Ctxt
Just (Hole _ _ t) <- lookupDefExact (Resolved i) (gamma defs)
| _ => pure False
pure t
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => pure False
pure (invertible gdef)
mutual
unifyIfEq : {auto c : Ref Ctxt Defs} ->
@ -541,9 +541,7 @@ mutual
= do defs <- get Ctxt
Just mdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => throw (UndefinedName nfc mname)
let inv = case definition mdef of
Hole _ _ i => i
_ => isPatName n
let inv = isPatName n || invertible mdef
if inv
then unifyInvertible mode loc env mname mref margs margs' Nothing
(NApp nfc (NMeta n i margs2)) args2'
@ -558,19 +556,16 @@ mutual
= postpone loc "Postponing hole application" env
(NApp loc (NMeta mname mref margs) margs') tm
unifyPatVar : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyMode -> FC -> Env Term vars ->
(metaname : Name) -> (metaref : Int) ->
(margs : List (Closure vars)) ->
(margs' : List (Closure vars)) ->
(soln : NF vars) ->
Core UnifyResult
-- TODO: if either side is a pattern variable application, and we're in a term,
-- (which will be a type) we can proceed because the pattern variable
-- has to end up pi bound. Unify the right most variables, and continue.
unifyPatVar mode loc env mname mref margs margs' tm
postponePatVar : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyMode -> FC -> Env Term vars ->
(metaname : Name) -> (metaref : Int) ->
(margs : List (Closure vars)) ->
(margs' : List (Closure vars)) ->
(soln : NF vars) ->
Core UnifyResult
postponePatVar mode loc env mname mref margs margs' tm
= postpone loc "Not in pattern fragment" env
(NApp loc (NMeta mname mref margs) margs') tm
@ -631,11 +626,13 @@ mutual
" with " ++ show qtm)
case !(patternEnv env args) of
Nothing =>
do Just (Hole _ _ inv) <- lookupDefExact (Resolved mref) (gamma defs)
| _ => unifyPatVar mode loc env mname mref margs margs' tmnf
if inv
do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
| _ => postponePatVar mode loc env mname mref margs margs' tmnf
let Hole _ _ = definition hdef
| _ => postponePatVar mode loc env mname mref margs margs' tmnf
if invertible hdef
then unifyHoleApp mode loc env mname mref margs margs' tmnf
else unifyPatVar mode loc env mname mref margs margs' tmnf
else postponePatVar mode loc env mname mref margs margs' tmnf
Just (newvars ** (locs, submv)) =>
do tm <- quote empty env tmnf
case shrinkTerm tm submv of
@ -1015,12 +1012,13 @@ mutual
export
setInvertible : {auto c : Ref Ctxt Defs} ->
FC -> Int -> Core ()
setInvertible loc i
= updateDef (Resolved i)
(\old => case old of
Hole locs p _ => Just (Hole locs p True)
_ => Nothing)
FC -> Name -> Core ()
setInvertible fc n
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
addDef n (record { invertible = True } gdef)
pure ()
public export
data SolveMode = Normal -- during elaboration: unifies and searches
@ -1082,10 +1080,10 @@ retryGuess mode smode (hid, (loc, hname))
DeterminingArg _ n i _ _ =>
do logTerm 5 ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
(type def)
setInvertible loc i
setInvertible loc (Resolved i)
pure False -- progress made!
_ => do logTerm 5 ("Search failed for " ++ show hname)
(type def)
_ => do logTermNF 5 ("Search failed at " ++ show rig ++ " for " ++ show hname)
[] (type def)
case smode of
LastChance =>
throw !(normaliseErr err)
@ -1135,9 +1133,9 @@ giveUpConstraints
= do defs <- get Ctxt
case !(lookupDefExact (Resolved hid) (gamma defs)) of
Just (BySearch _ _ _) =>
updateDef (Resolved hid) (const (Just (Hole 0 False False)))
updateDef (Resolved hid) (const (Just (Hole 0 False)))
Just (Guess _ _) =>
updateDef (Resolved hid) (const (Just (Hole 0 False False)))
updateDef (Resolved hid) (const (Just (Hole 0 False)))
_ => pure ()
export
@ -1164,7 +1162,7 @@ checkDots
Just ndef <- lookupDefExact n (gamma defs)
| Nothing => throw (UndefinedName fc n)
let h = case ndef of
Hole _ _ _ => True
Hole _ _ => True
_ => False
when (not (isNil (constraints cs)) || holesSolved cs || h) $

4
src/Core/UnifyState.idr
View File

@ -600,11 +600,11 @@ dumpHole lvl hole
++ "\n\twhen"
traverse dumpConstraint constraints
pure ()
(Hole _ p inj, ty) =>
(Hole _ p, ty) =>
log lvl $ "?" ++ show (fullname gdef) ++ " : " ++
show !(normaliseHoles defs [] ty)
++ if p then " (ImplBind)" else ""
++ if inj then " (Invertible)" else ""
++ if invertible gdef then " (Invertible)" else ""
(BySearch _ _ _, ty) =>
log lvl $ "Search " ++ show hole ++ " : " ++
show !(toFullNames !(normaliseHoles defs [] ty))

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

@ -109,21 +109,22 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
-- which appear in other method types
let ty_constr = substNames vars (map applyCon allmeths) ty
ty_imp <- bindTypeNames vars (bindIFace fc ity ty_constr)
cn <- inCurrentNS n
let tydecl = IClaim fc c vis (if d then [Inline, Invertible]
else [Inline])
(MkImpTy fc n ty_imp)
(MkImpTy fc cn ty_imp)
let conapp = apply (IVar fc cname)
(map (const (Implicit fc True)) constraints ++
map (IBindVar fc) (map bindName allmeths))
let argns = getExplicitArgs 0 ty
-- eta expand the RHS so that we put implicits in the right place
let fnclause = PatClause fc (IImplicitApp fc (IVar fc n)
let fnclause = PatClause fc (IImplicitApp fc (IVar fc cn)
(Just (UN "__con"))
conapp)
(mkLam argns
(apply (IVar fc (methName n))
(map (IVar fc) argns)))
let fndef = IDef fc n [fnclause]
let fndef = IDef fc cn [fnclause]
pure [tydecl, fndef]
where
applyCon : Name -> (Name, RawImp)

181
src/Idris/IDEMode/Main.idr
View File

@ -1,181 +0,0 @@
module Main
import Core.Binary
import Core.Context
import Core.Core
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.Options
import Core.Unify
import Idris.CommandLine
import Idris.Desugar
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.Parser
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Socket
import Idris.Socket.Data
import Data.Vect
import System
import BlodwenPaths
%default covering
findInput : List CLOpt -> Maybe String
findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs
-- Add extra library directories from the "BLODWEN_PATH"
-- environment variable
updatePaths : {auto c : Ref Ctxt Defs} ->
Core ()
updatePaths
= do setPrefix bprefix
defs <- get Ctxt
bpath <- coreLift $ getEnv "BLODWEN_PATH"
case bpath of
Just path => do traverse addExtraDir (map trim (split (==':') path))
pure ()
Nothing => pure ()
bdata <- coreLift $ getEnv "BLODWEN_DATA"
case bdata of
Just path => do traverse addDataDir (map trim (split (==':') path))
pure ()
Nothing => pure ()
-- BLODWEN_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting BLODWEN_PATH
-- for the tests means they test the local version not the installed
-- version
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"blodwen" ++ dirSep ++ "support")
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()
updateREPLOpts
= do opts <- get ROpts
ed <- coreLift $ getEnv "EDITOR"
case ed of
Just e => put ROpts (record { editor = e } opts)
Nothing => pure ()
showInfo : {auto c : Ref Ctxt Defs}
-> {auto o : Ref ROpts REPLOpts}
-> List CLOpt
-> Core Bool
showInfo Nil = pure False
showInfo (BlodwenPaths :: _)
= do defs <- get Ctxt
iputStrLn (toString (dirs (options defs)))
pure True
showInfo (_::rest) = showInfo rest
stMain : List CLOpt -> Core ()
stMain opts
= do c <- newRef Ctxt initCtxt
s <- newRef Syn initSyntax
m <- newRef Meta initMetadata
addPrimitives
setWorkingDir "."
updatePaths
let ide = ideMode opts
let ideSocket = ideModeSocket opts
let outmode = if ide then IDEMode 0 stdin stdout else REPL False
let fname = findInput opts
o <- newRef ROpts (REPLOpts.defaultOpts fname outmode)
finish <- showInfo opts
if finish
then pure ()
else do
-- If there's a --build or --install, just do that then quit
done <- processPackageOpts opts
when (not done) $
do preOptions opts
u <- newRef UST initUState
updateREPLOpts
case fname of
Nothing => readPrelude
Just f => loadMainFile f
doRepl <- postOptions opts
if doRepl
then
if ide || ideSocket
then
if not ideSocket
then do
setOutput (IDEMode 0 stdin stdout)
replIDE {c} {u} {m}
else do
f <- coreLift $ initIDESocketFile 38398
case f of
Left err => do
coreLift $ putStrLn err
coreLift $ exit 1
Right file => do
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
iputStrLn "Welcome to Idris 2. Good luck."
repl {c} {u} {m}
else
-- exit with an error code if there was an error, otherwise
-- just exit
do ropts <- get ROpts
case errorLine ropts of
Nothing => pure ()
Just _ => coreLift $ exit 1
-- Run any options (such as --version or --help) which imply printing a
-- message then exiting. Returns wheter the program should continue
quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _)
= do putStrLn versionMsg
pure False
quitOpts (Help :: _)
= do putStrLn usage
pure False
quitOpts (ShowPrefix :: _)
= do putStrLn bprefix
pure False
quitOpts (_ :: opts) = quitOpts opts
main : IO ()
main = do Right opts <- getCmdOpts
| Left err =>
do putStrLn err
putStrLn usage
continue <- quitOpts opts
if continue
then
coreRun (stMain opts)
(\err : Error _ =>
do putStrLn ("Uncaught error: " ++ show err)
exit 1)
(\res => pure ())
else pure ()
locMain : List CLOpt -> IO ()
locMain opts = coreRun (stMain opts)
(\err : Error _ =>
do putStrLn ("Uncaught error: " ++ show err)
exit 1)
(\res => pure ())

13
src/Idris/Parser.idr
View File

@ -1151,13 +1151,16 @@ recordDecl fname indents
n <- name
params <- many (ifaceParam fname indents)
keyword "where"
dc <- option Nothing (do exactIdent "constructor"
n <- name
pure (Just n))
flds <- assert_total (blockAfter col (fieldDecl fname))
dcflds <- blockWithOptHeaderAfter col ctor (fieldDecl fname)
end <- location
pure (PRecord (MkFC fname start end)
vis n params dc (concat flds))
vis n params (fst dcflds) (concat (snd dcflds)))
where
ctor : IndentInfo -> Rule Name
ctor idt = do exactIdent "constructor"
n <- name
atEnd idt
pure n
claim : FileName -> IndentInfo -> Rule PDecl
claim fname indents

6
src/Idris/REPL.idr
View File

@ -66,7 +66,7 @@ showInfo (n, idx, d)
isHole : GlobalDef -> Maybe Nat
isHole def
= case definition def of
Hole locs _ _ => Just locs
Hole locs _ => Just locs
_ => Nothing
showCount : RigCount -> String
@ -295,7 +295,7 @@ processEdit (ExprSearch line name hints all)
syn <- get Syn
let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
case !(lookupDefName name (gamma defs)) of
[(n, nidx, Hole locs _ _)] =>
[(n, nidx, Hole locs _)] =>
do tms <- exprSearch replFC name []
defs <- get Ctxt
restms <- traverse (normaliseHoles defs []) tms
@ -338,7 +338,7 @@ processEdit (MakeLemma line name)
syn <- get Syn
let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
case !(lookupDefTyName name (gamma defs)) of
[(n, nidx, Hole locs _ _, ty)] =>
[(n, nidx, Hole locs _, ty)] =>
do (lty, lapp) <- makeLemma replFC name locs ty
pty <- pterm lty
papp <- pterm lapp

22
src/Parser/Support.idr
View File

@ -522,6 +522,28 @@ blockAfter mincol item
then pure []
else blockEntries (AtPos col) item
export
blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter {ty} mincol header item
= do symbol "{"
commit
hidt <- optional $ blockEntry AnyIndent header
restOfBlock hidt
<|> do col <- column
if col <= mincol
then pure (Nothing, [])
else do hidt <- optional $ blockEntry (AtPos col) header
ps <- blockEntries (AtPos col) item
pure (map fst hidt, ps)
where
restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
symbol "}"
pure (Just h, ps)
restOfBlock Nothing = do ps <- blockEntries AnyIndent item
symbol "}"
pure (Nothing, ps)
export
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
nonEmptyBlock item

2
src/TTImp/Elab.idr
View File

@ -66,7 +66,7 @@ normaliseHoleTypes
= case !(lookupCtxtExact (Resolved i) (gamma defs)) of
Just gdef =>
case definition gdef of
Hole _ _ _ => updateType defs i gdef
Hole _ _ => updateType defs i gdef
_ => pure ()
Nothing => pure ()

2
src/TTImp/Elab/Ambiguity.idr
View File

@ -349,7 +349,7 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
holeIn gam tm
= case getFn tm of
Meta _ _ idx _ =>
do Just (Hole _ _ _) <- lookupDefExact (Resolved idx) gam
do Just (Hole _ _) <- lookupDefExact (Resolved idx) gam
| _ => pure False
pure True
_ => pure False

2
src/TTImp/Elab/App.idr
View File

@ -320,7 +320,7 @@ mutual
pure ()
case elabMode elabinfo of
InLHS _ => -- reset hole and redo it with the unexpanded definition
do updateDef (Resolved idx) (const (Just (Hole 0 False False)))
do updateDef (Resolved idx) (const (Just (Hole 0 False)))
solveIfUndefined env metaval argv
pure ()
_ => pure ()

8
src/TTImp/Elab/Check.idr
View File

@ -303,7 +303,7 @@ metaVar : {auto c : Ref Ctxt Defs} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Term vars)
metaVar fc rig env n ty
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) False False) True
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) False) True
pure tm
export
@ -312,7 +312,7 @@ implBindVar : {auto c : Ref Ctxt Defs} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Term vars)
implBindVar fc rig env n ty
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) True False) True
= do (_, tm) <- newMeta fc rig env n ty (Hole (length env) True) True
pure tm
export
@ -321,7 +321,7 @@ metaVarI : {auto c : Ref Ctxt Defs} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
metaVarI fc rig env n ty
= newMeta fc rig env n ty (Hole (length env) False False) True
= newMeta fc rig env n ty (Hole (length env) False) True
export
argVar : {auto c : Ref Ctxt Defs} ->
@ -329,7 +329,7 @@ argVar : {auto c : Ref Ctxt Defs} ->
FC -> RigCount ->
Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
argVar fc rig env n ty
= newMetaLets fc rig env n ty (Hole (length env) False False) False True
= newMetaLets fc rig env n ty (Hole (length env) False) False True
export
searchVar : {auto c : Ref Ctxt Defs} ->

8
src/TTImp/Elab/ImplicitBind.idr
View File

@ -164,7 +164,7 @@ bindUnsolved {vars} fc elabmode _
(Env Term vars', Term vars', Term vars', SubVars outer vars'))) ->
Core ()
mkImplicit defs outerEnv subEnv (n, rig, p, (vs ** (env, tm, exp, sub)))
= do Just (Hole _ _ _) <- lookupDefExact n (gamma defs)
= do Just (Hole _ _) <- lookupDefExact n (gamma defs)
| _ => pure ()
bindtm <- makeBoundVar n rig p outerEnv
sub subEnv
@ -304,7 +304,7 @@ implicitBind : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
implicitBind n
= do defs <- get Ctxt
Just (Hole _ _ _) <- lookupDefExact n (gamma defs)
Just (Hole _ _) <- lookupDefExact n (gamma defs)
| _ => pure ()
updateDef n (const (Just ImpBind))
removeHoleName n
@ -430,6 +430,10 @@ checkBindVar rig elabinfo nest env fc str topexp
do (tm, exp, bty) <- mkPatternHole fc rig n env
(implicitMode elabinfo)
topexp
-- In PI mode, it's invertible like any other pi bound thing
case implicitMode elabinfo of
PI _ => setInvertible fc n
_ => pure ()
log 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
defs <- get Ctxt
est <- get EST

6
src/TTImp/Interactive/ExprSearch.idr
View File

@ -75,7 +75,7 @@ searchIfHole fc opts defining topty env arg
defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
| Nothing => pure []
let Hole _ _ inv = definition gdef
let Hole _ _ = definition gdef
| _ => pure [!(normaliseHoles defs env (metaApp arg))]
-- already solved
tms <- search fc rig (record { depth = k} opts)
@ -171,7 +171,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty defining all
defining
hn <- uniqueName defs (map nameRoot vars) base
(idx, tm) <- newMeta fc rig env (UN hn) ty
(Hole (length env) False False)
(Hole (length env) False)
False
pure [tm]
else if holesOK opts
@ -428,7 +428,7 @@ search fc rig opts defining topty n_in
-- The definition should be 'BySearch' at this stage,
-- if it's arising from an auto implicit
case definition gdef of
Hole locs _ _ => searchHole fc rig opts defining n locs topty defs gdef
Hole locs _ => searchHole fc rig opts defining n locs topty defs gdef
BySearch _ _ _ => searchHole fc rig opts defining n
!(getArity defs [] (type gdef))
topty defs gdef

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

@ -47,7 +47,7 @@ expandClause loc n c
let Meta _ i fn _ = getFn rhs
| _ => throw (GenericMsg loc "No searchable hole on RHS")
defs <- get Ctxt
Just (Hole locs _ _) <- lookupDefExact (Resolved fn) (gamma defs)
Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs)
| _ => throw (GenericMsg loc "No searchable hole on RHS")
log 10 $ "Expression search for " ++ show (i, fn)
(rhs' :: _) <- exprSearch loc (Resolved fn) []

4
src/TTImp/ProcessData.idr
View File

@ -160,7 +160,9 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
TCon _ _ _ _ mw _ =>
do ok <- convert defs [] fullty (type ndef)
if ok then pure mw
else throw (AlreadyDefined fc n)
else do logTermNF 1 "Previous" [] (type ndef)
logTermNF 1 "Now" [] fullty
throw (AlreadyDefined fc n)
_ => throw (AlreadyDefined fc n)
logTermNF 5 ("data " ++ show n) [] fullty

8
src/TTImp/ProcessRecord.idr
View File

@ -73,10 +73,6 @@ elabRecord {vars} eopts fc env nest vis tn params rcon fields
log 5 $ "Record data type " ++ show dt
processDecl [] nest env (IData fc vis dt)
impName : Name -> Name
impName (UN n) = UN ("imp_" ++ n)
impName n = n
countExp : Term vs -> Nat
countExp (Bind _ n (Pi c Explicit _) sc) = S (countExp sc)
countExp (Bind _ n (Pi c _ _) sc) = countExp sc
@ -97,9 +93,7 @@ elabRecord {vars} eopts fc env nest vis tn params rcon fields
then S done else done)
upds (b :: tyenv) sc
else
do let fldName = case imp of
Explicit => n
_ => impName n
do let fldName = n
gname <- inCurrentNS fldName
ty <- unelab tyenv ty_chk
let ty' = substNames vars upds ty

2
src/TTImp/ProcessType.idr
View File

@ -74,7 +74,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
checkTerm idx InType (HolesOkay :: eopts) nest env
(IBindHere fc (PI Rig0) ty_raw)
(gType fc)
logTermNF 5 (show n) [] (abstractEnvType tfc env ty)
logTermNF 5 ("Type of " ++ show n) [] (abstractEnvType tfc env ty)
-- TODO: Check name visibility
-- If it's declared as externally defined, set the definition to
-- ExternFn <arity>, where the arity is assumed to be fixed (i.e.

52
src/TTImp/TTImp.idr
View File

@ -397,15 +397,14 @@ findImplicits tm = []
-- rhs
export
implicitsAs : Defs -> List Name -> RawImp -> Core RawImp
implicitsAs defs ns tm = setAs (ns ++ map UN (findIBinds tm)) tm
implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
where
setAs : List Name -> RawImp -> Core RawImp
setAs : List (Maybe Name) -> RawImp -> Core RawImp
setAs is (IApp loc f a)
= do f' <- setAs is f
pure $ IApp loc f' a
setAs is (IImplicitApp loc f n a)
= do let is' = maybe is (\n' => n' :: is) n
f' <- setAs is' f
= do f' <- setAs (n :: is) f
pure $ IImplicitApp loc f' n a
setAs is (IWithApp loc f a)
= do f' <- setAs is f
@ -413,23 +412,46 @@ implicitsAs defs ns tm = setAs (ns ++ map UN (findIBinds tm)) tm
setAs is (IVar loc n)
= case !(lookupTyExact n (gamma defs)) of
Nothing => pure $ IVar loc n
Just ty => pure $ impAs loc (filter (\x => not (x `elem` is))
!(findImps !(nf defs [] ty))) (IVar loc n)
Just ty => pure $ impAs loc
!(findImps is !(nf defs [] ty)) (IVar loc n)
where
findImps : NF [] -> Core (List Name)
findImps (NBind fc x (Pi _ Implicit _) sc)
= pure $
x :: !(findImps !(sc defs (toClosure defaultOpts [] (Erased fc))))
findImps (NBind fc x (Pi _ _ _) sc)
= findImps !(sc defs (toClosure defaultOpts [] (Erased fc)))
findImps _ = pure []
-- If there's an @{c} in the list of given implicits, that's the next
-- autoimplicit, so don't rewrite the LHS and update the list of given
-- implicits
updateNs : Name -> List (Maybe Name) -> Maybe (List (Maybe Name))
updateNs n (Nothing :: ns) = Just ns
updateNs n (x :: ns)
= if Just n == x
then Just ns -- found it
else do ns' <- updateNs n ns
pure (x :: ns')
updateNs n [] = Nothing
impAs : FC -> List Name -> RawImp -> RawImp
findImps : List (Maybe Name) -> NF [] -> Core (List (Name, PiInfo))
findImps ns (NBind fc x (Pi _ Explicit _) sc)
= findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc)))
-- if the implicit was given, skip it
findImps ns (NBind fc x (Pi _ AutoImplicit _) sc)
= case updateNs x ns of
Nothing => -- didn't find explicit call
pure $ (x, AutoImplicit) :: !(findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc))))
Just ns' => findImps ns' !(sc defs (toClosure defaultOpts [] (Erased fc)))
findImps ns (NBind fc x (Pi _ p _) sc)
= if Just x `elem` ns
then findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc)))
else pure $ (x, p) :: !(findImps ns !(sc defs (toClosure defaultOpts [] (Erased fc))))
findImps _ _ = pure []
impAs : FC -> List (Name, PiInfo) -> RawImp -> RawImp
impAs loc' [] tm = tm
impAs loc' (n :: ns) tm
impAs loc' ((UN n, AutoImplicit) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just (UN n)) (IBindVar loc' n)
impAs loc' ((n, Implicit) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just n)
(IAs loc' UseLeft n (Implicit loc' True))
impAs loc' (_ :: ns) tm = impAs loc' ns tm
setAs is tm = pure tm
export

4
tests/Main.idr
View File

@ -28,7 +28,7 @@ idrisTests
"basic011", "basic012", "basic013", "basic014", "basic015",
"basic016", "basic017", "basic018", "basic019", "basic020",
"basic021", "basic022", "basic023", "basic024", "basic025",
"basic026",
"basic026", "basic027",
"coverage001", "coverage002", "coverage003", "coverage004",
"error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009",
@ -38,7 +38,7 @@ idrisTests
"interactive009", "interactive010", "interactive011", "interactive012",
"interface001", "interface002", "interface003", "interface004",
"interface005", "interface006", "interface007", "interface008",
"interface009",
"interface009", "interface010", "interface011",
"lazy001",
"linear001", "linear002", "linear003", "linear004", "linear005",
"linear006", "linear007",

15
tests/idris2/basic027/Temp.idr Normal file
View File

@ -0,0 +1,15 @@
module Temp
import Data.List
safeHead : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead [] = absurd pr
safeHead (x::xs) = x
safeHead1 : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead1 @{pr} [] = absurd pr
safeHead1 (x::xs) = x
safeHead2 : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead2 @{t} [] = absurd t
safeHead2 (x::xs) = x

1
tests/idris2/basic027/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Temp (Temp.idr)

3
tests/idris2/basic027/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check Temp.idr
rm -rf build

7
tests/idris2/interface010/Dep.idr Normal file
View File

@ -0,0 +1,7 @@
module Dep
interface Monad m => FooBar m where
Foo : {0 a : Type} -> a -> m a -> Type
Bar : {0 A : Type} -> m A -> Type
foo : {0 A : Type} -> (x : A) -> (ma : m A) -> Foo x ma -> Bar ma

1
tests/idris2/interface010/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Dep (Dep.idr)

3
tests/idris2/interface010/run Executable file
View File

@ -0,0 +1,3 @@
$1 Dep.idr --check
rm -rf build

8
tests/idris2/interface011/FuncImpl.idr Normal file
View File

@ -0,0 +1,8 @@
module FuncImpl
public export
interface Monad m => FooBar m where
Foo : {A : Type} -> A -> m A -> Type
bar : {A : Type} -> (ma : m A) -> m (DPair A (\ a => Foo a ma))
foobar : {A : Type} -> (ma : m A) -> map DPair.fst (bar ma) = ma

1
tests/idris2/interface011/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building FuncImpl (FuncImpl.idr)

3
tests/idris2/interface011/run Executable file
View File

@ -0,0 +1,3 @@
$1 FuncImpl.idr --check
rm -rf build