edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-29 15:52:29 +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 2019-12-27 09:25:55 +01:00
commit c385a2a9cc
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/TTImp/Elab/Term.idr
View File

@ -44,11 +44,18 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamTm : RawImp -> Term vs -> Core (Maybe RawImp)
bindLamTm tm@(ILam _ _ Implicit _ _ _) (Bind fc n (Pi _ Implicit _) sc)
= pure (Just tm)
bindLamTm tm@(ILam _ _ AutoImplicit _ _ _) (Bind fc n (Pi _ AutoImplicit _) sc)
= pure (Just tm)
bindLamTm tm (Bind fc n (Pi c Implicit ty) sc)
= do n' <- genVarName (nameRoot n)
Just sc' <- bindLamTm tm sc
| Nothing => pure Nothing
pure $ Just (ILam fc c Implicit (Just n') (Implicit fc False) sc')
bindLamTm tm (Bind fc n (Pi c AutoImplicit ty) sc)
= do n' <- genVarName (nameRoot n)
Just sc' <- bindLamTm tm sc
| Nothing => pure Nothing
pure $ Just (ILam fc c AutoImplicit (Just n') (Implicit fc False) sc')
bindLamTm tm exp
= case getFn exp of
Ref _ Func _ => pure Nothing -- might still be implicit
@ -59,12 +66,20 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamNF : RawImp -> NF vars -> Core RawImp
bindLamNF tm@(ILam _ _ Implicit _ _ _) (NBind fc n (Pi _ Implicit _) sc)
= pure tm
bindLamNF tm@(ILam _ _ AutoImplicit _ _ _) (NBind fc n (Pi _ AutoImplicit _) sc)
= pure tm
bindLamNF tm (NBind fc n (Pi c Implicit ty) sc)
= do defs <- get Ctxt
n' <- genVarName (nameRoot n)
sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
sc' <- bindLamNF tm sctm
pure $ ILam fc c Implicit (Just n') (Implicit fc False) sc'
bindLamNF tm (NBind fc n (Pi c AutoImplicit ty) sc)
= do defs <- get Ctxt
n' <- genVarName (nameRoot n)
sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))
sc' <- bindLamNF tm sctm
pure $ ILam fc c AutoImplicit (Just n') (Implicit fc False) sc'
bindLamNF tm sc = pure tm
bindLam : RawImp -> Glued vars -> Core RawImp