git.iko.soy/Idris-dev
on master help sign in
Some fixes for adding declarations in wheres
c1de41cEdwin Brady
src/Idris/ElabDecls.hs+11−2
compare with master
unifiedsplit
@@ -77,8 +77,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
77 let nty' = normalise ctxt [] nty
77 let nty' = normalise ctxt [] nty
78
78
79 -- Add normalised type to internals
79 -- Add normalised type to internals
80− addInternalApp (fc_fname fc) (fc_line fc) (delab i nty')
80+ addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))
81− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i nty'))
81+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))
82
82
83 let (t, _) = unApply (getRetTy nty')
83 let (t, _) = unApply (getRetTy nty')
84 let corec = case t of
84 let corec = case t of
@@ -98,6 +98,15 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
98 addIBC (IBCCoercion n)
98 addIBC (IBCCoercion n)
99 when corec $ do setAccessibility n Frozen
99 when corec $ do setAccessibility n Frozen
100 addIBC (IBCAccess n Frozen)
100 addIBC (IBCAccess n Frozen)
101+ where
102+ -- for making an internalapp, we only want the explicit ones, and don't
103+ -- want the parameters, so just take the arguments which correspond to the
104+ -- user declared explicit ones
105+ mergeTy (PPi e n ty sc) (PPi e' _ _ sc')
106+ | e == e' = PPi e n ty (mergeTy sc sc')
107+ | otherwise = mergeTy sc sc'
108+ mergeTy _ sc = sc
109+
101
110
102elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
111elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
103 FC -> FnOpts -> Name -> PTerm -> Idris ()
112 FC -> FnOpts -> Name -> PTerm -> Idris ()
src/Idris/REPL.hs+12−5
@@ -590,12 +590,14 @@ process h fn (AddProofClauseFrom updatefile l n)
590process h fn (AddMissing updatefile l n)
590process h fn (AddMissing updatefile l n)
591 = do src <- runIO $ readFile fn
591 = do src <- runIO $ readFile fn
592 let (before, tyline : later) = splitAt (l-1) (lines src)
592 let (before, tyline : later) = splitAt (l-1) (lines src)
593+ let indent = getIndent 0 (show n) tyline
593 i <- getIState
594 i <- getIState
594 cl <- getInternalApp fn l
595 cl <- getInternalApp fn l
595 let n' = getAppName cl
596 let n' = getAppName cl
597+
596 extras <- case lookupCtxt n' (idris_patdefs i) of
598 extras <- case lookupCtxt n' (idris_patdefs i) of
597 [] -> return ""
599 [] -> return ""
598− [(_, tms)] -> showNew (show n ++ "_rhs") 1 tms
600+ [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms
599 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
601 let (nonblank, rest) = span (not . all isSpace) (tyline:later)
600 if updatefile then
602 if updatefile then
601 do let fb = fn ++ "~"
603 do let fb = fn ++ "~"
@@ -616,12 +618,17 @@ process h fn (AddMissing updatefile l n)
616 getAppName (PRef _ r) = r
618 getAppName (PRef _ r) = r
617 getAppName _ = n
619 getAppName _ = n
618
620
619− showNew nm i (tm : tms)
621+ showNew nm i ind (tm : tms)
620 = do (nm', i') <- getUniq nm i
622 = do (nm', i') <- getUniq nm i
621− rest <- showNew nm i' tms
623+ rest <- showNew nm i' ind tms
624+ return (replicate ind ' ' ++
622− return (showPat tm ++ " = ?" ++ nm' ++
625+ showPat tm ++ " = ?" ++ nm' ++
623 "\n" ++ rest)
626 "\n" ++ rest)
624− showNew nm i [] = return ""
627+ showNew nm i _ [] = return ""
628+
629+ getIndent i n [] = 0
630+ getIndent i n xs | take (length n) xs == n = i
631+ getIndent i n (x : xs) = getIndent (i + 1) n xs
625
632
626process h fn (MakeWith updatefile l n)
633process h fn (MakeWith updatefile l n)
627 = do src <- runIO $ readFile fn
634 = do src <- runIO $ readFile fn