git.iko.soy/Idris-dev
on master help sign in
Give invented pattern variables unique names
commit2c05448b5ca45caae91e3202783c592f00a4615b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 10 Nov 2011, 23:20 (15 years ago) parentffc64e3
3 files changed+30−11
compare with master
unifiedsplit
src/Core/Elaborate.hs+4−1 src/Idris/AbsSyntax.hs+19−5 src/Idris/Compiler.hs+7−5
src/Core/Elaborate.hs+4−1
@@ -188,7 +188,10 @@ rewrite :: Raw -> Elab ()
188188rewrite tm = processTactic' (Rewrite tm)
189189
190190patvar :: Name -> Elab ()
191−patvar n = processTactic' (PatVar n)
191+patvar n = do n' <- case n of
192+ UN _ -> return n
193+ MN _ _ -> unique_hole n
194+ processTactic' (PatVar n')
192195
193196patbind :: Name -> Elab ()
194197patbind n = processTactic' (PatBind n)
src/Idris/AbsSyntax.hs+19−5
@@ -40,11 +40,13 @@ data IState = IState { tt_ctxt :: Context,
4040 syntax_keywords :: [String],
4141 imported :: [FilePath],
4242 idris_prims :: [(Name, ([E.Name], E.Term))],
43+ idris_objs :: [FilePath],
44+ idris_libs :: [String],
4345 errLine :: Maybe Int
4446 }
4547
4648idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext
47− "" defaultOpts 6 [] [] [] [] [] Nothing
49+ "" defaultOpts 6 [] [] [] [] [] [] [] Nothing
4850
4951-- The monad for the main REPL - reading and processing files and updating
5052-- global state (hence the IO inner monad).
@@ -53,6 +55,18 @@ type Idris a = StateT IState IO a
5355getContext :: Idris Context
5456getContext = do i <- get; return (tt_ctxt i)
5557
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+
5670setErrLine :: Int -> Idris ()
5771setErrLine x = do i <- get;
5872 case (errLine i) of
@@ -621,16 +635,16 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)
621635 PClauses fc opts n' (map expandParamsC cs)
622636 where
623637 expandParamsC (PClause n lhs ws rhs ds)
624− = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])
625− ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])
638+ = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
639+ ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
626640 n' = if n `elem` ns then dec n else n in
627641 PClause n' (expandParams dec ps'' ns lhs)
628642 (map (expandParams dec ps'' ns) ws)
629643 (expandParams dec ps'' ns rhs)
630644 (map (expandParamsD ist dec ps'' ns) ds)
631645 expandParamsC (PWith n lhs ws wval ds)
632− = let ps' = updateps True (namesIn ist wval) (zip ps [0..])
633− ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])
646+ = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
647+ ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
634648 n' = if n `elem` ns then dec n else n in
635649 PWith n' (expandParams dec ps'' ns lhs)
636650 (map (expandParams dec ps'' ns) ws)
src/Idris/Compiler.hs+7−5
@@ -17,7 +17,10 @@ primDefs = [UN ["mkForeign"]]
1717
1818compile :: FilePath -> Idris ()
1919compile f = do ds <- mkDecls
20− lift $ compileWith [Debug] (mkProgram ds) f
20+ objs <- getObjectFiles
21+ libs <- getLibs
22+ lift $ compileObjWith [Debug] (mkProgram ds) (f ++ ".o")
23+ lift $ link ((f ++ ".o") : objs) f
2124
2225mkDecls :: Idris [EpicDecl]
2326mkDecls = do i <- getIState
@@ -27,7 +30,6 @@ mkDecls = do i <- getIState
2730ename x = name ("idris_" ++ show x)
2831aname x = name ("a_" ++ show x)
2932
30−-- The 'unsafePerformIO' makes sure it gets evaluated fully
3133epicMain = effect_ $ ref (ename (UN ["run__IO"])) @@
3234 ref (ename (UN ["main"]))
3335
@@ -59,8 +61,8 @@ instance ToEpic (TT Name) where
5961 return $ lazy_ arg'
6062 epic' env (P (DCon t a) n _) = return $ con_ t
6163 epic' env (P (TCon t a) n _) = return $ con_ t
62− epic' env (P _ n _) = return $ ref (ename n)
63− epic' env (V i) = return $ ref (env!!i)
64+ epic' env (P _ n _) = return $ ref (ename n)
65+ epic' env (V i) = return $ ref (env!!i)
6466 epic' env (Bind n (Lam _) sc)
6567 = do sc' <- epic' (aname n : env) sc
6668 return $ term ([aname n], sc')
@@ -73,7 +75,7 @@ instance ToEpic (TT Name) where
7375 a' <- epic' env a
7476 return (f' @@ a')
7577 epic' env (Constant c) = epic c
76− epic' env (Set _) = return impossible
78+ epic' env (Set _) = return impossible
7779
7880doForeign :: [TT Name] -> Idris E.Term
7981doForeign (_ : fgn : args)