idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #834 ] Fix implicitsAs for local definitions (#1199)

Browse Source
This commit is contained in:
G. Allais 2021-03-17 10:54:25 +00:00 committed by GitHub
parent 8f71aae705
commit f959987a51
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
12 changed files with 141 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Idris/IDEMode/Holes.idr
View File

@ -81,6 +81,7 @@ extractHoleData defs env fn (S args) (Bind fc x b sc)
let True = showName x
| False => do log "idemode.hole" 10 $ "Not showing name: " ++ show x
pure rest
log "idemode.hole" 10 $ "Showing name: " ++ show x
ity <- resugar env !(normalise defs env (binderType b))
let premise = MkHolePremise x ity (multiplicity b) (isImplicit b)
pure $ record { context $= (premise ::) } rest

2
src/TTImp/BindImplicits.idr
View File

@ -1,6 +1,7 @@
module TTImp.BindImplicits
import Core.Context
import Core.Context.Log
import Core.Core
import Core.TT
import TTImp.TTImp
@ -118,6 +119,7 @@ bindNames : {auto c : Ref Ctxt Defs} ->
bindNames arg tm
= if !isUnboundImplicits
then do let ns = nub (findBindableNames arg [] [] tm)
log "elab.bindnames" 10 $ "Found names :" ++ show ns
pure (map UN (map snd ns), doBind ns tm)
else pure ([], tm)

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

@ -47,7 +47,7 @@ mkOuterHole loc rig n topenv Nothing
let env = outerEnv est
nm <- genName ("type_of_" ++ nameRoot n)
ty <- metaVar loc erased env nm (TType loc)
log "elab" 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm
log "elab.implicits" 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm
put EST (addBindIfUnsolved nm rig Explicit topenv (embedSub sub ty) (TType loc) est)
tm <- implBindVar loc rig env n ty
pure (embedSub sub tm, embedSub sub ty)
@ -114,7 +114,7 @@ bindUnsolved {vars} fc elabmode _
= do est <- get EST
defs <- get Ctxt
let bifs = bindIfUnsolved est
log "elab" 5 $ "Bindable unsolved implicits: " ++ show (map fst bifs)
log "elab.implicits" 5 $ "Bindable unsolved implicits: " ++ show (map fst bifs)
traverse_ (mkImplicit defs (outerEnv est) (subEnv est)) (bindIfUnsolved est)
where
makeBoundVar : {outer, vs : _} ->
@ -146,7 +146,7 @@ bindUnsolved {vars} fc elabmode _
bindtm <- makeBoundVar n rig p outerEnv
sub subEnv
!(normaliseHoles defs env exp)
logTerm "elab" 5 ("Added unbound implicit") bindtm
logTerm "elab.implicits" 5 ("Added unbound implicit") bindtm
ignore $ unify (case elabmode of
InLHS _ => inLHS
_ => inTerm)
@ -331,8 +331,8 @@ getToBind {vars} fc elabmode impmode env excepts
let hnames = map fst res
-- Return then in dependency order
let res' = depSort hnames res
log "elab" 10 $ "Bound names: " ++ show res
log "elab" 10 $ "Sorted: " ++ show res'
log "elab.implicits" 10 $ "Bound names: " ++ show res
log "elab.implicits" 10 $ "Sorted: " ++ show res'
pure res'
where
normBindingTy : Defs -> ImplBinding vars -> Core (ImplBinding vars)
@ -346,7 +346,7 @@ getToBind {vars} fc elabmode impmode env excepts
Core (List (Name, ImplBinding vars))
normImps defs ns [] = pure []
normImps defs ns ((PV n i, bty) :: ts)
= do logTermNF "elab" 10 ("Implicit pattern var " ++ show (PV n i)) env
= do logTermNF "elab.implicits" 10 ("Implicit pattern var " ++ show (PV n i)) env
(bindingType bty)
if PV n i `elem` ns
then normImps defs ns ts
@ -354,7 +354,7 @@ getToBind {vars} fc elabmode impmode env excepts
pure ((PV n i, !(normBindingTy defs bty)) :: rest)
normImps defs ns ((n, bty) :: ts)
= do tmnf <- normaliseHoles defs env (bindingTerm bty)
logTerm "elab" 10 ("Normalising implicit " ++ show n) tmnf
logTerm "elab.implicits" 10 ("Normalising implicit " ++ show n) tmnf
case getFnArgs tmnf of
-- n reduces to another hole, n', so treat it as that as long
-- as it isn't already done
@ -425,7 +425,7 @@ checkBindVar rig elabinfo nest env fc str topexp
case implicitMode elabinfo of
PI _ => setInvertible fc n
_ => pure ()
log "elab" 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
log "elab.implicits" 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
est <- get EST
put EST (record { boundNames $= ((n, NameBinding rig Explicit tm exp) ::),
toBind $= ((n, NameBinding rig Explicit tm bty) :: ) } est)
@ -506,8 +506,8 @@ checkBindHere rig elabinfo nest env fc bindmode tm exp
checkDots -- Check dot patterns unifying with the claimed thing
-- before binding names
logTerm "elab" 5 "Binding names" tmv
logTermNF "elab" 5 "Normalised" env tmv
logTerm "elab.implicits" 5 "Binding names" tmv
logTermNF "elab.implicits" 5 "Normalised" env tmv
argImps <- getToBind fc (elabMode elabinfo)
bindmode env dontbind
clearToBind dontbind

7
src/TTImp/Elab/Local.idr
View File

@ -42,6 +42,7 @@ localHelper {vars} nest env nestdecls_in func
if vis == Public
then map setPublic nestdecls_in
else nestdecls_in
let defNames = definedInBlock emptyNS nestdecls
names' <- traverse (applyEnv f)
(nub defNames) -- binding names must be unique
@ -58,7 +59,11 @@ localHelper {vars} nest env nestdecls_in func
-- store the local hints, so we can reset them after we've elaborated
-- everything
let oldhints = localHints defs
traverse_ (processDecl [] nest' env') (map (updateName nest') nestdecls)
let nestdecls = map (updateName nest') nestdecls
log "elab.def.local" 20 $ show nestdecls
traverse_ (processDecl [] nest' env') nestdecls
ust <- get UST
put UST (record { delayedElab = olddelayed } ust)
defs <- get Ctxt

7
src/TTImp/ProcessDef.idr
View File

@ -318,16 +318,21 @@ checkLHS : {vars : _} ->
Term vars', Term vars')))
checkLHS {vars} trans mult hashit n opts nest env fc lhs_in
= do defs <- get Ctxt
logRaw "declare.def.lhs" 30 "Raw LHS: " lhs_in
lhs_raw <- if trans
then pure lhs_in
else lhsInCurrentNS nest lhs_in
logRaw "declare.def.lhs" 30 "Raw LHS in current NS: " lhs_raw
autoimp <- isUnboundImplicits
setUnboundImplicits True
(_, lhs_bound) <- bindNames False lhs_raw
setUnboundImplicits autoimp
logRaw "declare.def.lhs" 30 "Raw LHS with implicits bound" lhs_bound
lhs <- if trans
then pure lhs_bound
else implicitsAs defs vars lhs_bound
else implicitsAs n defs vars lhs_bound
logC "declare.def.lhs" 5 $ do pure $ "Checking LHS of " ++ show !(getFullName (Resolved n))
-- todo: add Pretty RawImp instance

76
src/TTImp/TTImp.idr
View File

@ -2,6 +2,7 @@ module TTImp.TTImp
import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Normalise
import Core.Options
@ -495,8 +496,13 @@ findImplicits tm = []
-- rhs
export
implicitsAs : {auto c : Ref Ctxt Defs} ->
Defs -> List Name -> RawImp -> Core RawImp
implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) [] tm
Int -> Defs ->
(vars : List Name) ->
RawImp -> Core RawImp
implicitsAs n defs ns tm
= do let implicits = findIBinds tm
log "declare.def.lhs.implicits" 30 $ "Found implicits: " ++ show implicits
setAs (map Just (ns ++ map UN implicits)) [] tm
where
-- Takes the function application expression which is the lhs of a clause
-- and decomposes it into the underlying function symbol and the variables
@ -516,11 +522,21 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) [] tm
setAs is es (IWithApp loc f a)
= do f' <- setAs is es f
pure $ IWithApp loc f' a
setAs is es (IVar loc n)
= case !(lookupTyExact n (gamma defs)) of
Nothing => pure $ IVar loc n
Just ty => pure $ impAs loc
!(findImps is es !(nf defs [] ty)) (IVar loc n)
setAs is es (IVar loc nm)
-- #834 Use the (already) resolved name rather than the local one
= case !(lookupTyExact (Resolved n) (gamma defs)) of
Nothing =>
do log "declare.def.lhs.implicits" 30 $
"Could not find variable " ++ show n
pure $ IVar loc nm
Just ty =>
do ty' <- nf defs [] ty
implicits <- findImps is es ns ty'
log "declare.def.lhs.implicits" 30 $
"\n In the type of " ++ show n ++ ": " ++ show ty ++
"\n Using locals: " ++ show ns ++
"\n Found implicits: " ++ show implicits
pure $ impAs loc implicits (IVar loc nm)
where
-- 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
@ -542,27 +558,43 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) [] tm
-- The second argument, `es`, specifies which *explicit* variables appear
-- in the lhs: this is used to determine when to stop searching for further
-- implicits to add.
findImps : List (Maybe Name) -> List (Maybe Name) -> NF [] -> Core (List (Name, PiInfo RawImp))
findImps : List (Maybe Name) -> List (Maybe Name) ->
List Name -> NF [] ->
Core (List (Name, PiInfo RawImp))
-- #834 When we are in a local definition, we have an explicit telescope
-- corresponding to the variables bound in the parent function.
-- So we first peel off all of the explicit quantifiers corresponding
-- to these variables.
findImps ns es (_ :: locals) (NBind fc x (Pi _ _ Explicit _) sc)
= do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
findImps ns es locals body
-- ^ TODO? check that name of the pi matches name of local?
-- don't add implicits coming after explicits that aren't given
findImps ns es (NBind fc x (Pi _ _ Explicit _) sc)
= case es of
findImps ns es [] (NBind fc x (Pi _ _ Explicit _) sc)
= do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
case es of
-- Explicits were skipped, therefore all explicits are given anyway
Just (UN "_") :: _ => findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False)))
Just (UN "_") :: _ => findImps ns es [] body
-- Explicits weren't skipped, so we need to check
_ => case updateNs x es of
Nothing => pure [] -- explicit wasn't given
Just es' => findImps ns es' !(sc defs (toClosure defaultOpts [] (Erased fc False)))
Nothing => pure [] -- explicit wasn't given
Just es' => findImps ns es' [] body
-- if the implicit was given, skip it
findImps ns es (NBind fc x (Pi _ _ AutoImplicit _) sc)
= case updateNs x ns of
findImps ns es [] (NBind fc x (Pi _ _ AutoImplicit _) sc)
= do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
case updateNs x ns of
Nothing => -- didn't find explicit call
pure $ (x, AutoImplicit) :: !(findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False))))
Just ns' => findImps ns' es !(sc defs (toClosure defaultOpts [] (Erased fc False)))
findImps ns es (NBind fc x (Pi _ _ p _) sc)
= if Just x `elem` ns
then findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False)))
else pure $ (x, forgetDef p) :: !(findImps ns es !(sc defs (toClosure defaultOpts [] (Erased fc False))))
findImps _ _ _ = pure []
pure $ (x, AutoImplicit) :: !(findImps ns es [] body)
Just ns' => findImps ns' es [] body
findImps ns es [] (NBind fc x (Pi _ _ p _) sc)
= do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
if Just x `elem` ns
then findImps ns es [] body
else pure $ (x, forgetDef p) :: !(findImps ns es [] body)
findImps _ _ locals _
= do log "declare.def.lhs.implicits" 50 $
"Giving up with the following locals left: " ++ show locals
pure []
impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp
impAs loc' [] tm = tm

3
tests/Main.idr
View File

@ -81,7 +81,8 @@ idrisTestsInteractive = MkTestPool []
"interactive013", "interactive014", "interactive015", "interactive016",
"interactive017", "interactive018", "interactive019", "interactive020",
"interactive021", "interactive022", "interactive023", "interactive024",
"interactive025", "interactive026", "interactive027", "interactive028"]
"interactive025", "interactive026", "interactive027", "interactive028",
"interactive029"]
idrisTestsInterface : TestPool
idrisTestsInterface = MkTestPool []

1
tests/idris2/interactive020/expected
View File

@ -3,6 +3,7 @@ Issue835> P : Nat -> Type
------------------------------
rhs1 : Dec (P 0)
Issue835> P : Nat -> Type
P2 : Nat -> Type
x1 : Nat
x : Nat
------------------------------

17
tests/idris2/interactive029/Issue834.idr Normal file
View File

@ -0,0 +1,17 @@
foo : {p,q : Nat -> Type} -> p x
foo = ?a
where
helper : {p2 : Nat -> Nat -> Type} -> p2 y 0
helper = ?b
helper1 : {p2 : Nat -> Nat -> Type} -> (y : Nat) -> p2 y 0
helper1 = ?c
helper2 : (y : Nat) -> {p2 : Nat -> Nat -> Type} -> p2 y 0
helper2 = ?d
-- introduce the ones after explicitly bound variables though
helper3 : (y : Nat) -> {p2 : Nat -> Nat -> Type} -> p2 y 0
helper3 y = ?e

33
tests/idris2/interactive029/expected Normal file
View File

@ -0,0 +1,33 @@
1/1: Building Issue834 (Issue834.idr)
Main> 0 x : Nat
p : Nat -> Type
q : Nat -> Type
------------------------------
a : p x
Main> 0 x : Nat
p : Nat -> Type
q : Nat -> Type
0 y : Nat
p2 : Nat -> Nat -> Type
------------------------------
b : p2 y 0
Main> 0 x : Nat
p : Nat -> Type
q : Nat -> Type
p2 : Nat -> Nat -> Type
------------------------------
c : (y : Nat) -> p2 y 0
Main> 0 x : Nat
p : Nat -> Type
q : Nat -> Type
------------------------------
d : (y : Nat) -> {p2 : Nat -> Nat -> Type} -> p2 y 0
Main> 0 x : Nat
p : Nat -> Type
q : Nat -> Type
p2 : Nat -> Nat -> Type
y : Nat
------------------------------
e : p2 y 0
Main>
Bye for now!

6
tests/idris2/interactive029/input Normal file
View File

@ -0,0 +1,6 @@
:t a
:t b
:t c
:t d
:t e
:q

3
tests/idris2/interactive029/run Normal file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner Issue834.idr < input
rm -rf build