2c05448 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Give invented pattern variables unique names

2c05448Edwin Brady15 years ago

src/Core/Elaborate.hs+4−1

compare with master

unifiedsplit

@@ -188,7 +188,10 @@ rewrite :: Raw -> Elab ()

188rewrite tm = processTactic' (Rewrite tm)

189

190patvar :: Name -> Elab ()

191+patvar n = do n' <- case n of

192+ UN _ -> return n

193+ MN _ _ -> unique_hole n

191−patvar n = processTactic' (PatVar n)

194+ processTactic' (PatVar n')

192

195

193patbind :: Name -> Elab ()

196patbind :: Name -> Elab ()

194patbind n = processTactic' (PatBind n)

197patbind n = processTactic' (PatBind n)

src/Idris/AbsSyntax.hs+19−5

@@ -40,11 +40,13 @@ data IState = IState { tt_ctxt :: Context,

40 syntax_keywords :: [String],

41 imported :: [FilePath],

42 idris_prims :: [(Name, ([E.Name], E.Term))],

43+ idris_objs :: [FilePath],

44+ idris_libs :: [String],

43 errLine :: Maybe Int

45 errLine :: Maybe Int

44 }

46 }

46idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

48idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

47− "" defaultOpts 6 [] [] [] [] [] Nothing

49+ "" defaultOpts 6 [] [] [] [] [] [] [] Nothing

49-- The monad for the main REPL - reading and processing files and updating

51-- The monad for the main REPL - reading and processing files and updating

50-- global state (hence the IO inner monad).

52-- global state (hence the IO inner monad).

@@ -53,6 +55,18 @@ type Idris a = StateT IState IO a

53getContext :: Idris Context

55getContext :: Idris Context

54getContext = do i <- get; return (tt_ctxt i)

56getContext = do i <- get; return (tt_ctxt i)

58+getObjectFiles :: Idris [FilePath]

59+getObjectFiles = do i <- get; return (idris_objs i)

60+

61+addObjectFile :: FilePath -> Idris ()

62+addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })

63+

64+getLibs :: Idris [String]

65+getLibs = do i <- get; return (idris_libs i)

66+

67+addLib :: String -> Idris ()

68+addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

69+

56setErrLine :: Int -> Idris ()

70setErrLine :: Int -> Idris ()

57setErrLine x = do i <- get;

71setErrLine x = do i <- get;

58 case (errLine i) of

72 case (errLine i) of

@@ -621,16 +635,16 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)

621 PClauses fc opts n' (map expandParamsC cs)

635 PClauses fc opts n' (map expandParamsC cs)

622 where

636 where

623 expandParamsC (PClause n lhs ws rhs ds)

637 expandParamsC (PClause n lhs ws rhs ds)

624− = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])

638+ = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])

625− ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])

639+ ps'' = updateps False (namesIn ist lhs) (zip ps [0..])

626 n' = if n `elem` ns then dec n else n in

640 n' = if n `elem` ns then dec n else n in

627 PClause n' (expandParams dec ps'' ns lhs)

641 PClause n' (expandParams dec ps'' ns lhs)

628 (map (expandParams dec ps'' ns) ws)

642 (map (expandParams dec ps'' ns) ws)

629 (expandParams dec ps'' ns rhs)

643 (expandParams dec ps'' ns rhs)

630 (map (expandParamsD ist dec ps'' ns) ds)

644 (map (expandParamsD ist dec ps'' ns) ds)

631 expandParamsC (PWith n lhs ws wval ds)

645 expandParamsC (PWith n lhs ws wval ds)

632− = let ps' = updateps True (namesIn ist wval) (zip ps [0..])

646+ = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])

633− ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])

647+ ps'' = updateps False (namesIn ist lhs) (zip ps [0..])

634 n' = if n `elem` ns then dec n else n in

648 n' = if n `elem` ns then dec n else n in

635 PWith n' (expandParams dec ps'' ns lhs)

649 PWith n' (expandParams dec ps'' ns lhs)

636 (map (expandParams dec ps'' ns) ws)

650 (map (expandParams dec ps'' ns) ws)

src/Idris/Compiler.hs+7−5

@@ -17,7 +17,10 @@ primDefs = [UN ["mkForeign"]]

18compile :: FilePath -> Idris ()

19compile f = do ds <- mkDecls

20+ objs <- getObjectFiles

21+ libs <- getLibs

20− lift $ compileWith [Debug] (mkProgram ds) f

22+ lift $ compileObjWith [Debug] (mkProgram ds) (f ++ ".o")

23+ lift $ link ((f ++ ".o") : objs) f

22mkDecls :: Idris [EpicDecl]

25mkDecls :: Idris [EpicDecl]

23mkDecls = do i <- getIState

26mkDecls = do i <- getIState

@@ -27,7 +30,6 @@ mkDecls = do i <- getIState

27ename x = name ("idris_" ++ show x)

30ename x = name ("idris_" ++ show x)

28aname x = name ("a_" ++ show x)

31aname x = name ("a_" ++ show x)

30−-- The 'unsafePerformIO' makes sure it gets evaluated fully

31epicMain = effect_ $ ref (ename (UN ["run__IO"])) @@

33epicMain = effect_ $ ref (ename (UN ["run__IO"])) @@

32 ref (ename (UN ["main"]))

34 ref (ename (UN ["main"]))

@@ -59,8 +61,8 @@ instance ToEpic (TT Name) where

59 return $ lazy_ arg'

61 return $ lazy_ arg'

60 epic' env (P (DCon t a) n _) = return $ con_ t

62 epic' env (P (DCon t a) n _) = return $ con_ t

61 epic' env (P (TCon t a) n _) = return $ con_ t

63 epic' env (P (TCon t a) n _) = return $ con_ t

62− epic' env (P _ n _) = return $ ref (ename n)

64+ epic' env (P _ n _) = return $ ref (ename n)

63− epic' env (V i) = return $ ref (env!!i)

65+ epic' env (V i) = return $ ref (env!!i)

64 epic' env (Bind n (Lam _) sc)

66 epic' env (Bind n (Lam _) sc)

65 = do sc' <- epic' (aname n : env) sc

67 = do sc' <- epic' (aname n : env) sc

66 return $ term ([aname n], sc')

68 return $ term ([aname n], sc')

@@ -73,7 +75,7 @@ instance ToEpic (TT Name) where

73 a' <- epic' env a

75 a' <- epic' env a

74 return (f' @@ a')

76 return (f' @@ a')

75 epic' env (Constant c) = epic c

77 epic' env (Constant c) = epic c

76− epic' env (Set _) = return impossible

78+ epic' env (Set _) = return impossible

78doForeign :: [TT Name] -> Idris E.Term

80doForeign :: [TT Name] -> Idris E.Term

79doForeign (_ : fgn : args)

81doForeign (_ : fgn : args)