c1968ed · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix parameter spotting in function types

We were only looking in the return type, not the argument types. Fixes #1391

commitc1968edd068c73f1135ac6e32f03a4b56e68182c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jul 2014, 17:11 (12 years ago) parentadb59d0

4 files changed+33−18

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4−1 src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/Core/TT.hs+1−1 src/Idris/ElabDecls.hs+25−13

src/Idris/AbsSyntax.hs+4−1

@@ -482,7 +482,10 @@ addDeferred' nt ns

482482 i <- getIState

483483 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

484484 idris_metavars i }

485− where tidyNames used (Bind (MN i x) b sc)

485+ where

486+ -- 'tidyNames' is to generate user accessible names in case they are

487+ -- needed in tactic scripts

488+ tidyNames used (Bind (MN i x) b sc)

486489 = let n' = uniqueName (UN x) used in

487490 Bind n' b $ tidyNames (n':used) sc

488491 tidyNames used (Bind n b sc)

src/Idris/AbsSyntaxTree.hs+3−3

@@ -1130,7 +1130,7 @@ instance Show PTerm where

11301130 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm

11311131

11321132instance Show PDecl where

1133− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d

1133+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d

11341134

11351135instance Show PClause where

11361136 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c

@@ -1466,7 +1466,7 @@ prettyName infixParen showNS bnd n

14661466 where fullName = text nameSpace <> parenthesise (text (baseName n))

14671467 baseName (UN n) = T.unpack n

14681468 baseName (NS n ns) = baseName n

1469− baseName (MN i s) = T.unpack s

1469+ baseName (MN i s) = T.unpack s

14701470 baseName n | n == falseTy = "_|_"

14711471 baseName other = show other

14721472 nameSpace = case n of

@@ -1556,7 +1556,7 @@ showName ist bnd ppo colour n = case ist of

15561556 Nothing -> showbasic n

15571557 where name = if ppopt_impl ppo then show n else showbasic n

15581558 showbasic n@(UN _) = showCG n

1559− showbasic (MN _ s) = str s

1559+ showbasic (MN i s) = str s

15601560 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

15611561 showbasic (SN s) = show s

15621562 fst3 (x, _, _) = x

src/Idris/Core/TT.hs+1−1

@@ -384,7 +384,7 @@ tcname _ = False

384384

385385implicitable (NS n _) = implicitable n

386386implicitable (UN xs) | T.null xs = False

387− | otherwise = isLower (T.head xs)

387+ | otherwise = isLower (T.head xs) || T.head xs == '_'

388388implicitable (MN _ x) = not (tnull x) && thead x /= '_'

389389implicitable _ = False

390390

src/Idris/ElabDecls.hs+25−13

@@ -136,11 +136,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

136136 (cty, ty, inacc) <- buildType info syn fc opts n ty'

137137

138138 addStatics n cty ty

139− logLvl 2 $ "Rechecked to " ++ show cty

140139 let nty = cty -- normalise ctxt [] cty

141140 -- if the return type is something coinductive, freeze the definition

142141 ctxt <- getContext

143142 let nty' = normalise ctxt [] nty

143+ logLvl 2 $ "Rechecked to " ++ show nty'

144144

145145 -- Add normalised type to internals

146146 i <- getIState

@@ -863,14 +863,18 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

863863 _ -> ifail "Something went inexplicably wrong"

864864 cimp <- case lookupCtxt cn (idris_implicits i) of

865865 [imps] -> return imps

866− let ptys = getProjs [] (renameBs cimp cty)

866+ ppos <- case lookupCtxt tyn (idris_datatypes i) of

867+ [ti] -> return $ param_pos ti

868+ let cty_imp = renameBs cimp cty

869+ let ptys = getProjs [] cty_imp

867870 let ptys_u = getProjs [] cty

868− let recty = getRecTy cty

871+ let recty = getRecTy cty_imp

872+ let recty_u = getRecTy cty

869873

870874 -- rename indices when we generate the getter/setter types, so

871875 -- that they don't clash with the names of the projections

872876 -- we're generating

873− let index_names_in = getRecNameMap "_in" recty

877+ let index_names_in = getRecNameMap "_in" ppos recty

874878 let recty_in = substMatches index_names_in recty

875879

876880 logLvl 1 $ show (recty, ptys)

@@ -884,7 +888,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

884888 let implBinds = getImplB id cty'

885889

886890 -- Generate update functions

887− update_decls <- mapM (mkUpdate recty index_names_in extraImpls

891+ update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls

888892 (getFieldNames cty')

889893 implBinds (length nonImp)) (zip nonImp [0..])

890894 mapM_ (elabDecl EAll info) (concat proj_decls)

@@ -932,15 +936,21 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

932936 getRecTy (PPi _ n ty s) = getRecTy s

933937 getRecTy t = t

934938

935− getRecNameMap x (PApp fc t args) = mapMaybe (toMN . getTm) args

939+ -- make sure we pick a consistent name for parameters; any name will do

940+ -- otherwise

941+ getRecNameMap x ppos (PApp fc t args)

942+ = mapMaybe toMN (zip [0..] (map getTm args))

936943 where

937− toMN (PRef fc n) = Just (n, PRef fc (sMN 0 (show n ++ x)))

944+ toMN (i, PRef fc n)

945+ | i `elem` ppos = Just (n, PRef fc (mkp n))

946+ | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))

938947 toMN _ = Nothing

939− getRecNameMap x _ = []

948+ getRecNameMap x _ _ = []

940949

941950 rec = sMN 0 "rec"

942951

943− mkp (UN n) = sMN 0 ("p_" ++ str n)

952+ -- only UNs propagate properly as parameters (bit of a hack then...)

953+ mkp (UN n) = sUN ("_p_" ++ str n)

944954 mkp (MN i n) = sMN i ("p_" ++ str n)

945955 mkp (NS n s) = NS (mkp n) s

946956

@@ -953,18 +963,19 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

953963 mkType (NS n s) = NS (mkType n) s

954964

955965 mkProj recty substs cimp ((pn_in, pty), pos)

956− = do let pn = expandNS syn pn_in

966+ = do let pn = expandNS syn pn_in -- projection name

967+ -- use pn_in in the indices, consistently, to avoid clash

957968 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

958969 (PPi expl rec recty

959970 (substMatches substs pty))

960971 let pls = repeat Placeholder

961972 let before = pos

962973 let after = length substs - (pos + 1)

963− let args = take before pls ++ PRef fc (mkp pn) : take after pls

974+ let args = take before pls ++ PRef fc (mkp pn_in) : take after pls

964975 let iargs = map implicitise (zip cimp args)

965976 let lhs = PApp fc (PRef fc pn)

966977 [pexp (PApp fc (PRef fc cn) iargs)]

967− let rhs = PRef fc (mkp pn)

978+ let rhs = PRef fc (mkp pn_in)

968979 let pclause = PClause fc pn lhs [] rhs []

969980 return [pfnTy, PClauses fc [] pn [pclause]]

970981

@@ -1425,7 +1436,8 @@ checkPossible info fc tcgen fname lhs_in

14251436 | otherwise = False -- name is different, unrecoverable

14261437

14271438getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1428− = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1439+ = nub $ getFixedInType i env [] t ++

1440+ getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

14291441getFixedInType i env (_ : is) (Bind n (Pi t) sc)

14301442 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

14311443getFixedInType i env is tm@(App f a)