e08a18d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'refs/remotes/upstream/master' into quasiquote

e08a18dDavid Raymond Christiansen12 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -9,6 +9,7 @@ New in 0.9.14:

9 functions and let. The keyword for this is "pi".

10* Experimental 'neweffects' library, with simplified API

11* All new JavaScript backend (avoids callstack overflows)

12+* Add support for %lib directive for NodeJS

12* Quasiquotes and quasiquote patterns allow easier work with reflected terms.

13* Quasiquotes and quasiquote patterns allow easier work with reflected terms.

13 `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected

14 `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected

14 version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected

15 version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected

Setup.hs+49−8

@@ -13,8 +13,9 @@ import Distribution.Simple.Utils (createDirectoryIfMissingVerbose, rewriteFile)

13import Distribution.PackageDescription

14import Distribution.Text

16+import System.Environment

16import System.Exit

17import System.Exit

17−import System.FilePath ((</>), splitDirectories)

18+import System.FilePath ((</>), splitDirectories,isAbsolute)

18import System.Directory

19import System.Directory

19import qualified System.FilePath.Posix as Px

20import qualified System.FilePath.Posix as Px

20import System.Process

21import System.Process

@@ -70,6 +71,12 @@ isRelease flags =

70 Just False -> False

71 Just False -> False

71 Nothing -> False

72 Nothing -> False

74+isFreestanding :: S.ConfigFlags -> Bool

75+isFreestanding flags =

76+ case lookup (FlagName "freestanding") (S.configConfigurationsFlags flags) of

77+ Just True -> True

78+ Just False -> False

79+ Nothing -> False

73-- -----------------------------------------------------------------------------

80-- -----------------------------------------------------------------------------

74-- Clean

81-- Clean

@@ -98,12 +105,12 @@ gitHash = do h <- Control.Exception.catch (readProcess "git" ["rev-parse", "--sh

98-- Put the Git hash into a module for use in the program

105-- Put the Git hash into a module for use in the program

99-- For release builds, just put the empty string in the module

106-- For release builds, just put the empty string in the module

100generateVersionModule verbosity dir release = do

107generateVersionModule verbosity dir release = do

101− hash <- gitHash

108+ hash <- gitHash

102− let versionModulePath = dir </> "Version_idris" Px.<.> "hs"

109+ let versionModulePath = dir </> "Version_idris" Px.<.> "hs"

103− putStrLn $ "Generating " ++ versionModulePath ++

110+ putStrLn $ "Generating " ++ versionModulePath ++

104 if release then " for release" else (" for prerelease " ++ hash)

111 if release then " for release" else (" for prerelease " ++ hash)

105− createDirectoryIfMissingVerbose verbosity True dir

112+ createDirectoryIfMissingVerbose verbosity True dir

106− rewriteFile versionModulePath (versionModuleContents hash)

113+ rewriteFile versionModulePath (versionModuleContents hash)

107

114

108 where versionModuleContents h = "module Version_idris where\n\n" ++

115 where versionModuleContents h = "module Version_idris where\n\n" ++

109 "gitHash :: String\n" ++

116 "gitHash :: String\n" ++

@@ -111,9 +118,38 @@ generateVersionModule verbosity dir release = do

111 then "gitHash = \"\"\n"

118 then "gitHash = \"\"\n"

112 else "gitHash = \"-git:" ++ h ++ "\"\n"

119 else "gitHash = \"-git:" ++ h ++ "\"\n"

113

120

121+-- Generate a module that contains the lib path for a freestanding Idris

122+generateTargetModule verbosity dir targetDir = do

123+ absPath <- return $ isAbsolute targetDir

124+ let targetModulePath = dir </> "Target_idris" Px.<.> "hs"

125+ putStrLn $ "Generating " ++ targetModulePath

126+ createDirectoryIfMissingVerbose verbosity True dir

127+ rewriteFile targetModulePath (versionModuleContents absPath targetDir)

128+ where versionModuleContents absolute td = "module Target_idris where\n\n" ++

129+ "import System.FilePath\n" ++

130+ "import System.Environment\n" ++

131+ "getDataDir :: IO String\n" ++

132+ if absolute

133+ then "getDataDir = return \"" ++ td ++ "\"\n"

134+ else "getDataDir = do \n" ++

135+ " expath <- getExecutablePath\n" ++

136+ " execDir <- return $ dropFileName expath\n" ++

137+ " return $ execDir ++ \"" ++ td ++ "\"\n"

138+ ++ "getDataFileName :: FilePath -> IO FilePath\n"

139+ ++ "getDataFileName name = do\n"

140+ ++ " dir <- getDataDir\n"

141+ ++ " return (dir ++ \"/\" ++ name)"

142+

143+

114idrisConfigure _ flags _ local = do

144idrisConfigure _ flags _ local = do

115 configureRTS

145 configureRTS

116 generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))

146 generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))

147+ when (isFreestanding $ configFlags local) (do

148+ targetDir <- lookupEnv "IDRIS_INSTALL_DIR"

149+ case targetDir of

150+ Just d -> generateTargetModule verbosity (autogenModulesDir local) d

151+ Nothing -> error $ "Trying to build freestanding without a target directory."

152+ ++ " Set it by defining IDRIS_INSTALL_DIR.")

117 where

153 where

118 verbosity = S.fromFlag $ S.configVerbosity flags

154 verbosity = S.fromFlag $ S.configVerbosity flags

119 version = pkgVersion . package $ localPkgDescr local

155 version = pkgVersion . package $ localPkgDescr local

@@ -128,12 +164,16 @@ idrisPreSDist args flags = do

128 let dir = S.fromFlag (S.sDistDirectory flags)

164 let dir = S.fromFlag (S.sDistDirectory flags)

129 let verb = S.fromFlag (S.sDistVerbosity flags)

165 let verb = S.fromFlag (S.sDistVerbosity flags)

130 generateVersionModule verb ("src") True

166 generateVersionModule verb ("src") True

167+ generateTargetModule verb "src" "./libs"

131 preSDist simpleUserHooks args flags

168 preSDist simpleUserHooks args flags

132

169

133idrisPostSDist args flags desc lbi = do

170idrisPostSDist args flags desc lbi = do

134 Control.Exception.catch (do let file = "src" </> "Version_idris" Px.<.> "hs"

171 Control.Exception.catch (do let file = "src" </> "Version_idris" Px.<.> "hs"

172+ let targetFile = "src" </> "Target_idris" Px.<.> "hs"

135− putStrLn $ "Removing generated module " ++ file

173+ putStrLn $ "Removing generated modules:\n "

174+ ++ file ++ "\n" ++ targetFile

175+ removeFile file

136− removeFile file)

176+ removeFile targetFile)

137 (\e -> let e' = (e :: SomeException) in return ())

177 (\e -> let e' = (e :: SomeException) in return ())

138 postSDist simpleUserHooks args flags desc lbi

178 postSDist simpleUserHooks args flags desc lbi

139

179

@@ -168,6 +208,7 @@ idrisBuild _ flags _ local = do

168 gmpflag True = ["GMP=-DIDRIS_GMP"]

208 gmpflag True = ["GMP=-DIDRIS_GMP"]

169

209

170

210

211+

171-- -----------------------------------------------------------------------------

212-- -----------------------------------------------------------------------------

172-- Copy/Install

213-- Copy/Install

173

214

idris.cabal+9

@@ -515,6 +515,11 @@ Flag release

515 Default: False

516 manual: True

517

518+Flag freestanding

519+ Description: Build an Idris that doesn't use cabal

520+ Default: False

521+ manual: True

522+

518Library

523Library

519 hs-source-dirs: src

524 hs-source-dirs: src

520 Exposed-modules:

525 Exposed-modules:

@@ -627,6 +632,7 @@ Library

627 , directory

632 , directory

628 , directory >= 1.2

633 , directory >= 1.2

629 , filepath

634 , filepath

635+ , fingertree >= 0.1

630 , haskeline >= 0.7

636 , haskeline >= 0.7

631 , language-java >= 0.2.6

637 , language-java >= 0.2.6

632 , lens >= 4.1.1

638 , lens >= 4.1.1

@@ -688,6 +694,9 @@ Library

688 if flag(curses)

694 if flag(curses)

689 build-depends: hscurses

695 build-depends: hscurses

690 cpp-options: -DCURSES

696 cpp-options: -DCURSES

697+ if flag(freestanding)

698+ other-modules: Target_idris

699+ cpp-options: -DFREESTANDING

691

700

692Executable idris

701Executable idris

693 Main-is: Main.hs

702 Main-is: Main.hs

jsrts/Runtime-common.js−1

@@ -5,7 +5,6 @@ var i$VM = function() {

5 this.valstack_base = 0;

7 this.ret = null;

8− this.reg1 = null;

10 this.callstack = [];

9 this.callstack = [];

11}

10}

jsrts/jsbn/jsbn.js+3−3

@@ -1,4 +1,4 @@

1−var __IDRRT__bigInt = (function() {

1+var i$bigInt = (function() {

4// See "LICENSE" for details.

@@ -1234,5 +1234,5 @@ return function(val) {

1234}

1235})();

1236

1237−var __IDRRT__ZERO = __IDRRT__bigInt("0");

1237+var i$ZERO = i$bigInt("0");

1238−var __IDRRT__ONE = __IDRRT__bigInt("1");

1238+var i$ONE = i$bigInt("1");

libs/base/System.idr+3

@@ -80,3 +80,6 @@ time = mkForeign (FFun "idris_time" [] FInt)

80usleep : Int -> IO ()

81usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i

83+system : String -> IO Int

84+system cmd = mkForeign (FFun "system" [FString] FInt) cmd

85+

libs/prelude/Prelude/Nat.idr+39−45

@@ -146,19 +146,15 @@ gt left right = lt right left

146

147||| Find the least of two natural numbers

148total minimum : Nat -> Nat -> Nat

149−minimum left right =

149+minimum Z m = Z

150− if lte left right then

150+minimum (S n) Z = Z

151− left

151+minimum (S n) (S m) = S (minimum n m)

152− else

153− right

154

152

155||| Find the greatest of two natural numbers

153||| Find the greatest of two natural numbers

156total maximum : Nat -> Nat -> Nat

154total maximum : Nat -> Nat -> Nat

157−maximum left right =

155+maximum Z m = m

158− if lte left right then

156+maximum (S n) Z = S n

159− right

157+maximum (S n) (S m) = S (maximum n m)

160− else

161− left

162

158

163--------------------------------------------------------------------------------

159--------------------------------------------------------------------------------

164-- Type class instances

160-- Type class instances

@@ -635,8 +631,40 @@ lteSuccZeroFalse Z = refl

635lteSuccZeroFalse (S n) = refl

631lteSuccZeroFalse (S n) = refl

636

632

637-- Minimum and maximum

633-- Minimum and maximum

634+total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r

635+maximumAssociative Z c r = refl

636+maximumAssociative (S k) Z r = refl

637+maximumAssociative (S k) (S j) Z = refl

638+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in refl

639+

640+total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l

641+maximumCommutative Z Z = refl

642+maximumCommutative Z (S k) = refl

643+maximumCommutative (S k) Z = refl

644+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in refl

645+

646+total maximumIdempotent : (n : Nat) -> maximum n n = n

647+maximumIdempotent Z = refl

648+maximumIdempotent (S k) = cong (maximumIdempotent k)

649+

650+total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r

651+minimumAssociative Z c r = refl

652+minimumAssociative (S k) Z r = refl

653+minimumAssociative (S k) (S j) Z = refl

654+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in refl

655+

656+total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l

657+minimumCommutative Z Z = refl

658+minimumCommutative Z (S k) = refl

659+minimumCommutative (S k) Z = refl

660+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in refl

661+

662+total minimumIdempotent : (n : Nat) -> minimum n n = n

663+minimumIdempotent Z = refl

664+minimumIdempotent (S k) = cong (minimumIdempotent k)

665+

638total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

666total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

639−minimumZeroZeroRight Z = refl

667+minimumZeroZeroRight Z = refl

640minimumZeroZeroRight (S right) = minimumZeroZeroRight right

668minimumZeroZeroRight (S right) = minimumZeroZeroRight right

641

669

642total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

670total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

@@ -652,15 +680,6 @@ minimumSuccSucc (S left) (S right) =

652 let inductiveHypothesis = minimumSuccSucc left right in

680 let inductiveHypothesis = minimumSuccSucc left right in

653 ?minimumSuccSuccStepCase

681 ?minimumSuccSuccStepCase

654

682

655−total minimumCommutative : (left : Nat) -> (right : Nat) ->

656− minimum left right = minimum right left

657−minimumCommutative Z Z = refl

658−minimumCommutative Z (S right) = refl

659−minimumCommutative (S left) Z = refl

660−minimumCommutative (S left) (S right) =

661− let inductiveHypothesis = minimumCommutative left right in

662− ?minimumCommutativeStepCase

663−

664total maximumZeroNRight : (right : Nat) -> maximum Z right = right

683total maximumZeroNRight : (right : Nat) -> maximum Z right = right

665maximumZeroNRight Z = refl

684maximumZeroNRight Z = refl

666maximumZeroNRight (S right) = refl

685maximumZeroNRight (S right) = refl

@@ -678,15 +697,6 @@ maximumSuccSucc (S left) (S right) =

678 let inductiveHypothesis = maximumSuccSucc left right in

697 let inductiveHypothesis = maximumSuccSucc left right in

679 ?maximumSuccSuccStepCase

698 ?maximumSuccSuccStepCase

680

699

681−total maximumCommutative : (left : Nat) -> (right : Nat) ->

682− maximum left right = maximum right left

683−maximumCommutative Z Z = refl

684−maximumCommutative (S left) Z = refl

685−maximumCommutative Z (S right) = refl

686−maximumCommutative (S left) (S right) =

687− let inductiveHypothesis = maximumCommutative left right in

688− ?maximumCommutativeStepCase

689−

690-- div and mod

700-- div and mod

691total modZeroZero : (n : Nat) -> mod 0 n = Z

701total modZeroZero : (n : Nat) -> mod 0 n = Z

692modZeroZero Z = refl

702modZeroZero Z = refl

@@ -852,28 +862,12 @@ plusZeroRightNeutralStepCase = proof {

852 trivial;

862 trivial;

853}

863}

854

864

855−maximumCommutativeStepCase = proof {

856− intros;

857− rewrite (boolElimSuccSucc (lte left right) right left);

858− rewrite (boolElimSuccSucc (lte right left) left right);

859− rewrite inductiveHypothesis;

860− trivial;

861−}

862−

863maximumSuccSuccStepCase = proof {

865maximumSuccSuccStepCase = proof {

864 intros;

866 intros;

865 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));

867 rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));

866 trivial;

868 trivial;

867}

869}

868

870

869−minimumCommutativeStepCase = proof {

870− intros;

871− rewrite (boolElimSuccSucc (lte left right) left right);

872− rewrite (boolElimSuccSucc (lte right left) right left);

873− rewrite inductiveHypothesis;

874− trivial;

875−}

876−

877minimumSuccSuccStepCase = proof {

871minimumSuccSuccStepCase = proof {

878 intros;

872 intros;

879 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));

873 rewrite (boolElimSuccSucc (lte left right) (S left) (S right));

src/IRTS/CodegenC.hs−1

@@ -7,7 +7,6 @@ import IRTS.Simplified

7import IRTS.System

8import IRTS.CodegenCommon

9import Idris.Core.TT

10−import Paths_idris

11import Util.System

10import Util.System

13import Numeric

12import Numeric

src/IRTS/CodegenJavaScript.hs+82−48

@@ -7,7 +7,7 @@ import IRTS.Lang

7import IRTS.Simplified

8import IRTS.CodegenCommon

9import Idris.Core.TT

10−import Paths_idris

10+import IRTS.System

11import Util.System

13import Control.Arrow

@@ -24,21 +24,39 @@ import System.IO

24import System.Directory

27−idrNamespace :: String

28−idrNamespace = "__IDR__"

29−idrRTNamespace = "__IDRRT__"

30−idrLTNamespace = "__IDRLT__"

31−idrCTRNamespace = "__IDRCTR__"

32−

33−data CompileInfo = CompileInfo { compileInfoApplyCases :: [Int]

27+data CompileInfo = CompileInfo { compileInfoApplyCases :: [Int]

34− , compileInfoEvalCases :: [Int]

28+ , compileInfoEvalCases :: [Int]

29+ , compileInfoNeedsBigInt :: Bool

35 }

30 }

38initCompileInfo :: [(Name, [BC])] -> CompileInfo

33initCompileInfo :: [(Name, [BC])] -> CompileInfo

39initCompileInfo bc =

34initCompileInfo bc =

40− CompileInfo (collectCases "APPLY" bc) (collectCases "EVAL" bc)

35+ CompileInfo (collectCases "APPLY" bc) (collectCases "EVAL" bc) (lookupBigInt bc)

41 where

36 where

37+ lookupBigInt :: [(Name, [BC])] -> Bool

38+ lookupBigInt = any (needsBigInt . snd)

39+ where

40+ needsBigInt :: [BC] -> Bool

41+ needsBigInt bc = or $ map testBCForBigInt bc

42+ where

43+ testBCForBigInt :: BC -> Bool

44+ testBCForBigInt (ASSIGNCONST _ c) =

45+ testConstForBigInt c

46+

47+ testBCForBigInt (CONSTCASE _ c d) =

48+ maybe False needsBigInt d

49+ || (or $ map (needsBigInt . snd) c)

50+ || (or $ map (testConstForBigInt . fst) c)

51+

52+ testBCForBigInt _ = False

53+

54+ testConstForBigInt :: Const -> Bool

55+ testConstForBigInt (BI _) = True

56+ testConstForBigInt (B64 _) = True

57+ testConstForBigInt _ = False

58+

59+

42 collectCases :: String -> [(Name, [BC])] -> [Int]

60 collectCases :: String -> [(Name, [BC])] -> [Int]

43 collectCases fun bc = getCases $ findFunction fun bc

61 collectCases fun bc = getCases $ findFunction fun bc

@@ -147,7 +165,7 @@ ffi code args = let parsed = ffiParse code in

147 | isDigit s =

165 | isDigit s =

148 FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)

166 FFIArg (read $ s : takeWhile isDigit ss) : ffiParse (dropWhile isDigit ss)

149 | otherwise =

167 | otherwise =

150− [FFIError $ "FFI - Invalid positional argument"]

168+ [FFIError "FFI - Invalid positional argument"]

151 ffiParse (s:ss) = FFICode s : ffiParse ss

169 ffiParse (s:ss) = FFICode s : ffiParse ss

152

170

153

171

@@ -159,8 +177,8 @@ ffi code args = let parsed = ffiParse code in

159

177

160 renderFFI :: [FFI] -> [String] -> String

178 renderFFI :: [FFI] -> [String] -> String

161 renderFFI [] _ = ""

179 renderFFI [] _ = ""

162− renderFFI ((FFICode c) : fs) args = c : renderFFI fs args

180+ renderFFI (FFICode c : fs) args = c : renderFFI fs args

163− renderFFI ((FFIArg i) : fs) args

181+ renderFFI (FFIArg i : fs) args

164 | i < length args && i >= 0 = args !! i ++ renderFFI fs args

182 | i < length args && i >= 0 = args !! i ++ renderFFI fs args

165 | otherwise = error "FFI - Argument index out of bounds"

183 | otherwise = error "FFI - Argument index out of bounds"

166

184

@@ -190,18 +208,18 @@ compileJS' indent (JSFunction args body) =

190 ++ "\n}\n"

208 ++ "\n}\n"

191

209

192compileJS' indent (JSType ty)

210compileJS' indent (JSType ty)

193− | JSIntTy <- ty = idrRTNamespace ++ "Int"

211+ | JSIntTy <- ty = "i$Int"

194− | JSStringTy <- ty = idrRTNamespace ++ "String"

212+ | JSStringTy <- ty = "i$String"

195− | JSIntegerTy <- ty = idrRTNamespace ++ "Integer"

213+ | JSIntegerTy <- ty = "i$Integer"

196− | JSFloatTy <- ty = idrRTNamespace ++ "Float"

214+ | JSFloatTy <- ty = "i$Float"

197− | JSCharTy <- ty = idrRTNamespace ++ "Char"

215+ | JSCharTy <- ty = "i$Char"

198− | JSPtrTy <- ty = idrRTNamespace ++ "Ptr"

216+ | JSPtrTy <- ty = "i$Ptr"

199− | JSForgotTy <- ty = idrRTNamespace ++ "Forgot"

217+ | JSForgotTy <- ty = "i$Forgot"

200

218

201compileJS' indent (JSSeq seq) =

219compileJS' indent (JSSeq seq) =

202 intercalate ";\n" (

220 intercalate ";\n" (

203 map (

221 map (

204− ((replicate indent ' ') ++) . (compileJS' indent)

222+ (replicate indent ' ' ++) . (compileJS' indent)

205 ) $ filter (/= JSNoop) seq

223 ) $ filter (/= JSNoop) seq

206 ) ++ ";"

224 ) ++ ";"

207

225

@@ -260,10 +278,10 @@ compileJS' indent (JSString str) =

260compileJS' indent (JSNum num)

278compileJS' indent (JSNum num)

261 | JSInt i <- num = show i

279 | JSInt i <- num = show i

262 | JSFloat f <- num = show f

280 | JSFloat f <- num = show f

263− | JSInteger JSBigZero <- num = "__IDRRT__ZERO"

281+ | JSInteger JSBigZero <- num = "i$ZERO"

264− | JSInteger JSBigOne <- num = "__IDRRT__ONE"

282+ | JSInteger JSBigOne <- num = "i$ONE"

265 | JSInteger (JSBigInt i) <- num = show i

283 | JSInteger (JSBigInt i) <- num = show i

266− | JSInteger (JSBigIntExpr e) <- num = "__IDRRT__bigInt(" ++ compileJS' indent e ++ ")"

284+ | JSInteger (JSBigIntExpr e) <- num = "i$bigInt(" ++ compileJS' indent e ++ ")"

267

285

268compileJS' indent (JSAssign lhs rhs) =

286compileJS' indent (JSAssign lhs rhs) =

269 compileJS' indent lhs ++ " = " ++ compileJS' indent rhs

287 compileJS' indent lhs ++ " = " ++ compileJS' indent rhs

@@ -294,14 +312,16 @@ compileJS' indent (JSCond branches) =

294 ++ replicate (indent + 2) ' ' ++ compileJS' (indent + 2) e

312 ++ replicate (indent + 2) ' ' ++ compileJS' (indent + 2) e

295 ++ ";\n" ++ replicate indent ' ' ++ "}"

313 ++ ";\n" ++ replicate indent ' ' ++ "}"

296

314

297−compileJS' indent (JSSwitch val [(_,seq)] Nothing) =

315+compileJS' indent (JSSwitch val [(_,JSSeq seq)] Nothing) =

316+ let (h,t) = splitAt 1 seq in

298− compileJS' indent seq

317+ (concatMap (compileJS' indent) h ++ ";\n")

318+ ++ (intercalate ";\n" $ map ((replicate indent ' ' ++) . compileJS' indent) t)

299

319

300compileJS' indent (JSSwitch val branches def) =

320compileJS' indent (JSSwitch val branches def) =

301 "switch(" ++ compileJS' indent val ++ "){\n"

321 "switch(" ++ compileJS' indent val ++ "){\n"

302 ++ concatMap mkBranch branches

322 ++ concatMap mkBranch branches

303 ++ mkDefault def

323 ++ mkDefault def

304− ++ (replicate indent ' ') ++ "}"

324+ ++ replicate indent ' ' ++ "}"

305 where

325 where

306 mkBranch :: (JS, JS) -> String

326 mkBranch :: (JS, JS) -> String

307 mkBranch (tag, code) =

327 mkBranch (tag, code) =

@@ -335,24 +355,27 @@ compileJS' indent (JSWord word)

335 | JSWord8 b <- word = "new Uint8Array([" ++ show b ++ "])"

355 | JSWord8 b <- word = "new Uint8Array([" ++ show b ++ "])"

336 | JSWord16 b <- word = "new Uint16Array([" ++ show b ++ "])"

356 | JSWord16 b <- word = "new Uint16Array([" ++ show b ++ "])"

337 | JSWord32 b <- word = "new Uint32Array([" ++ show b ++ "])"

357 | JSWord32 b <- word = "new Uint32Array([" ++ show b ++ "])"

338− | JSWord64 b <- word = idrRTNamespace ++ "bigInt(\"" ++ show b ++ "\")"

358+ | JSWord64 b <- word = "i$bigInt(\"" ++ show b ++ "\")"

339

359

340codegenJavaScript :: CodeGenerator

360codegenJavaScript :: CodeGenerator

361+codegenJavaScript ci =

341−codegenJavaScript ci = codegenJS_all JavaScript (simpleDecls ci)

362+ codegenJS_all JavaScript (simpleDecls ci)

342− (includes ci) (outputFile ci) (outputType ci)

363+ (includes ci) [] (outputFile ci) (outputType ci)

343

364

344codegenNode :: CodeGenerator

365codegenNode :: CodeGenerator

366+codegenNode ci =

345−codegenNode ci = codegenJS_all Node (simpleDecls ci)

367+ codegenJS_all Node (simpleDecls ci)

346− (includes ci) (outputFile ci) (outputType ci)

368+ (includes ci) (compileLibs ci) (outputFile ci) (outputType ci)

347

369

348codegenJS_all

370codegenJS_all

349 :: JSTarget

371 :: JSTarget

350 -> [(Name, SDecl)]

372 -> [(Name, SDecl)]

351 -> [FilePath]

373 -> [FilePath]

374+ -> [String]

352 -> FilePath

375 -> FilePath

353 -> OutputType

376 -> OutputType

354 -> IO ()

377 -> IO ()

355−codegenJS_all target definitions includes filename outputType = do

378+codegenJS_all target definitions includes libs filename outputType = do

356 let bytecode = map toBC definitions

379 let bytecode = map toBC definitions

357 let info = initCompileInfo bytecode

380 let info = initCompileInfo bytecode

358 let js = concatMap (translateDecl info) bytecode

381 let js = concatMap (translateDecl info) bytecode

@@ -365,14 +388,26 @@ codegenJS_all target definitions includes filename outputType = do

365 path <- (++) <$> getDataDir <*> (pure "/jsrts/")

388 path <- (++) <$> getDataDir <*> (pure "/jsrts/")

366 idrRuntime <- readFile $ path ++ "Runtime-common.js"

389 idrRuntime <- readFile $ path ++ "Runtime-common.js"

367 tgtRuntime <- readFile $ concat [path, "Runtime", rt, ".js"]

390 tgtRuntime <- readFile $ concat [path, "Runtime", rt, ".js"]

391+ jsbn <- if compileInfoNeedsBigInt info

368− jsbn <- readFile $ path ++ "jsbn/jsbn.js"

392+ then readFile $ path ++ "jsbn/jsbn.js"

393+ else return ""

369− let runtime = header ++ included ++ jsbn ++ idrRuntime ++ tgtRuntime

394+ let runtime = ( header

395+ ++ includeLibs libs

396+ ++ included

397+ ++ jsbn

398+ ++ idrRuntime

399+ ++ tgtRuntime

400+ )

370 writeFile filename $ runtime ++ concat code ++ main ++ invokeMain

401 writeFile filename $ runtime ++ concat code ++ main ++ invokeMain

371 setPermissions filename (emptyPermissions { readable = True

402 setPermissions filename (emptyPermissions { readable = True

372− , executable = target == Node

403+ , executable = target == Node

373− , writable = True

404+ , writable = True

374− })

405+ })

375 where

406 where

407+ includeLibs :: [String] -> String

408+ includeLibs =

409+ concatMap (\lib -> "var " ++ lib ++ " = require(\"" ++ lib ++"\");\n")

410+

376 getIncludes :: [FilePath] -> IO [String]

411 getIncludes :: [FilePath] -> IO [String]

377 getIncludes = mapM readFile

412 getIncludes = mapM readFile

378

413

@@ -455,15 +490,15 @@ splitFunction (JSAlloc name (Just (JSFunction args body@(JSSeq _)))) = do

455 where

490 where

456 processBranches :: [(JS,JS)] -> RWS () [(Int,JS)] Int [(JS,JS)]

491 processBranches :: [(JS,JS)] -> RWS () [(Int,JS)] Int [(JS,JS)]

457 processBranches =

492 processBranches =

458− traverse (runKleisli (arr id *** (Kleisli splitSequence)))

493+ traverse (runKleisli (arr id *** Kleisli splitSequence))

459

494

460 splitSequence :: JS -> RWS () [(Int, JS)] Int JS

495 splitSequence :: JS -> RWS () [(Int, JS)] Int JS

461− splitSequence js@(JSSeq seq) = do

496+ splitSequence js@(JSSeq seq) =

462 let (pre,post) = break isCall seq in

497 let (pre,post) = break isCall seq in

463 case post of

498 case post of

464 [] -> JSSeq <$> traverse splitCondition seq

499 [] -> JSSeq <$> traverse splitCondition seq

465 [js@(JSCond _)] -> splitCondition js

500 [js@(JSCond _)] -> splitCondition js

466− [js@(JSSwitch _ _ _)] -> splitCondition js

501+ [js@(JSSwitch {})] -> splitCondition js

467 [_] -> return js

502 [_] -> return js

468 (call:rest) -> do

503 (call:rest) -> do

469 depth <- get

504 depth <- get

@@ -533,7 +568,7 @@ translateDecl info (name@(MN 0 fun), bc)

533

568

534 isCase :: BC -> Bool

569 isCase :: BC -> Bool

535 isCase bc

570 isCase bc

536− | CASE _ _ _ _ <- bc = True

571+ | CASE {} <- bc = True

537 | otherwise = False

572 | otherwise = False

538

573

539 defaultCase :: [BC] -> [BC]

574 defaultCase :: [BC] -> [BC]

@@ -571,7 +606,7 @@ translateDecl info (name, bc) =

571translateReg :: Reg -> JS

606translateReg :: Reg -> JS

572translateReg reg

607translateReg reg

573 | RVal <- reg = jsRET

608 | RVal <- reg = jsRET

574− | Tmp <- reg = JSProj (JSIdent "vm") "reg1"

609+ | Tmp <- reg = JSRaw "//TMPREG"

575 | L n <- reg = jsLOC n

610 | L n <- reg = jsLOC n

576 | T n <- reg = jsTOP n

611 | T n <- reg = jsTOP n

577

612

@@ -612,7 +647,7 @@ translateChar ch

612 | '\\' <- ch = "\\\\"

647 | '\\' <- ch = "\\\\"

613 | '\"' <- ch = "\\\""

648 | '\"' <- ch = "\\\""

614 | '\'' <- ch = "\\\'"

649 | '\'' <- ch = "\\\'"

615− | ch `elem` asciiTab = "\\u00" ++ fill (showIntAtBase 16 intToDigit (ord ch) "")

650+ | ch `elem` asciiTab = "\\u00" ++ fill (showHex (ord ch) "")

616 | otherwise = [ch]

651 | otherwise = [ch]

617 where

652 where

618 fill :: String -> String

653 fill :: String -> String

@@ -628,8 +663,8 @@ translateChar ch

628

663

629translateName :: Name -> String

664translateName :: Name -> String

630translateName n = "_idris_" ++ concatMap cchar (showCG n)

665translateName n = "_idris_" ++ concatMap cchar (showCG n)

631− where cchar x | isAlpha x || isDigit x = [x]

666+ where cchar x | isAlphaNum x = [x]

632− | otherwise = "_" ++ show (fromEnum x) ++ "_"

667+ | otherwise = "_" ++ show (fromEnum x) ++ "_"

633

668

634jsASSIGN :: CompileInfo -> Reg -> Reg -> JS

669jsASSIGN :: CompileInfo -> Reg -> Reg -> JS

635jsASSIGN _ r1 r2 = JSAssign (translateReg r1) (translateReg r2)

670jsASSIGN _ r1 r2 = JSAssign (translateReg r1) (translateReg r2)

@@ -1499,6 +1534,5 @@ translateBC info bc

1499 | PROJECT r l a <- bc = jsPROJECT info r l a

1534 | PROJECT r l a <- bc = jsPROJECT info r l a

1500 | OP r o a <- bc = jsOP info r o a

1535 | OP r o a <- bc = jsOP info r o a

1501 | ERROR e <- bc = jsERROR info e

1536 | ERROR e <- bc = jsERROR info e

1502− | otherwise = JSRaw $ show bc

1537+ | otherwise = JSRaw $ "//" ++ show bc

1503− {- PROJECTINTO _ _ _ <- bc = undefined -}

1504

1538

src/IRTS/CodegenLLVM.hs−1

@@ -9,7 +9,6 @@ import qualified Idris.Core.TT as TT

9import Idris.Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)

11import Util.System

12−import Paths_idris

14import LLVM.General.Context

13import LLVM.General.Context

15import LLVM.General.Diagnostic

14import LLVM.General.Diagnostic

src/IRTS/Compiler.hs−2

@@ -47,8 +47,6 @@ import System.Directory

47import System.Environment

48import System.FilePath ((</>), addTrailingPathSeparator)

50−import Paths_idris

51−

52compile :: Codegen -> FilePath -> Term -> Idris ()

50compile :: Codegen -> FilePath -> Term -> Idris ()

53compile codegen f tm

51compile codegen f tm

54 = do checkMVs -- check for undefined metavariables

52 = do checkMVs -- check for undefined metavariables

src/IRTS/System.hs+7−2

@@ -1,6 +1,6 @@

1{-# LANGUAGE CPP #-}

2−module IRTS.System(getTargetDir,getCC,getLibFlags,getIdrisLibDir,

2+module IRTS.System(getDataFileName, getDataDir, getTargetDir,getCC,getLibFlags,getIdrisLibDir,

3− getIncFlags,getMvn,getExecutablePom) where

3+ getIncFlags,getMvn,getExecutablePom, version) where

5import Util.System

@@ -9,7 +9,12 @@ import Data.Maybe (fromMaybe)

9import System.FilePath ((</>), addTrailingPathSeparator)

10import System.Environment

12+#ifdef FREESTANDING

13+import Target_idris

14+import Paths_idris (version)

15+#else

12import Paths_idris

16import Paths_idris

17+#endif

14getCC :: IO String

19getCC :: IO String

15getCC = fromMaybe "gcc" <$> environment "IDRIS_CC"

20getCC = fromMaybe "gcc" <$> environment "IDRIS_CC"

src/Idris/AbsSyntax.hs−2

@@ -14,8 +14,6 @@ import Idris.IdeSlave hiding (Opt(..))

14import IRTS.CodegenCommon

15import Util.DynamicLinker

17−import Paths_idris

18−

19import System.Console.Haskeline

17import System.Console.Haskeline

20import System.IO

18import System.IO

src/Idris/AbsSyntaxTree.hs−2

@@ -15,8 +15,6 @@ import Util.DynamicLinker

16import Idris.Colours

18−import Paths_idris

19−

20import System.Console.Haskeline

18import System.Console.Haskeline

21import System.IO

19import System.IO

src/Idris/DSL.hs−1

@@ -3,7 +3,6 @@

3module Idris.DSL where

5import Idris.AbsSyntax

6−import Paths_idris

8import Idris.Core.TT

7import Idris.Core.TT

9import Idris.Core.Evaluate

8import Idris.Core.Evaluate

src/Idris/ElabDecls.hs−1

@@ -19,7 +19,6 @@ import Idris.PartialEval

19import Idris.DeepSeq

20import Idris.Output (iputStrLn, pshow, iWarn)

21import IRTS.Lang

22−import Paths_idris

24import Idris.Core.TT

23import Idris.Core.TT

25import Idris.Core.Elaborate hiding (Tactic(..))

24import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/IdrisDoc.hs+1−1

@@ -14,7 +14,7 @@ import Idris.AbsSyntax

14import Idris.Docs

15import Idris.Docstrings (nullDocstring)

17−import Paths_idris (getDataFileName)

17+import IRTS.System (getDataFileName)

19import Control.Monad (forM_)

20import Control.Monad.Trans.Error

src/Idris/Imports.hs−1

@@ -4,7 +4,6 @@ import Idris.AbsSyntax

4import Idris.Error

6import Idris.Core.TT

7−import Paths_idris

9import System.FilePath

8import System.FilePath

10import System.Directory

9import System.Directory

src/Idris/REPL.hs+1−1

@@ -34,7 +34,6 @@ import Idris.Interactive

34import Idris.WhoCalls

35import Idris.TypeSearch (searchByType)

37−import Paths_idris

38import Version_idris (gitHash)

37import Version_idris (gitHash)

39import Util.System

38import Util.System

40import Util.DynamicLinker

39import Util.DynamicLinker

@@ -48,6 +47,7 @@ import Idris.Core.Constraints

49import IRTS.Compiler

48import IRTS.Compiler

50import IRTS.CodegenCommon

49import IRTS.CodegenCommon

50+import IRTS.System

52import Data.List.Split (splitOn)

53import qualified Data.Text as T

src/Idris/TypeSearch.hs+96−62

@@ -10,14 +10,15 @@ import Data.Function (on)

10import Data.List (find, minimumBy, partition, sortBy, (\\))

11import Data.Map (Map)

12import qualified Data.Map as M

13−import Data.Maybe (catMaybes, fromMaybe, isJust)

13+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)

14import Data.Monoid (Monoid (mempty, mappend))

15+import qualified Data.PriorityQueue.FingerTree as Q

15import Data.Set (Set)

16import Data.Set (Set)

16import qualified Data.Set as S

17import qualified Data.Set as S

17import qualified Data.Text as T (pack, isPrefixOf)

18import qualified Data.Text as T (pack, isPrefixOf)

19import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

20import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

20−import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,

21+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

21 IState (idris_classes, idris_docstrings, tt_ctxt),

22 IState (idris_classes, idris_docstrings, tt_ctxt),

22 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

23 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

23import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

24import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

@@ -41,7 +42,7 @@ searchByType h pterm = do

41 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

42 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

42 putIState i -- don't actually make any changes

43 putIState i -- don't actually make any changes

43 let names = searchUsing searchPred i ty

44 let names = searchUsing searchPred i ty

44− let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $

45+ let names' = take numLimit $

45 sortBy (compare `on` getScore) names

46 sortBy (compare `on` getScore) names

46 let docs =

47 let docs =

47 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

48 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

@@ -51,7 +52,6 @@ searchByType h pterm = do

51 where

52 where

52 getScore = defaultScoreFunction . snd . snd

53 getScore = defaultScoreFunction . snd . snd

53 numLimit = 50

54 numLimit = 50

54− scoreLimit = 100

55 syn = defaultSyntax { implicitAllowed = True } -- syntax

56 n = sMN 0 "searchType" -- name

@@ -84,10 +84,9 @@ searchUsing pred istate ty =

85-- Our default search predicate.

86searchPred :: IState -> Type -> Type -> Maybe Score

87−searchPred istate ty1 = \ty2 -> case matcher ty2 of

87+searchPred istate ty1 = matcher where

88− xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)

88+ maxScore = 100

89− where

90− matcher = unifyWithHoles istate ty1

89+ matcher = unifyWithHoles istate maxScore ty1

93typeFromDef :: (Def, b, c, d) -> Maybe Type

92typeFromDef :: (Def, b, c, d) -> Maybe Type

@@ -218,36 +217,53 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG

218inArgTys = map . first . second

217inArgTys = map . first . second

219

218

220

219

220+typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

221+typeclassUnify classInfo ctxt ty tyTry = do

222+ res <- tcToMaybe $ match_unify ctxt [] ty retTy [] holes []

223+ guard $ null (holes \\ map fst res)

224+ let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs

225+ return argTys'

226+ where

227+ tyTry' = vToP tyTry

228+ holes = map fst nonTcArgs

229+ retTy = getRetTy tyTry'

230+ (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'

231+

232+isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool

233+isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where

234+ (clss, args) = unApply ty

235+ getClassName (P (TCon _ _) className _) = [className]

236+ getClassName _ = []

237+

238+

239+instance Ord Score where

240+ compare = compare `on` defaultScoreFunction

241+

221--DONT run vToP first!

242--DONT run vToP first!

222-- | Try to match two types together in a unification-like procedure.

243-- | Try to match two types together in a unification-like procedure.

223-- Returns a list of possible scores representing ways in which the two

244-- Returns a list of possible scores representing ways in which the two

224-- types can be matched.

245-- types can be matched.

225−unifyWithHoles :: IState -> Type -> Type -> [Score]

246+unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score

226−unifyWithHoles istate type1 = \type2 -> let

247+unifyWithHoles istate maxScore type1 = \type2 -> let

227 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)

248 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)

228 argNames2 = map (fst . fst) dag2

249 argNames2 = map (fst . fst) dag2

229 startingHoles = argNames1 ++ argNames2

250 startingHoles = argNames1 ++ argNames2

230

251

231 startingTypes = (retTy1, retTy2) : []

252 startingTypes = (retTy1, retTy2) : []

253+ in do

232− in case unifyQueue (State startingHoles dag1 dag2

254+ state <- unifyQueue (State startingHoles dag1 dag2

233 typeClassArgs1 typeClassArgs2

255 typeClassArgs1 typeClassArgs2

234 mempty startingHoles) startingTypes

256 mempty startingHoles) startingTypes

235− of Nothing -> []

257+ getResults (Q.singleton (score state) state)

236− Just state -> possibleMatches state

237 where

258 where

238 ctxt = tt_ctxt istate

259 ctxt = tt_ctxt istate

239 classInfo = idris_classes istate

260 classInfo = idris_classes istate

240

261

241− isTypeClassArg :: Type -> Bool

242− isTypeClassArg ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where

243− (clss, args) = unApply ty

244− getClassName (P (TCon _ _) className _) = [className]

245− getClassName _ = []

246−

247 (dag1, typeClassArgs1, retTy1) = makeDag type1

262 (dag1, typeClassArgs1, retTy1) = makeDag type1

248 argNames1 = map (fst . fst) dag1

263 argNames1 = map (fst . fst) dag1

249 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)

264 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)

250− makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP isTypeClassArg . vToP

265+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .

266+ computeDagP (isTypeClassArg classInfo) . vToP

251 first3 f (a,b,c) = (f a, b, c)

267 first3 f (a,b,c) = (f a, b, c)

252

268

253 -- update our state with the unification resolutions

269 -- update our state with the unification resolutions

@@ -278,9 +294,13 @@ unifyWithHoles istate type1 = \type2 -> let

278 (Nothing, Nothing) -> nextStep

294 (Nothing, Nothing) -> nextStep

279 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

295 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

280 where

296 where

297+ varsInTy = map fst $ M.toList (usedVars term) --[]

298+ toDelete = name : varsInTy

299+ deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]

300+

281 inScore f state = state { score = f (score state) }

301 inScore f state = state { score = f (score state) }

282− state' = modifyTypes (subst name term) . deleteLeft name . deleteRight name $

302+ state' = modifyTypes (subst name term) . deleteMany $

283− state { holes = holes \\ [name]}

303+ state { holes = holes \\ toDelete }

284 nextStep = resolveUnis xs state'

304 nextStep = resolveUnis xs state'

285

305

286

306

@@ -288,12 +308,13 @@ unifyWithHoles istate type1 = \type2 -> let

288 unifyQueue :: State -> [(Type, Type)] -> Maybe State

308 unifyQueue :: State -> [(Type, Type)] -> Maybe State

289 unifyQueue state [] = return state

309 unifyQueue state [] = return state

290 unifyQueue state ((ty1, ty2) : queue) = do

310 unifyQueue state ((ty1, ty2) : queue) = do

311+ --trace ("go: \n" ++ show state) True `seq` return ()

291 res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []

312 res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []

292 (state', queueAdditions) <- resolveUnis res state

313 (state', queueAdditions) <- resolveUnis res state

293 guard $ scoreCriterion (score state')

314 guard $ scoreCriterion (score state')

294 unifyQueue state' (queue ++ queueAdditions)

315 unifyQueue state' (queue ++ queueAdditions)

295

316

296− possClassInstances :: [Name] -> Type -> [([(Name, Type)], Type)]

317+ possClassInstances :: [Name] -> Type -> [Type]

297 possClassInstances usedNames ty = do

318 possClassInstances usedNames ty = do

298 className <- getClassName clss

319 className <- getClassName clss

299 classDef <- lookupCtxt className classInfo

320 classDef <- lookupCtxt className classInfo

@@ -301,57 +322,70 @@ unifyWithHoles istate type1 = \type2 -> let

301 def <- lookupCtxt n (definitions ctxt)

322 def <- lookupCtxt n (definitions ctxt)

302 ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

323 ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

303 let ty' = vToP (uniqueBinders usedNames ty)

324 let ty' = vToP (uniqueBinders usedNames ty)

304− return (getArgTys ty', getRetTy ty')

325+ return ty'

305 where

326 where

306− (clss, args) = unApply ty

327+ (clss, _) = unApply ty

307 getClassName (P (TCon _ _) className _) = [className]

328 getClassName (P (TCon _ _) className _) = [className]

308 getClassName _ = []

329 getClassName _ = []

309

330

331+

332+ getResults :: Q.PQueue Score State -> Maybe Score

333+ getResults queue = do

334+ ((nextScore, next), rest) <- Q.minViewWithKey queue

335+ if isFinal next

336+ then return nextScore

337+ else do

338+ guard (defaultScoreFunction nextScore <= maxScore)

339+ let additions = if scoreCriterion nextScore

340+ then Q.fromList [ (score state, state) | state <- nextSteps next ]

341+ else Q.empty

342+ getResults (Q.union rest additions)

343+ where

344+ isFinal (State [] [] [] [] [] score _) = True

345+ isFinal _ = False

346+

310 -- | Find all possible matches starting from a given state.

347 -- | Find all possible matches starting from a given state.

311− possibleMatches :: State -> [Score]

348+ -- We go in stages rather than concatenating all three results in hopes of narrowing

312− possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]

349+ -- the search tree. Once we advance in a phase, there should be no going back.

350+ nextSteps :: State -> [State]

351+

352+ -- Stage 2 - match typeclasses

353+ nextSteps (State [] [] [] c1 c2 scoreAcc usedNames) =

354+ if null results2 then results3 else results2

355+ where

356+ -- try to match a typeclass argument from the left with a typeclass argument from the right

357+ results2 =

358+ catMaybes [ unifyQueue (State [] [] []

359+ (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]

360+ | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

361+

362+ -- try to hunt match a typeclass constraint by replacing it with an instance

363+ results3 = results3A ++ results3B

364+ typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]

365+ results3A = [ State [] [] []

366+ (deleteFromArgList n c1 ++ newClassArgs) c2

367+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))

368+ (usedNames ++ newHoles)

369+ | ((n, ty), inst) <- typeClassArgs c1

370+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst

371+ , let newHoles = map fst newClassArgs ]

372+ results3B = [ State [] [] []

373+ c1 (deleteFromArgList n c2 ++ newClassArgs)

374+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))

375+ (usedNames ++ newHoles)

376+ | ((n, ty), inst) <- typeClassArgs c2

377+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst

378+ , let newHoles = map fst newClassArgs ]

379+

380+ -- Stage 1 - match arguments

313− possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) =

381+ nextSteps (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = results1 where

314− concat [ possibleMatches state | state <- results, scoreCriterion (score state) ] where

315

382

316 -- we only try to match arguments whose names don't appear in the types

383 -- we only try to match arguments whose names don't appear in the types

317 -- of any other arguments

384 -- of any other arguments

318 canBeFirst :: ArgsDAG -> [(Name, Type)]

385 canBeFirst :: ArgsDAG -> [(Name, Type)]

319 canBeFirst = map fst . filter (S.null . snd . snd)

386 canBeFirst = map fst . filter (S.null . snd . snd)

320

387

321− -- this is done rather than concatenating all three results in hopes of narrowing

322− -- the search tree

323− results = fromMaybe [] $ find (not . null) [results1, results2, results3]

324−

325 -- try to match an argument from the left with an argument from the right

388 -- try to match an argument from the left with an argument from the right

326 results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)

389 results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)

327 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]

390 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]

328 | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

391 | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

329−

330− -- try to match a typeclass argument from the left with a typeclass argument from the right

331− results2 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) dag1 (inArgTys subst2for1 dag2)

332− (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]

333− | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

334−

335− -- try to hunt match a typeclass constraint by replacing it with an instance

336− results3 = if null dag1 || null dag2 then catMaybes (results3A ++ results3B) else []

337− typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]

338− noDeps (n, ty) = ((n, ty), (0, S.empty))

339− results3A = [ unifyQueue

340− (State ((holes \\ [n]) ++ newHoles) (dag1 ++ map noDeps newNonClassArgs) dag2

341− (deleteFromArgList n c1 ++ newClassArgs) c2

342− (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))

343− (usedNames ++ newHoles)

344− )

345− [(ty, inst)]

346− | ((n, ty), (newArgs, inst)) <- typeClassArgs c1, let newHoles = map fst newArgs

347− , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]

348− results3B = [ unifyQueue

349− (State ((holes \\ [n]) ++ newHoles) dag1 (dag2 ++ map noDeps newNonClassArgs)

350− c1 (deleteFromArgList n c2 ++ newClassArgs)

351− (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))

352− (usedNames ++ newHoles)

353− )

354− [(ty, inst)]

355− | ((n, ty), (newArgs, inst)) <- typeClassArgs c2, let newHoles = map fst newArgs

356− , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]

357−

src/Pkg/PParser.hs−2

@@ -10,8 +10,6 @@ import Idris.AbsSyntaxTree

10import Idris.ParseHelpers

11import Idris.CmdOptions

13−import Paths_idris

14−

15import Control.Monad.State.Strict

13import Control.Monad.State.Strict

16import Control.Applicative

14import Control.Applicative

src/Pkg/Package.hs−2

@@ -29,8 +29,6 @@ import IRTS.System

30import Pkg.PParser

32−import Paths_idris (getDataDir)

33−

34-- To build a package:

32-- To build a package:

35-- * read the package description

33-- * read the package description

36-- * check all the library dependencies exist

34-- * check all the library dependencies exist