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

Fix reflection of PiInfo

Browse Source 
It needs to account for the implicit parameter
This commit is contained in:
Edwin Brady 2020-06-02 12:10:57 +01:00
parent 8e788658c4
commit e7f8e2df8c
1 changed files with 8 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Core/Reflect.idr
View File

@ -444,7 +444,7 @@ Reify t => Reify (PiInfo t) where
(NS _ (UN "ImplicitArg"), _) => pure Implicit (NS _ (UN "ImplicitArg"), _) => pure Implicit
(NS _ (UN "ExplicitArg"), _) => pure Explicit (NS _ (UN "ExplicitArg"), _) => pure Explicit
(NS _ (UN "AutoImplicit"), _) => pure AutoImplicit (NS _ (UN "AutoImplicit"), _) => pure AutoImplicit
(NS _ (UN "DefImplicit"), [t]) (NS _ (UN "DefImplicit"), [_, t])
=> do t' <- reify defs !(evalClosure defs t) => do t' <- reify defs !(evalClosure defs t)
pure (DefImplicit t') pure (DefImplicit t')
_ => cantReify val "PiInfo" _ => cantReify val "PiInfo"
@ -452,12 +452,15 @@ Reify t => Reify (PiInfo t) where
export export
Reflect t => Reflect (PiInfo t) where Reflect t => Reflect (PiInfo t) where
reflect fc defs env Implicit = getCon fc defs (reflectiontt "ImplicitArg") reflect fc defs env Implicit
reflect fc defs env Explicit = getCon fc defs (reflectiontt "ExplicitArg") = appCon fc defs (reflectiontt "ImplicitArg") [Erased fc False]
reflect fc defs env AutoImplicit = getCon fc defs (reflectiontt "AutoImplicit") reflect fc defs env Explicit
= appCon fc defs (reflectiontt "ExplicitArg") [Erased fc False]
reflect fc defs env AutoImplicit
= appCon fc defs (reflectiontt "AutoImplicit") [Erased fc False]
reflect fc defs env (DefImplicit t) reflect fc defs env (DefImplicit t)
= do t' <- reflect fc defs env t = do t' <- reflect fc defs env t
appCon fc defs (reflectiontt "DefImplicit") [t'] appCon fc defs (reflectiontt "DefImplicit") [Erased fc False, t']
export export
Reify LazyReason where Reify LazyReason where