88f6bf1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix obscure where naming bug

88f6bf1Edwin Brady15 years ago

lib/prelude.idr+7−1

compare with master

unifiedsplit

@@ -162,7 +162,7 @@ ceiling x = prim__floatCeil x;

162---- some basic io

163

164putStr : String -> IO ();

165−putStr x = mkForeign (FFun "putStr" (FString :: Nil) FUnit) x;

165+putStr x = mkForeign (FFun "putStr" [FString] FUnit) x;

166

167putStrLn : String -> IO ();

168putStrLn x = putStr (x ++ "\n");

@@ -173,6 +173,12 @@ print x = putStrLn (show x);

173readLine : IO String;

174readLine = mkForeign (FFun "readStr" Nil FString);

175

176+putChar : Char -> IO ();

177+putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c;

178+

179+getChar : IO Char;

180+getChar = mkForeign (FFun "getchar" [] FChar);

181+

176---- some basic file handling

182---- some basic file handling

177

183

178data File = FHandle Ptr;

184data File = FHandle Ptr;

src/Idris/AbsSyntax.hs+38−3

@@ -762,9 +762,31 @@ piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

762expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

763expandParams dec ps ns tm = en tm

764 where

765+ -- if we shadow a name (say in a lambda binding) that is used in a call to

766+ -- a lifted function, we need access to both names - once in the scope of the

767+ -- binding and once to call the lifted functions. So we'll explicitly shadow

768+ -- it. (Yes, it's a hack. The alternative would be to resolve names earlier

769+ -- but we didn't...)

770+

771+ mkShadow (UN n) = MN 0 n

772+ mkShadow (MN i n) = MN (i+1) n

773+ mkShadow (NS x s) = NS (mkShadow x) s

774+

765− en (PLam n t s) = PLam n (en t) (en s)

775+ en (PLam n t s)

776+ | n `elem` map fst ps

777+ = let n' = mkShadow n in

778+ PLam n' (en t) (en (shadow n n' s))

779+ | otherwise = PLam n (en t) (en s)

766− en (PPi p n t s) = PPi p n (en t) (en s)

780+ en (PPi p n t s)

781+ | n `elem` map fst ps

782+ = let n' = mkShadow n in

783+ PPi p n' (en t) (en (shadow n n' s))

784+ | otherwise = PPi p n (en t) (en s)

785+ en (PLet n ty v s)

786+ | n `elem` map fst ps

787+ = let n' = mkShadow n in

788+ PLet n' (en ty) (en v) (en (shadow n n' s))

767− en (PLet n ty v s) = PLet n (en ty) (en v) (en s)

789+ | otherwise = PLet n (en ty) (en v) (en s)

768 en (PEq f l r) = PEq f (en l) (en r)

790 en (PEq f l r) = PEq f (en l) (en r)

769 en (PPair f l r) = PPair f (en l) (en r)

791 en (PPair f l r) = PPair f (en l) (en r)

770 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

792 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

@@ -1129,3 +1151,16 @@ substMatch n tm t = sm t where

1129 sm (PHidden x) = PHidden (sm x)

1151 sm (PHidden x) = PHidden (sm x)

1130 sm x = x

1152 sm x = x

1131

1153

1154+shadow :: Name -> Name -> PTerm -> PTerm

1155+shadow n n' t = sm t where

1156+ sm (PRef fc x) | n == x = PRef fc n'

1157+ sm (PLam x t sc) = PLam x (sm t) (sm sc)

1158+ sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1159+ sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1160+ sm (PEq f x y) = PEq f (sm x) (sm y)

1161+ sm (PPair f x y) = PPair f (sm x) (sm y)

1162+ sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1163+ sm (PAlternative as) = PAlternative (map sm as)

1164+ sm (PHidden x) = PHidden (sm x)

1165+ sm x = x

1166+

test/READMEnew file+7

@@ -0,0 +1,7 @@

1+Tests:

3+001: Well-typed interpreter

4+002: Universe checking

5+003: Literate source and string processing

6+004: File operations

7+005: Num class resolution [regression]; span & break; ad-hoc overloading