c1968ed · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix parameter spotting in function types

c1968edEdwin Brady12 years ago

src/Idris/AbsSyntax.hs+4−1

compare with master

unifiedsplit

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

482 i <- getIState

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

484 idris_metavars i }

485+ where

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

487+ -- needed in tactic scripts

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

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

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

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

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

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

488 tidyNames used (Bind n b sc)

491 tidyNames used (Bind n b sc)

src/Idris/AbsSyntaxTree.hs+3−3

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

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

1131

1132instance 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

1134

1135instance Show PClause where

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

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

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

1467 baseName (UN n) = T.unpack n

1468 baseName (NS n ns) = baseName n

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

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

1470 baseName n | n == falseTy = "_|_"

1471 baseName other = show other

1472 nameSpace = case n of

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

1556 Nothing -> showbasic n

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

1558 showbasic n@(UN _) = showCG n

1559− showbasic (MN _ s) = str s

1559+ showbasic (MN i s) = str s

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

1561 showbasic (SN s) = show s

1562 fst3 (x, _, _) = x

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

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

384

385implicitable (NS n _) = implicitable n

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

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

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

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

389implicitable _ = False

390

src/Idris/ElabDecls.hs+25−13

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

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

137

138 addStatics n cty ty

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

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

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

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

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

142 ctxt <- getContext

141 ctxt <- getContext

143 let nty' = normalise ctxt [] nty

142 let nty' = normalise ctxt [] nty

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

144

145 -- Add normalised type to internals

146 i <- getIState

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

863 _ -> ifail "Something went inexplicably wrong"

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

865 [imps] -> return imps

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

867+ [ti] -> return $ param_pos ti

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

868+ let cty_imp = renameBs cimp cty

869+ let ptys = getProjs [] cty_imp

867 let ptys_u = getProjs [] cty

870 let ptys_u = getProjs [] cty

868− let recty = getRecTy cty

871+ let recty = getRecTy cty_imp

872+ let recty_u = getRecTy cty

869

873

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

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

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

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

872 -- we're generating

876 -- we're generating

873− let index_names_in = getRecNameMap "_in" recty

877+ let index_names_in = getRecNameMap "_in" ppos recty

874 let recty_in = substMatches index_names_in recty

878 let recty_in = substMatches index_names_in recty

875

879

876 logLvl 1 $ show (recty, ptys)

880 logLvl 1 $ show (recty, ptys)

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

884 let implBinds = getImplB id cty'

888 let implBinds = getImplB id cty'

885

889

886 -- Generate update functions

890 -- Generate update functions

887− update_decls <- mapM (mkUpdate recty index_names_in extraImpls

891+ update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls

888 (getFieldNames cty')

892 (getFieldNames cty')

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

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

890 mapM_ (elabDecl EAll info) (concat proj_decls)

894 mapM_ (elabDecl EAll info) (concat proj_decls)

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

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

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

933 getRecTy t = t

937 getRecTy t = t

934

938

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

940+ -- otherwise

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

941+ getRecNameMap x ppos (PApp fc t args)

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

936 where

943 where

944+ toMN (i, PRef fc n)

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

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

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

938 toMN _ = Nothing

947 toMN _ = Nothing

939− getRecNameMap x _ = []

948+ getRecNameMap x _ _ = []

940

949

941 rec = sMN 0 "rec"

950 rec = sMN 0 "rec"

942

951

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

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

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

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

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

945 mkp (NS n s) = NS (mkp n) s

955 mkp (NS n s) = NS (mkp n) s

946

956

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

953 mkType (NS n s) = NS (mkType n) s

963 mkType (NS n s) = NS (mkType n) s

954

964

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

965 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

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

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

958 (PPi expl rec recty

969 (PPi expl rec recty

959 (substMatches substs pty))

970 (substMatches substs pty))

960 let pls = repeat Placeholder

971 let pls = repeat Placeholder

961 let before = pos

972 let before = pos

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

973 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

964 let iargs = map implicitise (zip cimp args)

975 let iargs = map implicitise (zip cimp args)

965 let lhs = PApp fc (PRef fc pn)

976 let lhs = PApp fc (PRef fc pn)

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

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

967− let rhs = PRef fc (mkp pn)

978+ let rhs = PRef fc (mkp pn_in)

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

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

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

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

970

981

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

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

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

1426

1437

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

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

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

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

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

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

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

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

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

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

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