git.iko.soy/Idris-dev
on master help sign in
Compiler saturates constructors before compiling
4804676Edwin Brady
lib/prelude.idr+1−1
compare with master
unifiedsplit
@@ -98,7 +98,7 @@ instance Monad IO where {
98}
98}
99
99
100instance Monad Maybe where {
100instance Monad Maybe where {
101− return = Just
101+ return t = Just t
102
102
103 Nothing >>= k = Nothing
103 Nothing >>= k = Nothing
104 (Just x) >>= k = k x
104 (Just x) >>= k = k x
lib/system.idr+3−2
@@ -6,7 +6,8 @@ import prelude
6
6
7getArgs : IO (List String)
7getArgs : IO (List String)
8getArgs = do { n <- numArgs
8getArgs = do { n <- numArgs
9− ga' [] 0 n }
9+ ga' [] 0 n
10+ }
10 where {
11 where {
11 numArgs : IO Int
12 numArgs : IO Int
12 numArgs = mkForeign (FFun "epic_numArgs" [] FInt)
13 numArgs = mkForeign (FFun "epic_numArgs" [] FInt)
@@ -18,7 +19,7 @@ getArgs = do { n <- numArgs
18 ga' acc i n = if (i == n) then (return $ rev acc) else
19 ga' acc i n = if (i == n) then (return $ rev acc) else
19 do { arg <- getArg i
20 do { arg <- getArg i
20 ga' (arg :: acc) (i+1) n }
21 ga' (arg :: acc) (i+1) n }
21− }
22+}
22
23
23getEnv : String -> IO String
24getEnv : String -> IO String
24getEnv x = mkForeign (FFun "getenv" [FString] FString) x
25getEnv x = mkForeign (FFun "getenv" [FString] FString) x
src/Idris/Compiler.hs+16
@@ -73,6 +73,8 @@ instance ToEpic (TT Name) where
73 = do v' <- epic' env v
73 = do v' <- epic' env v
74 k' <- epic' env k
74 k' <- epic' env k
75 return (k' @@ (effect_ v'))
75 return (k' @@ (effect_ v'))
76+ | (P (DCon t a) n _, args) <- unApply tm
77+ = epicCon env t a n args
76 epic' env (P (DCon t a) n _) = return $ con_ t
78 epic' env (P (DCon t a) n _) = return $ con_ t
77 epic' env (P (TCon t a) n _) = return $ con_ t
79 epic' env (P (TCon t a) n _) = return $ con_ t
78 epic' env (P _ n _) = return $ ref (ename n)
80 epic' env (P _ n _) = return $ ref (ename n)
@@ -91,6 +93,20 @@ instance ToEpic (TT Name) where
91 epic' env (Constant c) = epic c
93 epic' env (Constant c) = epic c
92 epic' env (Set _) = return impossible
94 epic' env (Set _) = return impossible
93
95
96+ epicCon env t arity n args
97+ | length args == arity = buildApp env (con_ t) args
98+ | otherwise = let extra = satArgs (arity - length args) in
99+ do sc' <- epicCon env t arity n
100+ (args ++ map (\n -> P Bound n undefined) extra)
101+ return $ term (map ename extra, sc')
102+
103+ satArgs n = map (\i -> MN i "sat") [1..n]
104+
105+ buildApp env e [] = return e
106+ buildApp env e (x:xs) = do x' <- epic' env x
107+ buildApp env (e @@ x') xs
108+
109+
94doForeign :: [TT Name] -> Idris E.Term
110doForeign :: [TT Name] -> Idris E.Term
95doForeign (_ : fgn : args)
111doForeign (_ : fgn : args)
96 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn
112 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn