4804676 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Compiler saturates constructors before compiling

commit48046767d2e5ffd3f7d0ec913cf6dc447b9e8174 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 12:40 (15 years ago) parent961d2a3

3 files changed+20−3

compare with master

unifiedsplit

lib/prelude.idr+1−1 lib/system.idr+3−2 src/Idris/Compiler.hs+16

lib/prelude.idr+1−1

@@ -98,7 +98,7 @@ instance Monad IO where {

9898}

9999

100100instance Monad Maybe where {

101− return = Just

101+ return t = Just t

102102

103103 Nothing >>= k = Nothing

104104 (Just x) >>= k = k x

lib/system.idr+3−2

@@ -6,7 +6,8 @@ import prelude

77getArgs : IO (List String)

88getArgs = do { n <- numArgs

9− ga' [] 0 n }

9+ ga' [] 0 n

10+ }

1011 where {

1112 numArgs : IO Int

1213 numArgs = mkForeign (FFun "epic_numArgs" [] FInt)

@@ -18,7 +19,7 @@ getArgs = do { n <- numArgs

1819 ga' acc i n = if (i == n) then (return $ rev acc) else

1920 do { arg <- getArg i

2021 ga' (arg :: acc) (i+1) n }

21− }

22+}

2223

2324getEnv : String -> IO String

2425getEnv x = mkForeign (FFun "getenv" [FString] FString) x

src/Idris/Compiler.hs+16

@@ -73,6 +73,8 @@ instance ToEpic (TT Name) where

7373 = do v' <- epic' env v

7474 k' <- epic' env k

7575 return (k' @@ (effect_ v'))

76+ | (P (DCon t a) n _, args) <- unApply tm

77+ = epicCon env t a n args

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

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

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

@@ -91,6 +93,20 @@ instance ToEpic (TT Name) where

9193 epic' env (Constant c) = epic c

9294 epic' env (Set _) = return impossible

9395

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+

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

95111doForeign (_ : fgn : args)

96112 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn