41f3d97 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstring

41f3d97Benjamin Saunders14 years ago

CHANGELOG+4−1

compare with master

unifiedsplit

@@ -22,12 +22,15 @@ User visible changes:

22* Added System.Concurrency modules

23* Added 'postulate' declarations

24* Allow type annotations on 'let' tactic

25+* EXPERIMENTAL JavaScript generation, with '--target javascript' option

26Internal changes:

27Internal changes:

28* Separate inlining methods at compile-time and run-time

29* Separate inlining methods at compile-time and run-time

29* Fixed nested parameters blocks

30* Fixed nested parameters blocks

30−* Improve efficiency of elaborator by only normalising when necessary

31+* Improve efficiency of elaborator by:

32+ - only normalising when necessary

33+ - reducing backtracking with resolving ambiguities

31* Better compilation of case trees

34* Better compilation of case trees

33New in 0.9.5:

36New in 0.9.5:

CONTRIBUTORSnew file+23

@@ -0,0 +1,23 @@

1+Thanks to the following for their help and contributions:

3+Ozgur Akgun

4+Nicola Botta

5+Edwin Brady

6+Jason Dagit

7+Cezar Ionescu

8+Irene Knapp

9+Mathnerd314

10+Mekeor Melire

11+Melissa Mozifian

12+Dominic Mulligan

13+raichoo

14+Tom Prince

15+Seo Sanghyeon

16+Benjamin Saunders

17+startling

18+Chetan T

19+Dirk Ullrich

20+Leif Warner

21+Daniel Waterworth

22+Jonas Westerlund

23+

idris.cabal+3−2

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.5.2

2+Version: 0.9.6

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -51,7 +51,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr

51 lib/Network/*.idr lib/Control/*.idr

52 lib/Control/Monad/*.idr lib/Language/*.idr

53 lib/System/Concurrency/*.idr

54− lib/Data/*.idr

54+ lib/Data/*.idr lib/Debug/*.idr

55 tutorial/examples/*.idr lib/base.ipkg

56 config.mk

57 rts/*.c rts/*.h rts/Makefile

@@ -84,6 +84,7 @@ Executable idris

84 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

85 IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,

86 IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,

87+ IRTS.CodegenJavaScript,

87 IRTS.CodegenCommon, IRTS.DumpBC

88 IRTS.CodegenCommon, IRTS.DumpBC

89 Paths_idris

90 Paths_idris

lib/Builtins.idr+4−1

@@ -19,6 +19,9 @@ replace refl prf = prf

19sym : {l:a} -> {r:a} -> l = r -> r = l

20sym refl = refl

22+trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c

23+trans refl refl = refl

24+

22lazy : a -> a

25lazy : a -> a

23lazy x = x -- compiled specially

26lazy x = x -- compiled specially

@@ -40,7 +43,7 @@ namespace Builtins {

40id : a -> a

43id : a -> a

41id x = x

44id x = x

43−the : (A : Type) -> A -> A

46+the : (a : Type) -> a -> a

44the _ = id

47the _ = id

46const : a -> b -> a

49const : a -> b -> a

lib/Language/Reflection.idr+9−1

@@ -1,7 +1,7 @@

1module Language.Reflection

3TTName : Type

4−TTName = String

4+TTName = String -- needs to capture namespaces too...

6data TT = Var TTName

7 | Lam TTName TT TT

@@ -9,3 +9,11 @@ data TT = Var TTName

9 | Let TTName TT TT TT

10 | App TTName TT TT

12+data Tactic = Try Tactic Tactic

13+ | GoalType TTName Tactic -- only run if the goal has the right type

14+ | Refine TTName

15+ | Seq Tactic Tactic

16+ | Trivial

17+ | Solve

18+ | Exact TT -- not yet implemented

19+

lib/Prelude/Maybe.idr+26

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

1module Prelude.Maybe

3import Builtins

4+import Prelude.Algebra

5+import Prelude.Cast

7+%access public

8+%default total

5data Maybe a

10data Maybe a

6 = Nothing

11 = Nothing

@@ -41,3 +46,24 @@ toMaybe False j = Nothing

41maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b

46maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b

42maybe_bind Nothing k = Nothing

47maybe_bind Nothing k = Nothing

43maybe_bind (Just x) k = k x

48maybe_bind (Just x) k = k x

49+

50+-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to

51+-- <http://en.wikipedia.org/wiki/Monoid>: \"Any semigroup S may be

52+-- turned into a monoid simply by adjoining an element e not in S

53+-- and defining i+i = i and i+s = s = s+i for all s ∈ S.\"

54+

55+instance (Semigroup a) => Semigroup (Maybe a) where

56+ Nothing <+> m = m

57+ m <+> Nothing = m

58+ (Just m1) <+> (Just m2) = Just (m1 <+> m2)

59+

60+instance (Monoid a) => Monoid (Maybe a) where

61+ neutral = Nothing

62+

63+

64+instance (Monoid a, Eq a) => Cast a (Maybe a) where

65+ cast x = if x == neutral then Nothing else Just x

66+

67+instance (Monoid a) => Cast (Maybe a) a where

68+ cast Nothing = neutral

69+ cast (Just x) = x

papers/impl-paper/impldtp.tex+4−1

@@ -54,7 +54,10 @@

56\title

57+[Idris, a General Purpose Dependently Typed Programm Language]

58+{Idris, a General Purpose Dependently Typed Programming Language:

59+Design and Implementation}

57− {Implementing General Purpose Dependently Typed Programming Languages}

60+%Implementing General Purpose Dependently Typed Programming Languages}

58%\subtitle{Implementing Domain Specific Languages by Overloading}

61%\subtitle{Implementing Domain Specific Languages by Overloading}

60\author[Edwin Brady]

63\author[Edwin Brady]

src/Core/CaseTree.hs+1−1

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

1−{-# LANGUAGE PatternGuards, DeriveFunctor #-}

1+{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

3module Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

4 Phase(..), CaseTree,

src/Core/CoreParser.hs−4

@@ -55,12 +55,10 @@ lexWS = do i <- getInput

56 simpleSpace = skipMany1 (satisfy isSpace)

57 oneLineComment = do try (do string ("--")

58− skipMany simpleSpace

59 satisfy (\x -> x /= '|' && x /= '^'))

58 satisfy (\x -> x /= '|' && x /= '^'))

60 skipMany (satisfy (/= '\n'))

59 skipMany (satisfy (/= '\n'))

61 return ()

60 return ()

62 multiLineComment = do try (do string "{-"

61 multiLineComment = do try (do string "{-"

63− skipMany simpleSpace

64 satisfy (\x -> x /= '|' && x /= '^'))

62 satisfy (\x -> x /= '|' && x /= '^'))

65 inCommentMulti

63 inCommentMulti

@@ -136,7 +134,6 @@ mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

136pDocComment :: Char -> CParser a String

134pDocComment :: Char -> CParser a String

137pDocComment c

135pDocComment c

138 = try (do string ("--")

136 = try (do string ("--")

139− option ' ' (lchar ' ')

140 char c

137 char c

141 skipMany simpleSpace

138 skipMany simpleSpace

142 i <- getInput

139 i <- getInput

@@ -145,7 +142,6 @@ pDocComment c

145 whiteSpace

142 whiteSpace

146 return doc)

143 return doc)

147 <|> try (do string ("{-")

144 <|> try (do string ("{-")

148− option ' ' (lchar ' ')

149 char c

145 char c

150 skipMany simpleSpace

146 skipMany simpleSpace

151 i <- getInput

147 i <- getInput

src/Core/Elaborate.hs+21−5

@@ -155,8 +155,16 @@ get_inj = do ES p _ _ <- get

155 return (injective (fst p))

156

157checkInjective :: (Term, Term, Term) -> Elab' aux ()

158−checkInjective (tm, l, r) = if isInjective tm then return ()

158+checkInjective (tm, l, r) = do ctxt <- get_context

159+ if isInj ctxt tm then return ()

159 else lift $ tfail (NotInjective tm l r)

160 else lift $ tfail (NotInjective tm l r)

161+ where isInj ctxt (P _ n _)

162+ | isConName Nothing n ctxt = True

163+ isInj ctxt (App f a) = isInj ctxt f

164+ isInj ctxt (Constant _) = True

165+ isInj ctxt (TType _) = True

166+ isInj ctxt (Bind _ (Pi _) sc) = True

167+ isInj ctxt _ = False

160

168

161-- get instance argument names

169-- get instance argument names

162get_instances :: Elab' aux [Name]

170get_instances :: Elab' aux [Name]

@@ -236,6 +244,9 @@ regret = processTactic' Regret

236compute :: Elab' aux ()

244compute :: Elab' aux ()

237compute = processTactic' Compute

245compute = processTactic' Compute

238

246

247+hnf_compute :: Elab' aux ()

248+hnf_compute = processTactic' HNF_Compute

249+

239eval_in :: Raw -> Elab' aux ()

250eval_in :: Raw -> Elab' aux ()

240eval_in t = processTactic' (EvalIn t)

251eval_in t = processTactic' (EvalIn t)

241

252

@@ -366,7 +377,8 @@ apply fn imps =

366 map fst (filter (not.snd) (zip args (map fst imps)))

377 map fst (filter (not.snd) (zip args (map fst imps)))

367 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

378 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

368 unified p

379 unified p

380+ let unify = -- trace ("Not done " ++ show hs) $

369− let unify = dropGiven dont hs

381+ dropGiven dont hs

370 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

382 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

371 ptm <- get_term

383 ptm <- get_term

372 end_unify

384 end_unify

@@ -398,7 +410,7 @@ apply_elab n args =

398 do ty <- get_type (Var n)

410 do ty <- get_type (Var n)

399 ctxt <- get_context

411 ctxt <- get_context

400 env <- get_env

412 env <- get_env

401− claims <- doClaims (normalise ctxt env ty) args []

413+ claims <- doClaims (hnf ctxt env ty) args []

402 prep_fill n (map fst claims)

414 prep_fill n (map fst claims)

403 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

415 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

404 elabClaims [] False claims

416 elabClaims [] False claims

@@ -476,11 +488,15 @@ arg n tyhole = do ty <- unique_hole tyhole

476

488

477-- Try a tactic, if it fails, try another

489-- Try a tactic, if it fails, try another

478try :: Elab' aux a -> Elab' aux a -> Elab' aux a

490try :: Elab' aux a -> Elab' aux a -> Elab' aux a

491+try t1 t2 = try' t1 t2 False

492+

493+try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

494+try' t1 t2 proofSearch

479−try t1 t2 = do s <- get

495+ = do s <- get

480 case runStateT t1 s of

496 case runStateT t1 s of

481 OK (v, s') -> do put s'

497 OK (v, s') -> do put s'

482 return v

498 return v

483− Error e1 -> if recoverableErr e1 then

499+ Error e1 -> if proofSearch || recoverableErr e1 then

484 do case runStateT t2 s of

500 do case runStateT t2 s of

485 OK (v, s') -> do put s'; return v

501 OK (v, s') -> do put s'; return v

486 Error e2 -> if score e1 >= score e2

502 Error e2 -> if score e1 >= score e2

src/Core/Evaluate.hs+32−51

@@ -19,29 +19,14 @@ import Data.Binary hiding (get, put)

19import Core.TT

20import Core.CaseTree

22−data EvalState = ES { limited :: [(Name, Int)],

22+data EvalState = ES { limited :: [(Name, Int)] }

23− steps :: Int -- number of applications/let reductions

24− }

25−

26−-- Evaluation fails if we hit a boredom threshold - in which case, just return

27−-- the original (capture the failure in a Maybe)

29type Eval a = State EvalState a

24type Eval a = State EvalState a

31data EvalOpt = Spec | HNF | Simplify Bool | AtREPL

26data EvalOpt = Spec | HNF | Simplify Bool | AtREPL

32 deriving (Show, Eq)

27 deriving (Show, Eq)

34−initEval = ES [] 0

29+initEval = ES []

35−

36−step :: Int -> Eval ()

37−step max = do e <- get

38− put (e { steps = steps e + 1 })

39− if steps e > max then fail "Threshold exceeded"

40− else return ()

41−

42−getSteps :: Eval Int

43−getSteps = do e <- get

44− return (steps e)

46-- VALUES (as HOAS) ---------------------------------------------------------

31-- VALUES (as HOAS) ---------------------------------------------------------

@@ -77,18 +62,15 @@ instance Show (a -> b) where

77-- i.e. it's an intermediate environment that we have while type checking or

62-- i.e. it's an intermediate environment that we have while type checking or

78-- while building a proof.

63-- while building a proof.

80−threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking

81− -- in fact it's a maximum recursion depth

82−

83-- Normalise fully type checked terms (so, assume all names/let bindings resolved)

65-- Normalise fully type checked terms (so, assume all names/let bindings resolved)

84normaliseC :: Context -> Env -> TT Name -> TT Name

66normaliseC :: Context -> Env -> TT Name -> TT Name

85normaliseC ctxt env t

67normaliseC ctxt env t

86− = evalState (do val <- eval False ctxt threshold [] env t []

68+ = evalState (do val <- eval False ctxt [] env t []

87 quote 0 val) initEval

69 quote 0 val) initEval

89normaliseAll :: Context -> Env -> TT Name -> TT Name

71normaliseAll :: Context -> Env -> TT Name -> TT Name

90normaliseAll ctxt env t

72normaliseAll ctxt env t

91− = evalState (do val <- eval False ctxt threshold [] env t [AtREPL]

73+ = evalState (do val <- eval False ctxt [] env t [AtREPL]

92 quote 0 val) initEval

74 quote 0 val) initEval

94normalise :: Context -> Env -> TT Name -> TT Name

76normalise :: Context -> Env -> TT Name -> TT Name

@@ -96,12 +78,12 @@ normalise = normaliseTrace False

97normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name

79normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name

98normaliseTrace tr ctxt env t

80normaliseTrace tr ctxt env t

99− = evalState (do val <- eval tr ctxt threshold [] (map finalEntry env) (finalise t) []

81+ = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []

100 quote 0 val) initEval

82 quote 0 val) initEval

101

102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

84specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

103specialise ctxt env limits t

85specialise ctxt env limits t

104− = evalState (do val <- eval False ctxt threshold limits (map finalEntry env) (finalise t) []

86+ = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []

105 quote 0 val) (initEval { limited = limits })

87 quote 0 val) (initEval { limited = limits })

106

107-- Like normalise, but we only reduce functions that are marked as okay to

89-- Like normalise, but we only reduce functions that are marked as okay to

@@ -109,7 +91,7 @@ specialise ctxt env limits t

109

110simplify :: Context -> Bool -> Env -> TT Name -> TT Name

92simplify :: Context -> Bool -> Env -> TT Name -> TT Name

111simplify ctxt runtime env t

93simplify ctxt runtime env t

112− = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0),

94+ = evalState (do val <- eval False ctxt [(UN "lazy", 0),

113 (UN "par", 0),

95 (UN "par", 0),

114 (UN "fork", 0)]

96 (UN "fork", 0)]

115 (map finalEntry env) (finalise t)

97 (map finalEntry env) (finalise t)

@@ -118,7 +100,9 @@ simplify ctxt runtime env t

118

100

119hnf :: Context -> Env -> TT Name -> TT Name

101hnf :: Context -> Env -> TT Name -> TT Name

120hnf ctxt env t

102hnf ctxt env t

121− = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]

103+ = evalState (do val <- eval False ctxt []

104+ (map finalEntry env)

105+ (finalise t) [HNF]

122 quote 0 val) initEval

106 quote 0 val) initEval

123

107

124

108

@@ -146,31 +130,27 @@ usable s n ns = case lookup n ns of

146 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

130 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

147 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

131 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

148

132

149−reduction :: Eval ()

150−reduction = do ES ns s <- get

151− put (ES ns (s+1))

152−

153-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

133-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

154-- such as we might have during construction of a proof)

134-- such as we might have during construction of a proof)

155

135

156−eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->

136+eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

157 [EvalOpt] -> Eval Value

137 [EvalOpt] -> Eval Value

158−eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

138+eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

159 spec = Spec `elem` opts

139 spec = Spec `elem` opts

160 simpl = Simplify True `elem` opts

140 simpl = Simplify True `elem` opts

161 atRepl = AtREPL `elem` opts

141 atRepl = AtREPL `elem` opts

142+ hnf = HNF `elem` opts

162

143

163 canSimplify inl inr n stk

144 canSimplify inl inr n stk

164 = (Simplify False `elem` opts && (not inl || elem n stk))

145 = (Simplify False `elem` opts && (not inl || elem n stk))

165 || (Simplify True `elem` opts && (not inr || elem n stk))

146 || (Simplify True `elem` opts && (not inr || elem n stk))

166

147

167 ev ntimes stk top env (P _ n ty)

148 ev ntimes stk top env (P _ n ty)

168− | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

169− ev ntimes stk top env v

149+ | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

170 ev ntimes_in stk top env (P Ref n ty)

150 ev ntimes_in stk top env (P Ref n ty)

151+ | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

171 | (True, ntimes) <- usable simpl n ntimes_in

152 | (True, ntimes) <- usable simpl n ntimes_in

172 = do let val = lookupDefAcc Nothing n atRepl ctxt

153 = do let val = lookupDefAcc Nothing n atRepl ctxt

173− when (not atRepl) $ step maxred

174 case val of

154 case val of

175 [(Function _ tm, Public)] ->

155 [(Function _ tm, Public)] ->

176 ev ntimes (n:stk) True env tm

156 ev ntimes (n:stk) True env tm

@@ -191,13 +171,11 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

191 ev ntimes stk top env (Bind n (Let t v) sc)

171 ev ntimes stk top env (Bind n (Let t v) sc)

192-- | not simpl || vinstances 0 sc < 2

172-- | not simpl || vinstances 0 sc < 2

193 = do v' <- ev ntimes stk top env v --(finalise v)

173 = do v' <- ev ntimes stk top env v --(finalise v)

194− when (not atRepl) $ step maxred

195 sc' <- ev ntimes stk top (v' : env) sc

174 sc' <- ev ntimes stk top (v' : env) sc

196 wknV (-1) sc'

175 wknV (-1) sc'

197{- | otherwise -- put this back when the Bind works properly

176{- | otherwise -- put this back when the Bind works properly

198 = do t' <- ev ntimes stk top env t

177 = do t' <- ev ntimes stk top env t

199 v' <- ev ntimes stk top env v --(finalise v)

178 v' <- ev ntimes stk top env v --(finalise v)

200− when (not atRepl) $ step maxred

201 -- use Tmp as a placeholder, then make it a variable reference

179 -- use Tmp as a placeholder, then make it a variable reference

202 -- again when evaluation finished

180 -- again when evaluation finished

203 sc' <- ev ntimes stk top (v' : env) sc

181 sc' <- ev ntimes stk top (v' : env) sc

@@ -205,13 +183,11 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

205 ev ntimes stk top env (Bind n (NLet t v) sc)

183 ev ntimes stk top env (Bind n (NLet t v) sc)

206 = do t' <- ev ntimes stk top env (finalise t)

184 = do t' <- ev ntimes stk top env (finalise t)

207 v' <- ev ntimes stk top env (finalise v)

185 v' <- ev ntimes stk top env (finalise v)

208− when (not atRepl) $ step maxred

209 sc' <- ev ntimes stk top (v' : env) sc

186 sc' <- ev ntimes stk top (v' : env) sc

210 return $ VBind n (Let t' v') (\x -> return sc')

187 return $ VBind n (Let t' v') (\x -> return sc')

211 ev ntimes stk top env (Bind n b sc)

188 ev ntimes stk top env (Bind n b sc)

212 = do b' <- vbind env b

189 = do b' <- vbind env b

213− when (not atRepl) $ step maxred

214− return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

190+ return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)

215 where vbind env t

191 where vbind env t

216 | simpl

192 | simpl

217 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

193 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

@@ -222,9 +198,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

222-- | laz == UN "lazy"

198-- | laz == UN "lazy"

223-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a

199-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a

224 ev ntimes stk top env (App f a)

200 ev ntimes stk top env (App f a)

225− = do f' <- ev ntimes stk top env f

201+ = do f' <- ev ntimes stk False env f

226 a' <- ev ntimes stk False env a

202 a' <- ev ntimes stk False env a

227− when (not atRepl) $ step maxred

228 evApply ntimes stk top env [a'] f'

203 evApply ntimes stk top env [a'] f'

229 ev ntimes stk top env (Constant c) = return $ VConstant c

204 ev ntimes stk top env (Constant c) = return $ VConstant c

230 ev ntimes stk top env Erased = return VErased

205 ev ntimes stk top env Erased = return VErased

@@ -232,18 +207,18 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

232

207

233 evApply ntimes stk top env args (VApp f a) =

208 evApply ntimes stk top env args (VApp f a) =

234 evApply ntimes stk top env (a:args) f

209 evApply ntimes stk top env (a:args) f

235− evApply ntimes stk top env args f = do when (not atRepl) $ step maxred

236− apply ntimes stk top env f args

210+ evApply ntimes stk top env args f = apply ntimes stk top env f args

237

211

238− apply ntimes stk top env f as

239− | length stk > threshold = return $ unload env f as

240 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)

212 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)

241 = do a' <- sc a

213 = do a' <- sc a

242 app <- apply ntimes stk top env a' as

214 app <- apply ntimes stk top env a' as

243 wknV (-1) app

215 wknV (-1) app

244-- apply ntimes stk False env f args

216-- apply ntimes stk False env f args

245-- | spec = specApply ntimes stk env f args

217-- | spec = specApply ntimes stk env f args

246− apply ntimes_in stk top env f@(VP Ref n ty) args

218+ apply ntimes_in stk top env f@(VP Ref n ty) args

219+ | not top && hnf = case args of

220+ [] -> return f

221+ _ -> return $ unload env f args

247 | (True, ntimes) <- usable simpl n ntimes_in

222 | (True, ntimes) <- usable simpl n ntimes_in

248 = traceWhen traceon (show stk) $

223 = traceWhen traceon (show stk) $

249 do let val = lookupDefAcc Nothing n atRepl ctxt

224 do let val = lookupDefAcc Nothing n atRepl ctxt

@@ -284,7 +259,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

284 | length ns <= length args

259 | length ns <= length args

285 = do let args' = take (length ns) args

260 = do let args' = take (length ns) args

286 let rest = drop (length ns) args

261 let rest = drop (length ns) args

287− t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree

262+ t <- evTree ntimes stk top env

263+ (zipWith (\n t -> (n, t)) ns args') tree

288 return (t, rest)

264 return (t, rest)

289 | otherwise = return (Nothing, args)

265 | otherwise = return (Nothing, args)

290

266

@@ -293,7 +269,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

293 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing

269 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing

294 evTree ntimes stk top env amap (STerm tm)

270 evTree ntimes stk top env amap (STerm tm)

295 = do let etm = pToVs (map fst amap) tm

271 = do let etm = pToVs (map fst amap) tm

272+ etm' <- ev ntimes stk (not (conHeaded tm))

296− etm' <- ev ntimes stk top (map snd amap ++ env) etm

273+ (map snd amap ++ env) etm

297 return $ Just etm'

274 return $ Just etm'

298 evTree ntimes stk top env amap (Case n alts)

275 evTree ntimes stk top env amap (Case n alts)

299 = case lookup n amap of

276 = case lookup n amap of

@@ -306,6 +283,10 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

306 _ -> return Nothing

283 _ -> return Nothing

307 _ -> return Nothing

284 _ -> return Nothing

308

285

286+ conHeaded tm@(App _ _)

287+ | (P (DCon _ _) _ _, args) <- unApply tm = True

288+ conHeaded t = False

289+

309 chooseAlt' ntimes stk env _ (f, args) alts amap

290 chooseAlt' ntimes stk env _ (f, args) alts amap

310 = do f' <- apply ntimes stk True env f args

291 = do f' <- apply ntimes stk True env f args

311 chooseAlt env f' (getValArgs f') alts amap

292 chooseAlt env f' (getValArgs f') alts amap

@@ -542,7 +523,7 @@ convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool

542convEq ctxt = ceq [] where

523convEq ctxt = ceq [] where

543 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool

524 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool

544 ceq ps (P xt x _) (P yt y _)

525 ceq ps (P xt x _) (P yt y _)

545− | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True

526+ | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

546 | otherwise = sameDefs ps x y

527 | otherwise = sameDefs ps x y

547 ceq ps (V x) (V y) = return (x == y)

528 ceq ps (V x) (V y) = return (x == y)

548 ceq ps (Bind _ xb xs) (Bind _ yb ys)

529 ceq ps (Bind _ xb xs) (Bind _ yb ys)

@@ -685,7 +666,7 @@ initContext = MkContext [] 0 emptyContext

685ctxtAlist :: Context -> [(Name, Def)]

666ctxtAlist :: Context -> [(Name, Def)]

686ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

667ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

687

668

688−veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval

669+veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

689

670

690addToCtxt :: Name -> Term -> Type -> Context -> Context

671addToCtxt :: Name -> Term -> Type -> Context -> Context

691addToCtxt n tm ty uctxt

672addToCtxt n tm ty uctxt

src/Core/ProofState.hs+11−3

@@ -54,6 +54,7 @@ data Tactic = Attack

54 | StartUnify Name

55 | EndUnify

56 | Compute

57+ | HNF_Compute

57 | EvalIn Raw

58 | EvalIn Raw

58 | CheckIn Raw

59 | CheckIn Raw

59 | Intro (Maybe Name)

60 | Intro (Maybe Name)

@@ -387,7 +388,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

387 Nothing -> x

388 Nothing -> x

388 let t' = case t of

389 let t' = case t of

389 x@(Bind y (Pi s) _) -> x

390 x@(Bind y (Pi s) _) -> x

390− _ -> normalise ctxt env t

391+ _ -> hnf ctxt env t

391 (tyv, tyt) <- lift $ check ctxt env ty

392 (tyv, tyt) <- lift $ check ctxt env ty

392-- ns <- lift $ unify ctxt env tyv t'

393-- ns <- lift $ unify ctxt env tyv t'

393 case t' of

394 case t' of

@@ -407,7 +408,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

407 Nothing -> x

408 Nothing -> x

408 let t' = case t of

409 let t' = case t of

409 x@(Bind y (Pi s) _) -> x

410 x@(Bind y (Pi s) _) -> x

410− _ -> normalise ctxt env t

411+ _ -> hnf ctxt env t

411 case t' of

412 case t' of

412 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

413 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

413 let t' = instantiate (P Bound n s) (pToV y t) in

414 let t' = instantiate (P Bound n s) (pToV y t) in

@@ -477,7 +478,7 @@ patbind :: Name -> RunTactic

477patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

478patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

478 do let t' = case t of

479 do let t' = case t of

479 x@(Bind y (PVTy s) t) -> x

480 x@(Bind y (PVTy s) t) -> x

480− _ -> normalise ctxt env t

481+ _ -> hnf ctxt env t

481 case t' of

482 case t' of

482 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

483 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

483 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

484 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

@@ -488,6 +489,12 @@ compute :: RunTactic

488compute ctxt env (Bind x (Hole ty) sc) =

489compute ctxt env (Bind x (Hole ty) sc) =

489 do return $ Bind x (Hole (normalise ctxt env ty)) sc

490 do return $ Bind x (Hole (normalise ctxt env ty)) sc

490

491

492+hnf_compute :: RunTactic

493+hnf_compute ctxt env (Bind x (Hole ty) sc) =

494+ do let ty' = hnf ctxt env ty in

495+-- trace ("HNF " ++ show (ty, ty')) $

496+ return $ Bind x (Hole ty') sc

497+

491check_in :: Raw -> RunTactic

498check_in :: Raw -> RunTactic

492check_in t ctxt env tm =

499check_in t ctxt env tm =

493 do (val, valty) <- lift $ check ctxt env t

500 do (val, valty) <- lift $ check ctxt env t

@@ -603,6 +610,7 @@ process t h = tactic (Just h) (mktac t)

603 mktac Solve = solve

610 mktac Solve = solve

604 mktac (StartUnify n) = start_unify n

611 mktac (StartUnify n) = start_unify n

605 mktac Compute = compute

612 mktac Compute = compute

613+ mktac HNF_Compute = hnf_compute

606 mktac (Intro n) = intro n

614 mktac (Intro n) = intro n

607 mktac (IntroTy ty n) = introTy ty n

615 mktac (IntroTy ty n) = introTy ty n

608 mktac (Forall n t) = forall n t

616 mktac (Forall n t) = forall n t

src/Core/Typecheck.hs+7−6

@@ -28,11 +28,12 @@ convertsC ctxt env x y

29converts :: Context -> Env -> Term -> Term -> TC ()

30converts ctxt env x y

31+ = case convEq' ctxt x y of

31− = if x == y then return () else

32+ OK _ -> return ()

32− if (finalise (normalise ctxt env x) ==

33+ _ -> case convEq' ctxt (finalise (normalise ctxt env x))

33− finalise (normalise ctxt env y))

34+ (finalise (normalise ctxt env y)) of

34− then return ()

35+ OK _ -> return ()

35− else tfail (CantConvert

36+ _ -> tfail (CantConvert

36 (finalise (normalise ctxt env x))

37 (finalise (normalise ctxt env x))

37 (finalise (normalise ctxt env y)) (errEnv env))

38 (finalise (normalise ctxt env y)) (errEnv env))

@@ -67,7 +68,7 @@ check' holes ctxt env top = chk env top where

67 let fty' = case uniqueBinders (map fst env) (finalise fty) of

68 let fty' = case uniqueBinders (map fst env) (finalise fty) of

68 ty@(Bind x (Pi s) t) -> ty

69 ty@(Bind x (Pi s) t) -> ty

69 _ -> uniqueBinders (map fst env)

70 _ -> uniqueBinders (map fst env)

70− $ normalise ctxt env fty

71+ $ hnf ctxt env fty

71 case fty' of

72 case fty' of

72 Bind x (Pi s) t ->

73 Bind x (Pi s) t ->

73-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

74-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

src/Core/Unify.hs+34−12

@@ -21,18 +21,21 @@ type Injs = [(TT Name, TT Name, TT Name)]

21type Fails = [(TT Name, TT Name, Env, Err)]

23data UInfo = UI Int Injs Fails

24+ deriving Show

25unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

26unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

26 Injs, Fails)

27 Injs, Fails)

27unify ctxt env topx topy =

28unify ctxt env topx topy =

28-- trace ("Unifying " ++ show (topx, topy)) $

29-- trace ("Unifying " ++ show (topx, topy)) $

30+ -- don't bother if topx and topy are different at the head

29− case runStateT (un' False [] topx topy) (UI 0 [] []) of

31+ case runStateT (un False [] topx topy) (UI 0 [] []) of

30− OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

32+ OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

31− _ ->

33+-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

34+ res ->

32 let topxn = normalise ctxt env topx

35 let topxn = normalise ctxt env topx

33 topyn = normalise ctxt env topy in

36 topyn = normalise ctxt env topy in

34−-- trace ("Unifying " ++ show (topxn, topyn)) $

37+-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

35− case runStateT (un' False [] topxn topyn)

38+ case runStateT (un False [] topxn topyn)

36 (UI 0 [] []) of

39 (UI 0 [] []) of

37 OK (v, UI _ inj fails) ->

40 OK (v, UI _ inj fails) ->

38 return (filter notTrivial v, inj, reverse fails)

41 return (filter notTrivial v, inj, reverse fails)

@@ -41,6 +44,10 @@ unify ctxt env topx topy =

41 notTrivial (x, P _ x' _) = x /= x'

44 notTrivial (x, P _ x' _) = x /= x'

42 notTrivial _ = True

45 notTrivial _ = True

47+ headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y

48+ headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

49+ headDiff _ _ = False

50+

44 injective (P (DCon _ _) _ _) = True

51 injective (P (DCon _ _) _ _) = True

45 injective (P (TCon _ _) _ _) = True

52 injective (P (TCon _ _) _ _) = True

46 injective (App f a) = injective f

53 injective (App f a) = injective f

@@ -59,6 +66,17 @@ unify ctxt env topx topy =

59 then return r

66 then return r

60 else do put (UI s i f); u2

67 else do put (UI s i f); u2

69+ un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

70+ StateT UInfo

71+ TC [(Name, TT Name)]

72+ un = un'

73+-- un fn names x y

74+-- = let (xf, _) = unApply x

75+-- (yf, _) = unApply y in

76+-- if headDiff xf yf then unifyFail x y else

77+-- uplus (un' fn names x y)

78+-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

79+

62 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

80 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

63 StateT UInfo

81 StateT UInfo

64 TC [(Name, TT Name)]

82 TC [(Name, TT Name)]

@@ -141,8 +159,9 @@ unify ctxt env topx topy =

141 let r = recoverable x y

159 let r = recoverable x y

142 let err = CantUnify r

160 let err = CantUnify r

143 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

161 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

162+ if (not r) then lift $ tfail err

144− put (UI s i ((x, y, env, err) : f))

163+ else do put (UI s i ((x, y, env, err) : f))

145− return [] -- lift $ tfail err

164+ return [] -- lift $ tfail err

146

165

147 -- shortcut failure, if we *know* nothing can fix it

166 -- shortcut failure, if we *know* nothing can fix it

148 unifyFail x y = do UI s i f <- get

167 unifyFail x y = do UI s i f <- get

@@ -198,12 +217,15 @@ unify ctxt env topx topy =

198 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

217 recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

199 | x == y = True

218 | x == y = True

200 | otherwise = False

219 | otherwise = False

220+ recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

221+ | x == y = True

222+ | otherwise = False

201−-- recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

223+ recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

202−-- recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

224+ recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

203− recoverable p@(P _ _ _) (App f a) = recoverable p f

225+ recoverable p@(P _ n _) (App f a) = recoverable p f

204− recoverable (App f a) p@(P _ _ _) = recoverable f p

226+-- recoverable (App f a) p@(P _ _ _) = recoverable f p

205 recoverable (App f a) (App f' a')

227 recoverable (App f a) (App f' a')

206− = recoverable f f' && recoverable a a'

228+ = recoverable f f' -- && recoverable a a'

207 recoverable _ _ = True

229 recoverable _ _ = True

208

230

209errEnv = map (\(x, b) -> (x, binderTy b))

231errEnv = map (\(x, b) -> (x, binderTy b))

src/IRTS/CodegenC.hs+2

@@ -460,5 +460,7 @@ doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

460doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

461doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

462doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

463+doOp v LChInt args = v ++ creg (last args)

464+doOp v LIntCh args = v ++ creg (last args)

463doOp v LNoOp args = v ++ creg (last args)

465doOp v LNoOp args = v ++ creg (last args)

464doOp _ op _ = "FAIL /* " ++ show op ++ " */"

466doOp _ op _ = "FAIL /* " ++ show op ++ " */"

src/IRTS/CodegenJavaScript.hsnew file+501

@@ -0,0 +1,501 @@

1+{-# LANGUAGE PatternGuards #-}

3+{-

4+ BigInteger Javascript code taken from:

5+ https://github.com/peterolson/BigInteger.js

6+-}

8+module IRTS.CodegenJavaScript (codegenJavaScript) where

10+import Idris.AbsSyntax

11+import IRTS.Bytecode

12+import IRTS.Lang

13+import IRTS.Simplified

14+import IRTS.CodegenCommon

15+import Core.TT

16+import Paths_idris

17+import Util.System

18+

19+import Control.Arrow

20+import Data.Char

21+import Data.List

22+import System.IO

23+

24+type NamespaceName = String

25+

26+idrNamespace :: NamespaceName

27+idrNamespace = "__IDR__"

28+

29+codegenJavaScript

30+ :: [(Name, SDecl)]

31+ -> FilePath

32+ -> OutputType

33+ -> IO ()

34+codegenJavaScript definitions filename outputType =

35+ writeFile filename output

36+ where

37+ def = map (first translateNamespace) definitions

38+

39+ mainLoop :: String

40+ mainLoop = intercalate "\n" [ "\nfunction main() {"

41+ , createTailcall "__IDR__.runMain0()"

42+ , "}\n\nmain();\n"

43+ ]

44+

45+ output :: String

46+ output = concat [ idrRuntime

47+ , concatMap (translateModule Nothing) def

48+ , mainLoop

49+ ]

50+

51+idrRuntime :: String

52+idrRuntime =

53+ createModule Nothing idrNamespace $ concat

54+ [ "__IDR__.Type = function(type) { this.type = type; };"

55+ , "__IDR__.Int = new __IDR__.Type('Int');"

56+ , "__IDR__.Char = new __IDR__.Type('Char');"

57+ , "__IDR__.String = new __IDR__.Type('String');"

58+ , "__IDR__.Integer = new __IDR__.Type('Integer');"

59+ , "__IDR__.Float = new __IDR__.Type('Float');"

60+ , "__IDR__.Forgot = new __IDR__.Type('Forgot');"

61+

62+ , "__IDR__.bigInt=function(){var e=1e7,t=7,n={positive:!1,negative:!0},r=function(e,t){var n=e.value,r=t.value,i=n.length>r.length?n.length:r.length;for(var s=0;s<i;s++)n[s]=n[s]||0,r[s]=r[s]||0;for(var s=i-1;s>=0;s--){if(n[s]!==0||r[s]!==0)break;n.pop(),r.pop()}n.length||(n=[0],r=[0]),e.value=n,t.value=r},i=function(e,s){if(typeof e=='object')return e;e+='';var u=n.positive,a=[];e[0]==='-'&&(u=n.negative,e=e.slice(1));var e=e.split('e');if(e.length>2)throw new Error('Invalid integer');if(e[1]){var f=e[1];f[0]==='+'&&(f=f.slice(1)),f=i(f);if(f.lesser(0))throw new Error('Cannot include negative exponent part for integers');while(f.notEquals(0))e[0]+='0',f=f.prev()}e=e[0],e==='-0'&&(e='0');var l=/^([1-9][0-9]*)$|^0$/.test(e);if(!l)throw new Error('Invalid integer');while(e.length){var c=e.length>t?e.length-t:0;a.push(+e.slice(c)),e=e.slice(0,c)}var h=o(a,u);return s&&r(s,h),h},s=function(e,t){var e=o(e,n.positive),t=o(t,n.positive);if(e.equals(0))throw new Error('Cannot divide by 0');var r=0;do{var i=1,s=o(e.value,n.positive),u=s.times(10);while(u.lesser(t))s=u,i*=10,u=u.times(10);while(s.lesserOrEquals(t))t=t.minus(s),r+=i}while(e.lesserOrEquals(t));return{remainder:t.value,result:r}},o=function(f,l){var c={value:f,sign:l},h={value:f,sign:l,negate:function(e){var t=e||c;return o(t.value,!t.sign)},abs:function(e){var t=e||c;return o(t.value,n.positive)},add:function(t,s){var u,a=c,f;s?(a=i(t))&&(f=i(s)):f=i(t,a),u=a.sign;if(a.sign!==f.sign)return a=o(a.value,n.positive),f=o(f.value,n.positive),u===n.positive?h.subtract(a,f):h.subtract(f,a);r(a,f);var l=a.value,p=f.value,d=[],v=0;for(var m=0;m<l.length||v>0;m++){var g=l[m]+p[m]+v;v=g>e?1:0,g-=v*e,d.push(g)}return o(d,u)},plus:function(e,t){return h.add(e,t)},subtract:function(t,r){var s=c,u;r?(s=i(t))&&(u=i(r)):u=i(t,s);if(s.sign!==u.sign)return h.add(s,h.negate(u));if(s.sign===n.negative)return h.subtract(h.negate(u),h.negate(s));if(h.compare(s,u)===-1)return h.negate(h.subtract(u,s));var a=s.value,f=u.value,l=[],p=0;for(var d=0;d<a.length;d++){a[d]-=p,p=a[d]<f[d]?1:0;var v=p*e+a[d]-f[d];l.push(v)}return o(l,n.positive)},minus:function(e,t){return h.subtract(e,t)},multiply:function(t,n){var r,s=c,u;n?(s=i(t))&&(u=i(n)):u=i(t,s),r=s.sign!==u.sign;var a=s.value,f=u.value,l=[];for(var h=0;h<a.length;h++){l[h]=[];var p=h;while(p--)l[h].push(0)}var d=0;for(var h=0;h<a.length;h++){var v=a[h];for(var p=0;p<f.length||d>0;p++){var m=f[p],g=m?v*m+d:d;d=g>e?Math.floor(g/e):0,g-=d*e,l[h].push(g)}}var y=-1;for(var h=0;h<l.length;h++){var b=l[h].length;b>y&&(y=b)}var w=[],d=0;for(var h=0;h<y||d>0;h++){var E=d;for(var p=0;p<l.length;p++)E+=l[p][h]||0;d=E>e?Math.floor(E/e):0,E-=d*e,w.push(E)}return o(w,r)},times:function(e,t){return h.multiply(e,t)},divmod:function(e,t){var r,u=c,a;t?(u=i(e))&&(a=i(t)):a=i(e,u),r=u.sign!==a.sign;if(o(u.value,u.sign).equals(0))return{quotient:o([0],n.positive),remainder:o([0],n.positive)};if(a.equals(0))throw new Error('Cannot divide by zero');var f=u.value,l=a.value,h=[],p=[];for(var d=f.length-1;d>=0;d--){var e=[f[d]].concat(p),v=s(l,e);h.push(v.result),p=v.remainder}return h.reverse(),{quotient:o(h,r),remainder:o(p,u.sign)}},divide:function(e,t){return h.divmod(e,t).quotient},over:function(e,t){return h.divide(e,t)},mod:function(e,t){return h.divmod(e,t).remainder},pow:function(e,t){var n=c,r;t?(n=i(e))&&(r=i(t)):r=i(e,n);var s=n,f=r;if(f.lesser(0))return u;if(f.equals(0))return a;var l=o(s.value,s.sign);if(f.mod(2).equals(0)){var h=l.pow(f.over(2));return h.times(h)}return l.times(l.pow(f.minus(1)))},next:function(e){var t=e||c;return h.add(t,1)},prev:function(e){var t=e||c;return h.subtract(t,1)},compare:function(e,t){var s=c,o;t?(s=i(e))&&(o=i(t,s)):o=i(e,s),r(s,o);if(s.value.length===1&&o.value.length===1&&s.value[0]===0&&o.value[0]===0)return 0;if(o.sign!==s.sign)return s.sign===n.positive?1:-1;var u=s.sign===n.positive?1:-1,a=s.value,f=o.value;for(var l=a.length-1;l>=0;l--){if(a[l]>f[l])return 1*u;if(f[l]>a[l])return-1*u}return 0},compareAbs:function(e,t){var r=c,s;return t?(r=i(e))&&(s=i(t,r)):s=i(e,r),r.sign=s.sign=n.positive,h.compare(r,s)},equals:function(e,t){return h.compare(e,t)===0},notEquals:function(e,t){return!h.equals(e,t)},lesser:function(e,t){return h.compare(e,t)<0},greater:function(e,t){return h.compare(e,t)>0},greaterOrEquals:function(e,t){return h.compare(e,t)>=0},lesserOrEquals:function(e,t){return h.compare(e,t)<=0},isPositive:function(e){var t=e||c;return t.sign===n.positive},isNegative:function(e){var t=e||c;return t.sign===n.negative},isEven:function(e){var t=e||c;return t.value[0]%2===0},isOdd:function(e){var t=e||c;return t.value[0]%2===1},toString:function(r){var i=r||c,s='',o=i.value.length;while(o--)s+=(e.toString()+i.value[o]).slice(-t);while(s[0]==='0')s=s.slice(1);s.length||(s='0');var u=i.sign===n.positive?'':'-';return u+s},toJSNumber:function(e){return+h.toString(e)},valueOf:function(e){return h.toJSNumber(e)}};return h},u=o([0],n.positive),a=o([1],n.positive),f=o([1],n.negative),l=function(e){return typeof e=='undefined'?u:i(e)};return l.zero=u,l.one=a,l.minusOne=f,l}();typeof module!='undefined'&&(module.exports=__IDR__.bigInt);"

63+

64+ , "__IDR__.Tailcall = function(f) { this.f = f };"

65+

66+ , "__IDR__.Con = function(i,name,vars)"

67+ , "{this.i = i;this.name = name;this.vars = vars;};\n"

68+

69+ , "__IDR__.tailcall = function(f){\n"

70+ ++ "var __f = f;\n"

71+ ++ "while (__f) {\n"

72+ ++ "var f = __f;\n"

73+ ++ "__f = null;\n"

74+ ++ "var ret = f();\n"

75+ ++ "if (ret instanceof __IDR__.Tailcall) {\n"

76+ ++ "__f = ret.f;"

77+ ++ "\n} else {\n"

78+ ++ "return ret;"

79+ ++ "\n}"

80+ ++ "\n}"

81+ ++ "\n};\n"

82+

83+ , "var newline_regex =/(.*)\\n$/;\n"

84+

85+ , "__IDR__.print = function(s){\n"

86+ ++ "var m = s.match(newline_regex);\n"

87+ ++ "console.log(m ? m[1] : s);"

88+ ++ "\n};\n"

89+ ]

90+

91+createModule :: Maybe String -> NamespaceName -> String -> String

92+createModule toplevel modname body =

93+ concat [header modname, body, footer modname]

94+ where

95+ header :: NamespaceName -> String

96+ header modname =

97+ concatMap (++ "\n")

98+ [ "\nvar " ++ modname ++ ";"

99+ , "(function(" ++ modname ++ "){"

100+ ]

101+

102+ footer :: NamespaceName -> String

103+ footer modname =

104+ let m = maybe "" (++ ".") toplevel ++ modname in

105+ "\n})("

106+ ++ m

107+ ++ " || ("

108+ ++ m

109+ ++ " = {})"

110+ ++ ");\n"

111+

112+translateModule :: Maybe String -> ([String], SDecl) -> String

113+translateModule toplevel ([modname], decl) =

114+ let body = translateDeclaration modname decl in

115+ createModule toplevel modname body

116+translateModule toplevel (n:ns, decl) =

117+ createModule toplevel n $ translateModule (Just n) (ns, decl)

118+

119+translateIdentifier :: String -> String

120+translateIdentifier =

121+ concatMap replaceBadChars

122+ where replaceBadChars :: Char -> String

123+ replaceBadChars ' ' = "_"

124+ replaceBadChars '_' = "__"

125+ replaceBadChars '@' = "_at"

126+ replaceBadChars '[' = "_OSB"

127+ replaceBadChars ']' = "_CSB"

128+ replaceBadChars '(' = "_OP"

129+ replaceBadChars ')' = "_CP"

130+ replaceBadChars '{' = "_OB"

131+ replaceBadChars '}' = "_CB"

132+ replaceBadChars '!' = "_bang"

133+ replaceBadChars '#' = "_hash"

134+ replaceBadChars '.' = "_dot"

135+ replaceBadChars ',' = "_comma"

136+ replaceBadChars ':' = "_colon"

137+ replaceBadChars '+' = "_plus"

138+ replaceBadChars '-' = "_minus"

139+ replaceBadChars '*' = "_times"

140+ replaceBadChars '<' = "_lt"

141+ replaceBadChars '>' = "_gt"

142+ replaceBadChars '=' = "_eq"

143+ replaceBadChars '|' = "_pipe"

144+ replaceBadChars '&' = "_amp"

145+ replaceBadChars '/' = "_SL"

146+ replaceBadChars '\\' = "_BSL"

147+ replaceBadChars '%' = "_per"

148+ replaceBadChars '?' = "_que"

149+ replaceBadChars '~' = "_til"

150+ replaceBadChars '\'' = "_apo"

151+ replaceBadChars c

152+ | isDigit c = "_" ++ [c] ++ "_"

153+ | otherwise = [c]

154+

155+translateNamespace :: Name -> [String]

156+translateNamespace (UN _) = [idrNamespace]

157+translateNamespace (NS _ ns) = idrNamespace : map translateIdentifier ns

158+translateNamespace (MN _ _) = [idrNamespace]

159+

160+translateName :: Name -> String

161+translateName (UN name) = translateIdentifier name

162+translateName (NS name _) = translateName name

163+translateName (MN i name) = translateIdentifier name ++ show i

164+

165+translateQualifiedName :: Name -> String

166+translateQualifiedName name =

167+ intercalate "." (translateNamespace name) ++ "." ++ translateName name

168+

169+translateConstant :: Const -> String

170+translateConstant (I i) = show i

171+translateConstant (BI i) = "__IDR__.bigInt('" ++ show i ++ "')"

172+translateConstant (Fl f) = show f

173+translateConstant (Ch c) = show c

174+translateConstant (Str s) = show s

175+translateConstant IType = "__IDR__.Int"

176+translateConstant ChType = "__IDR__.Char"

177+translateConstant StrType = "__IDR__.String"

178+translateConstant BIType = "__IDR__.Integer"

179+translateConstant FlType = "__IDR__.Float"

180+translateConstant Forgot = "__IDR__.Forgot"

181+translateConstant c =

182+ "(function(){throw 'Unimplemented Const: " ++ show c ++ "';})()"

183+

184+translateParameterlist =

185+ map translateParameter

186+ where translateParameter (MN i name) = name ++ show i

187+ translateParameter (UN name) = name

188+

189+translateDeclaration :: NamespaceName -> SDecl -> String

190+translateDeclaration modname (SFun name params stackSize body) =

191+ modname

192+ ++ "."

193+ ++ translateName name

194+ ++ " = function("

195+ ++ intercalate "," p

196+ ++ "){\n"

197+ ++ concatMap assignVar (zip [0..] p)

198+ ++ concatMap allocVar [numP..(numP+stackSize-1)]

199+ ++ "return "

200+ ++ translateExpression modname body

201+ ++ ";\n};\n"

202+ where

203+ numP :: Int

204+ numP = length params

205+

206+ allocVar :: Int -> String

207+ allocVar n = "var __var_" ++ show n ++ ";\n"

208+

209+ assignVar :: (Int, String) -> String

210+ assignVar (n, s) = "var __var_" ++ show n ++ " = " ++ s ++ ";\n"

211+

212+ p :: [String]

213+ p = translateParameterlist params

214+

215+translateVariableName :: LVar -> String

216+translateVariableName (Loc i) =

217+ "__var_" ++ show i

218+

219+translateExpression :: NamespaceName -> SExp -> String

220+translateExpression modname (SLet name value body) =

221+ "(function("

222+ ++ translateVariableName name

223+ ++ "){\nreturn "

224+ ++ translateExpression modname body

225+ ++ ";\n})("

226+ ++ translateExpression modname value

227+ ++ ")"

228+

229+translateExpression _ (SConst cst) =

230+ translateConstant cst

231+

232+translateExpression _ (SV var) =

233+ translateVariableName var

234+

235+translateExpression modname (SApp False name vars) =

236+ createTailcall $ translateFunctionCall name vars

237+

238+translateExpression modname (SApp True name vars) =

239+ "new __IDR__.Tailcall("

240+ ++ "function(){\n"

241+ ++ "return " ++ translateFunctionCall name vars

242+ ++ ";\n});"

243+

244+translateExpression _ (SOp op vars)

245+ | LPlus <- op

246+ , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

247+ | LMinus <- op

248+ , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs

249+ | LTimes <- op

250+ , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs

251+ | LDiv <- op

252+ , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs

253+ | LMod <- op

254+ , (lhs:rhs:_) <- vars = translateBinaryOp "%" lhs rhs

255+ | LEq <- op

256+ , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

257+ | LLt <- op

258+ , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

259+ | LLe <- op

260+ , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs

261+ | LGt <- op

262+ , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs

263+ | LGe <- op

264+ , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

265+ | LAnd <- op

266+ , (lhs:rhs:_) <- vars = translateBinaryOp "&" lhs rhs

267+ | LOr <- op

268+ , (lhs:rhs:_) <- vars = translateBinaryOp "|" lhs rhs

269+ | LXOr <- op

270+ , (lhs:rhs:_) <- vars = translateBinaryOp "^" lhs rhs

271+ | LSHL <- op

272+ , (lhs:rhs:_) <- vars = translateBinaryOp "<<" rhs lhs

273+ | LSHR <- op

274+ , (lhs:rhs:_) <- vars = translateBinaryOp ">>" rhs lhs

275+ | LCompl <- op

276+ , (arg:_) <- vars = '~' : translateVariableName arg

277+

278+ | LBPlus <- op

279+ , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"

280+ | LBMinus <- op

281+ , (lhs:rhs:_) <- vars = translateBinaryOp ".minus(" lhs rhs ++ ")"

282+ | LBTimes <- op

283+ , (lhs:rhs:_) <- vars = translateBinaryOp ".times(" lhs rhs ++ ")"

284+ | LBDiv <- op

285+ , (lhs:rhs:_) <- vars = translateBinaryOp ".divide(" lhs rhs ++ ")"

286+ | LBMod <- op

287+ , (lhs:rhs:_) <- vars = translateBinaryOp ".mod(" lhs rhs ++ ")"

288+ | LBEq <- op

289+ , (lhs:rhs:_) <- vars = translateBinaryOp ".equals(" lhs rhs ++ ")"

290+ | LBLt <- op

291+ , (lhs:rhs:_) <- vars = translateBinaryOp ".lesser(" lhs rhs ++ ")"

292+ | LBLe <- op

293+ , (lhs:rhs:_) <- vars = translateBinaryOp ".lesserOrEquals(" lhs rhs ++ ")"

294+ | LBGt <- op

295+ , (lhs:rhs:_) <- vars = translateBinaryOp ".greater(" lhs rhs ++ ")"

296+ | LBGe <- op

297+ , (lhs:rhs:_) <- vars = translateBinaryOp ".greaterOrEquals(" lhs rhs ++ ")"

298+

299+ | LFPlus <- op

300+ , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

301+ | LFMinus <- op

302+ , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs

303+ | LFTimes <- op

304+ , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs

305+ | LFDiv <- op

306+ , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs

307+ | LFEq <- op

308+ , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

309+ | LFLt <- op

310+ , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

311+ | LFLe <- op

312+ , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs

313+ | LFGt <- op

314+ , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs

315+ | LFGe <- op

316+ , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

317+

318+ | LStrConcat <- op

319+ , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

320+ | LStrEq <- op

321+ , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

322+ | LStrLt <- op

323+ , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

324+ | LStrLen <- op

325+ , (arg:_) <- vars = translateVariableName arg ++ ".length"

326+

327+ | LStrInt <- op

328+ , (arg:_) <- vars = "parseInt(" ++ translateVariableName arg ++ ")"

329+ | LIntStr <- op

330+ , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

331+ | LIntBig <- op

332+ , (arg:_) <- vars = "__IDR__.bigint(" ++ translateVariableName arg ++ ")"

333+ | LBigInt <- op

334+ , (arg:_) <- vars = translateVariableName arg ++ ".valueOf()"

335+ | LBigStr <- op

336+ , (arg:_) <- vars = translateVariableName arg ++ ".toString()"

337+ | LStrBig <- op

338+ , (arg:_) <- vars = "__IDR__.bigint(" ++ translateVariableName arg ++ ")"

339+ | LFloatStr <- op

340+ , (arg:_) <- vars = "String(" ++ translateVariableName arg ++ ")"

341+ | LStrFloat <- op

342+ , (arg:_) <- vars = "parseFloat(" ++ translateVariableName arg ++ ")"

343+ | LIntFloat <- op

344+ , (arg:_) <- vars = translateVariableName arg

345+ | LFloatInt <- op

346+ , (arg:_) <- vars = translateVariableName arg

347+ | LChInt <- op

348+ , (arg:_) <- vars = translateVariableName arg ++ ".charCodeAt(0)"

349+ | LIntCh <- op

350+ , (arg:_) <- vars =

351+ "String.fromCharCode(" ++ translateVariableName arg ++ ")"

352+

353+ | LFExp <- op

354+ , (arg:_) <- vars = "Math.exp(" ++ translateVariableName arg ++ ")"

355+ | LFLog <- op

356+ , (arg:_) <- vars = "Math.log(" ++ translateVariableName arg ++ ")"

357+ | LFSin <- op

358+ , (arg:_) <- vars = "Math.sin(" ++ translateVariableName arg ++ ")"

359+ | LFCos <- op

360+ , (arg:_) <- vars = "Math.cos(" ++ translateVariableName arg ++ ")"

361+ | LFTan <- op

362+ , (arg:_) <- vars = "Math.tan(" ++ translateVariableName arg ++ ")"

363+ | LFASin <- op

364+ , (arg:_) <- vars = "Math.asin(" ++ translateVariableName arg ++ ")"

365+ | LFACos <- op

366+ , (arg:_) <- vars = "Math.acos(" ++ translateVariableName arg ++ ")"

367+ | LFATan <- op

368+ , (arg:_) <- vars = "Math.atan(" ++ translateVariableName arg ++ ")"

369+ | LFSqrt <- op

370+ , (arg:_) <- vars = "Math.sqrt(" ++ translateVariableName arg ++ ")"

371+ | LFFloor <- op

372+ , (arg:_) <- vars = "Math.floor(" ++ translateVariableName arg ++ ")"

373+ | LFCeil <- op

374+ , (arg:_) <- vars = "Math.ceil(" ++ translateVariableName arg ++ ")"

375+

376+ | LStrCons <- op

377+ , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

378+ | LStrHead <- op

379+ , (arg:_) <- vars = translateVariableName arg ++ "[0]"

380+ | LStrRev <- op

381+ , (arg:_) <- vars = let v = translateVariableName arg in

382+ v ++ "split('').reverse().join('')"

383+ | LStrIndex <- op

384+ , (lhs:rhs:_) <- vars = let l = translateVariableName lhs

385+ r = translateVariableName rhs in

386+ l ++ "[" ++ r ++ "]"

387+ | LStrTail <- op

388+ , (arg:_) <- vars = let v = translateVariableName arg in

389+ v ++ ".substr(1," ++ v ++ ".length-1)"

390+ where

391+ translateBinaryOp :: String -> LVar -> LVar -> String

392+ translateBinaryOp f lhs rhs =

393+ translateVariableName lhs

394+ ++ f

395+ ++ translateVariableName rhs

396+

397+translateExpression _ (SError msg) =

398+ "(function(){throw \'" ++ msg ++ "\';})();"

399+

400+translateExpression _ (SForeign _ _ "putStr" [(FString, var)]) =

401+ "__IDR__.print(" ++ translateVariableName var ++ ");"

402+

403+translateExpression _ (SForeign _ _ fun args) =

404+ fun

405+ ++ "("

406+ ++ intercalate "," (map (translateVariableName . snd) args)

407+ ++ ");"

408+

409+translateExpression modname (SChkCase var cases) =

410+ "(function(e){\n"

411+ ++ intercalate " else " (map (translateCase modname "e") cases)

412+ ++ "\n})("

413+ ++ translateVariableName var

414+ ++ ")"

415+

416+translateExpression modname (SCase var cases) =

417+ "(function(e){\n"

418+ ++ intercalate " else " (map (translateCase modname "e") cases)

419+ ++ "\n})("

420+ ++ translateVariableName var

421+ ++ ")"

422+

423+translateExpression _ (SCon i name vars) =

424+ concat [ "new __IDR__.Con("

425+ , show i

426+ , ","

427+ , '\'' : translateQualifiedName name ++ "\',["

428+ , intercalate "," $ map translateVariableName vars

429+ , "])"

430+ ]

431+

432+translateExpression modname (SUpdate var e) =

433+ translateVariableName var ++ " = " ++ translateExpression modname e

434+

435+translateExpression modname (SProj var i) =

436+ translateVariableName var ++ ".vars[" ++ show i ++"]"

437+

438+translateExpression _ SNothing = "null"

439+

440+translateExpression _ e =

441+ "(function(){throw 'Not yet implemented: "

442+ ++ filter (/= '\'') (show e)

443+ ++ "';})()"

444+

445+translateCase :: String -> String -> SAlt -> String

446+translateCase modname _ (SDefaultCase e) =

447+ createIfBlock "true" (translateExpression modname e)

448+

449+translateCase modname var (SConstCase ty e)

450+ | ChType <- ty = matchHelper "Char"

451+ | StrType <- ty = matchHelper "String"

452+ | IType <- ty = matchHelper "Int"

453+ | BIType <- ty = matchHelper "Integer"

454+ | FlType <- ty = matchHelper "Float"

455+ | Forgot <- ty = matchHelper "Forgot"

456+ where

457+ matchHelper tyName = translateTypeMatch modname var tyName e

458+

459+translateCase modname var (SConstCase cst@(BI _) e) =

460+ let cond = var ++ ".equals(" ++ translateConstant cst ++ ")" in

461+ createIfBlock cond (translateExpression modname e)

462+

463+translateCase modname var (SConstCase cst e) =

464+ let cond = var ++ " == " ++ translateConstant cst in

465+ createIfBlock cond (translateExpression modname e)

466+

467+translateCase modname var (SConCase a i name vars e) =

468+ let isCon = var ++ " instanceof __IDR__.Con"

469+ isI = show i ++ " == " ++ var ++ ".i"

470+ params = intercalate "," $ map (("__var_" ++) . show) [a..(a+length vars)]

471+ args = ".apply(this," ++ var ++ ".vars)"

472+ f b =

473+ "(function("

474+ ++ params

475+ ++ "){\nreturn " ++ b ++ "\n})" ++ args

476+ cond = intercalate " && " [isCon, isI] in

477+ createIfBlock cond $ f (translateExpression modname e)

478+

479+translateTypeMatch :: String -> String -> String -> SExp -> String

480+translateTypeMatch modname var ty exp =

481+ let e = translateExpression modname exp in

482+ createIfBlock (var

483+ ++ " instanceof __IDR__.Type && "

484+ ++ var ++ ".type == '"++ ty ++"'") e

485+

486+

487+createIfBlock cond e =

488+ "if (" ++ cond ++") {\n"

489+ ++ "return " ++ e

490+ ++ ";\n}"

491+

492+createTailcall call =

493+ "__IDR__.tailcall(function(){return " ++ call ++ "})"

494+

495+translateFunctionCall name vars =

496+ concat (intersperse "." $ translateNamespace name)

497+ ++ "."

498+ ++ translateName name

499+ ++ "("

500+ ++ intercalate "," (map translateVariableName vars)

501+ ++ ")"

src/IRTS/Compiler.hs+3−1

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

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE PatternGuards, TypeSynonymInstances #-}

3module IRTS.Compiler where

@@ -9,6 +9,7 @@ import IRTS.CodegenCommon

9import IRTS.CodegenC

10import IRTS.CodegenJava

11import IRTS.DumpBC

12+import IRTS.CodegenJavaScript

12import IRTS.Inliner

13import IRTS.Inliner

14import Idris.AbsSyntax

15import Idris.AbsSyntax

@@ -70,6 +71,7 @@ compile target f tm

70 (concatMap mkLib libs) NONE

71 (concatMap mkLib libs) NONE

71 ViaJava -> liftIO $ codegenJava c f outty

72 ViaJava -> liftIO $ codegenJava c f outty

72 Bytecode -> liftIO $ dumpBC c f

73 Bytecode -> liftIO $ dumpBC c f

74+ ToJavaScript -> liftIO $ codegenJavaScript c f outty

73 Error e -> fail $ show e

75 Error e -> fail $ show e

74 where checkMVs = do i <- get

76 where checkMVs = do i <- get

75 case idris_metavars i \\ primDefs of

77 case idris_metavars i \\ primDefs of

src/IRTS/LParser.hs+1

@@ -9,6 +9,7 @@ import IRTS.Bytecode

9import IRTS.CodegenCommon

10import IRTS.CodegenC

11import IRTS.CodegenJava

12+import IRTS.CodegenJavaScript

12import IRTS.Defunctionalise

13import IRTS.Defunctionalise

13import Paths_idris

14import Paths_idris

src/IRTS/Lang.hs+1−1

@@ -37,7 +37,7 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod

38 | LStrConcat | LStrLt | LStrEq | LStrLen

40− | LIntBig | LBigInt | LStrBig | LBigStr

41 | LPrintNum | LPrintStr | LReadStr

src/Idris/AbsSyntaxTree.hs+3−1

@@ -140,7 +140,7 @@ type Idris = StateT IState (InputT IO)

140

141-- Commands in the REPL

142

143−data Target = ViaC | ViaJava | Bytecode

143+data Target = ViaC | ViaJava | Bytecode | ToJavaScript

144 deriving (Show, Eq)

145

146data Command = Quit

@@ -472,6 +472,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

472 | ProofState | ProofTerm | Undo

473 | Try (PTactic' t) (PTactic' t)

474 | TSeq (PTactic' t) (PTactic' t)

475+ | ReflectTac t -- see Language.Reflection module

476+ | GoalType String (PTactic' t)

475 | Qed | Abandon

477 | Qed | Abandon

476 deriving (Show, Eq, Functor)

478 deriving (Show, Eq, Functor)

477{-!

479{-!

src/Idris/Delaborate.hs+6−3

@@ -77,15 +77,18 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

77 "\nThis is probably a bug, or a missing error message.\n" ++

78 "Please consider reporting at " ++ bugaddr

79pshow i (CantUnify _ x y e sc s)

80+ = let imps = opt_showimp (idris_options i) in

80− = "Can't unify " ++ show (delab i x)

81+ "Can't unify " ++ showImp imps (delab i x)

81− ++ " with " ++ show (delab i y) ++

82+ ++ " with " ++ showImp imps (delab i y) ++

82-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

83-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

83 case e of

84 case e of

84 Msg "" -> ""

85 Msg "" -> ""

85 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

86 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

86 if (opt_errContext (idris_options i)) then showSc i sc else ""

87 if (opt_errContext (idris_options i)) then showSc i sc else ""

87pshow i (CantConvert x y env)

88pshow i (CantConvert x y env)

89+ = let imps = opt_showimp (idris_options i) in

88− = "Can't convert " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

90+ "Can't convert " ++ showImp imps (delab i x) ++ " with "

91+ ++ showImp imps (delab i y) ++

89 if (opt_errContext (idris_options i)) then showSc i env else ""

92 if (opt_errContext (idris_options i)) then showSc i env else ""

90pshow i (InfiniteUnify x tm env)

93pshow i (InfiniteUnify x tm env)

91 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

94 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

src/Idris/ElabDecls.hs+6−5

@@ -440,6 +440,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

440

441 simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,

442 simplify ctxt rt [] y)

443+-- simpl rt ctxt (Right (x, y)) = Right (x, y)

443 simpl rt ctxt t = t

444 simpl rt ctxt t = t

444

445

445 sameLength ((_, x, _) : xs)

446 sameLength ((_, x, _) : xs)

@@ -461,9 +462,9 @@ elabVal info aspat tm_in

461 -- * elaboration as a function a -> b

462 -- * elaboration as a function a -> b

462

463

463 ((tm', defer, is), _) <-

464 ((tm', defer, is), _) <-

464− tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

465+-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

465− (build i info aspat (MN 0 "val") tm))

466+-- (build i info aspat (MN 0 "val") tm))

466− (elaborate ctxt (MN 0 "val") infP []

467+ tclift (elaborate ctxt (MN 0 "val") infP []

467 (build i info aspat (MN 0 "val") (infTerm tm)))

468 (build i info aspat (MN 0 "val") (infTerm tm)))

468 logLvl 3 ("Value: " ++ show tm')

469 logLvl 3 ("Value: " ++ show tm')

469 recheckC (FC "(input)" 0) [] tm'

470 recheckC (FC "(input)" 0) [] tm'

@@ -565,7 +566,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

565 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

566 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

566 case converts ctxt [] clhsty crhsty of

567 case converts ctxt [] clhsty crhsty of

567 OK _ -> return ()

568 OK _ -> return ()

568− Error _ -> ierror (At fc (CantUnify False clhsty crhsty (Msg "") [] 0))

569+ Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

569 i <- get

570 i <- get

570 checkInferred fc (delab' i crhs True) rhs

571 checkInferred fc (delab' i crhs True) rhs

571 return $ Right (clhs, crhs)

572 return $ Right (clhs, crhs)

@@ -793,7 +794,7 @@ elabClass info syn doc fc constraints tn ps ds

793 pibind [] x = x

794 pibind [] x = x

794 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

795 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

795

796

796− mdec (UN n) = (UN ('!':n))

797+ mdec (UN n) = UN ('!':n)

797 mdec (NS x n) = NS (mdec x) n

798 mdec (NS x n) = NS (mdec x) n

798 mdec x = x

799 mdec x = x

799

800

src/Idris/ElabTerm.hs+85−38

@@ -112,7 +112,8 @@ elab ist info pattern tcgen fn tm

112 elab' ina (PResolveTC fc)

113 | pattern = do c <- unique_hole (MN 0 "c")

114 instanceArg c

115+ | otherwise = do g <- goal

115− | otherwise = try (resolveTC 2 fn ist)

116+ try (resolveTC 2 fn ist)

116 (do c <- unique_hole (MN 0 "c")

117 (do c <- unique_hole (MN 0 "c")

117 instanceArg c)

118 instanceArg c)

118 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

119 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

@@ -147,9 +148,7 @@ elab ist info pattern tcgen fn tm

147 ctxt <- get_context

148 ctxt <- get_context

148 let (tc, _) = unApply ty

149 let (tc, _) = unApply ty

149 let as' = pruneByType tc ctxt as

150 let as' = pruneByType tc ctxt as

150− let as'' = as' -- pruneAlt as'

151− try (tryAll (zip (map (elab' ina) as'') (map showHd as'')))

151+ tryAll (zip (map (elab' ina) as') (map showHd as'))

152− (tryAll (zip (map (elab' ina) as') (map showHd as')))

153 where showHd (PApp _ h _) = show h

152 where showHd (PApp _ h _) = show h

154 showHd x = show x

153 showHd x = show x

155 elab' ina (PAlternative False as)

154 elab' ina (PAlternative False as)

@@ -292,16 +291,17 @@ elab ist info pattern tcgen fn tm

292-- when True

291-- when True

293 tryWhen True

292 tryWhen True

294 (do ns <- apply (Var f) (map isph args)

293 (do ns <- apply (Var f) (map isph args)

294+ ptm <- get_term

295− let (ns', eargs)

295+ let (ns', eargs) = unzip $

296− = unzip $

296+ sortBy (\(_,x) (_,y) ->

297− sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

297+ compare (priority x) (priority y))

298 (zip ns args)

299− try

299+ tryWhen True

300− (elabArgs (ina || not isinf, guarded)

300+ (elabArgs (ina || not isinf, guarded)

301− [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

301+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

302− (elabArgs (ina || not isinf, guarded)

302+ (elabArgs (ina || not isinf, guarded)

303− [] False (reverse ns')

303+ [] False (reverse ns')

304− (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

304+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))

305 mkSpecialised ist fc f (map getTm args') tm

306 solve)

307 (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

@@ -317,6 +317,10 @@ elab ist info pattern tcgen fn tm

317 where tcArg (n, PConstraint _ _ Placeholder _) = True

318 tcArg _ = False

319

320+ tacTm (PTactics _) = True

321+ tacTm (PProof _) = True

322+ tacTm _ = False

323+

320 elab' ina@(_, a) (PApp fc f [arg])

324 elab' ina@(_, a) (PApp fc f [arg])

321 = erun fc $

325 = erun fc $

322 do ptm <- get_term

326 do ptm <- get_term

@@ -400,10 +404,10 @@ elab ist info pattern tcgen fn tm

400 failed' <- -- trace (show (n, t, hs, tm)) $

404 failed' <- -- trace (show (n, t, hs, tm)) $

401 case n `elem` hs of

405 case n `elem` hs of

402 True ->

406 True ->

403− if r

407+-- if r

404− then try (do focus n; elabE ina t; return failed)

408+-- then try (do focus n; elabE ina t; return failed)

405− (return ((n,(lazy, t)):failed))

409+-- (return ((n,(lazy, t)):failed))

406− else do focus n; elabE ina t; return failed

410+ do focus n; elabE ina t; return failed

407 False -> return failed

411 False -> return failed

408 elabArgs ina failed r ns args

412 elabArgs ina failed r ns args

409

413

@@ -454,17 +458,17 @@ pruneByType (P _ n _) c as

454pruneByType t _ as = as

458pruneByType t _ as = as

455

459

456trivial :: IState -> ElabD ()

460trivial :: IState -> ElabD ()

457−trivial ist = try (do elab ist toplevel False False (MN 0 "tac")

461+trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

458 (PRefl (FC "prf" 0) Placeholder)

462 (PRefl (FC "prf" 0) Placeholder)

459− return ())

463+ return ())

460− (do env <- get_env

464+ (do env <- get_env

461− tryAll (map fst env)

465+ tryAll (map fst env)

462− return ())

466+ return ()) True

463 where

467 where

464 tryAll [] = fail "No trivial solution"

468 tryAll [] = fail "No trivial solution"

465− tryAll (x:xs) = try (elab ist toplevel False False

469+ tryAll (x:xs) = try' (elab ist toplevel False False

466 (MN 0 "tac") (PRef (FC "prf" 0) x))

470 (MN 0 "tac") (PRef (FC "prf" 0) x))

467− (tryAll xs)

471+ (tryAll xs) True

468

472

469findInstances :: IState -> Term -> [Name]

473findInstances :: IState -> Term -> [Name]

470findInstances ist t

474findInstances ist t

@@ -476,18 +480,19 @@ findInstances ist t

476

480

477resolveTC :: Int -> Name -> IState -> ElabD ()

481resolveTC :: Int -> Name -> IState -> ElabD ()

478resolveTC 0 fn ist = fail $ "Can't resolve type class"

482resolveTC 0 fn ist = fail $ "Can't resolve type class"

479−resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

483+resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True

480resolveTC depth fn ist

484resolveTC depth fn ist

485+ = do hnf_compute

481− = try (trivial ist)

486+ try' (trivial ist)

482− (do t <- goal

487+ (do t <- goal

483− let insts = findInstances ist t

488+ let insts = findInstances ist t

484− let (tc, ttypes) = unApply t

489+ let (tc, ttypes) = unApply t

485− scopeOnly <- needsDefault t tc ttypes

490+ scopeOnly <- needsDefault t tc ttypes

486− tm <- get_term

491+ tm <- get_term

487-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

492-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

488-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

493-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

489− let depth' = if scopeOnly then 2 else depth

494+ let depth' = if scopeOnly then 2 else depth

490− blunderbuss t depth' insts)

495+ blunderbuss t depth' insts) True

491 where

496 where

492 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

497 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

493 | otherwise = (fail "Can't resolve", show n)

498 | otherwise = (fail "Can't resolve", show n)

@@ -506,8 +511,8 @@ resolveTC depth fn ist

506

511

507 blunderbuss t d [] = lift $ tfail $ CantResolve t

512 blunderbuss t d [] = lift $ tfail $ CantResolve t

508 blunderbuss t d (n:ns)

513 blunderbuss t d (n:ns)

509− | n /= fn && tcname n = try (resolve n d)

514+ | n /= fn && tcname n = try' (resolve n d)

510− (blunderbuss t d ns)

515+ (blunderbuss t d ns) True

511 | otherwise = blunderbuss t d ns

516 | otherwise = blunderbuss t d ns

512

517

513 resolve n depth

518 resolve n depth

@@ -564,8 +569,8 @@ runTac autoSolve ist tac = do env <- get_env

564 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

569 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

565 runT Intros = do g <- goal

570 runT Intros = do g <- goal

566 attack; intro (bname g)

571 attack; intro (bname g)

567− try (runT Intros)

572+ try' (runT Intros)

568− (return ())

573+ (return ()) True

569 where

574 where

570 bname (Bind n _ _) = Just n

575 bname (Bind n _ _) = Just n

571 bname _ = Nothing

576 bname _ = Nothing

@@ -629,10 +634,52 @@ runTac autoSolve ist tac = do env <- get_env

629 runT Trivial = do trivial ist; when autoSolve solveAll

634 runT Trivial = do trivial ist; when autoSolve solveAll

630 runT (Focus n) = focus n

635 runT (Focus n) = focus n

631 runT Solve = solve

636 runT Solve = solve

632− runT (Try l r) = do try (runT l) (runT r)

637+ runT (Try l r) = do try' (runT l) (runT r) True

633 runT (TSeq l r) = do runT l; runT r

638 runT (TSeq l r) = do runT l; runT r

639+ runT (ReflectTac tm) = do attack -- let x : Tactic = tm in ...

640+ valn <- unique_hole (MN 0 "tacval")

641+ claim valn (Var tacticTy)

642+ tacn <- unique_hole (MN 0 "tacn")

643+ letbind tacn (Var tacticTy) (Var valn)

644+ focus valn

645+ elab ist toplevel False False (MN 0 "tac") tm

646+ (tm', ty') <- get_type_val (Var tacn)

647+ ctxt <- get_context

648+ env <- get_env

649+ let tactic = normalise ctxt env tm'

650+ runReflected tactic

651+-- p <- get_term

652+-- trace (show p ++ "\n\n") $

653+ return ()

654+ where tacticTy = tacm "Tactic"

655+ runT (GoalType n tac) = do g <- goal

656+ case unApply g of

657+ (P _ n' _, _) ->

658+ if nsroot n' == UN n

659+ then runT tac

660+ else fail "Wrong goal type"

661+ _ -> fail "Wrong goal type"

634 runT x = fail $ "Not implemented " ++ show x

662 runT x = fail $ "Not implemented " ++ show x

635

663

664+ runReflected t = do t' <- reify t

665+ runTac autoSolve ist t'

666+ tacm n = NS (UN n) ["Reflection", "Language"]

667+

668+ reify :: Term -> ElabD PTactic

669+ reify (P _ n _) | n == tacm "Trivial" = return Trivial

670+ reify (P _ n _) | n == tacm "Solve" = return Solve

671+ reify f@(App _ _)

672+ | (P _ f _, args) <- unApply f = reifyAp f args

673+ reify t = fail ("Unknown tactic " ++ show t)

674+

675+ reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)

676+ reifyAp t [Constant (Str x)]

677+ | t == tacm "Refine" = return $ Refine (UN x) []

678+ reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

679+ reifyAp t [Constant (Str n), x]

680+ | t == tacm "GoalType" = liftM (GoalType n) (reify x)

681+ reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

682+

636solveAll = try (do solve; solveAll) (return ())

683solveAll = try (do solve; solveAll) (return ())

637

684

638-- If the function application is specialisable, make a new

685-- If the function application is specialisable, make a new

src/Idris/IBC.hs+4

@@ -1355,6 +1355,8 @@ instance (Binary t) => Binary (PTactic' t) where

1355 put x1

1356 put x2

1357 Qed -> putWord8 15

1358+ ReflectTac x1 -> do putWord8 16

1359+ put x1

1358 get

1360 get

1359 = do i <- getWord8

1361 = do i <- getWord8

1360 case i of

1362 case i of

@@ -1386,6 +1388,8 @@ instance (Binary t) => Binary (PTactic' t) where

1386 x2 <- get

1388 x2 <- get

1387 return (TSeq x1 x2)

1389 return (TSeq x1 x2)

1388 15 -> return Qed

1390 15 -> return Qed

1391+ 16 -> do x1 <- get

1392+ return (ReflectTac x1)

1389 _ -> error "Corrupted binary data for PTactic'"

1393 _ -> error "Corrupted binary data for PTactic'"

1390

1394

1391

1395

src/Idris/Parser.hs+12−6

@@ -390,7 +390,7 @@ pSyntaxRule syn

390 when (length ns /= length (nub ns))

391 $ fail "Repeated variable in syntax rule"

392 lchar '='

393− tm <- pExpr (impOK syn)

393+ tm <- pTExpr (impOK syn)

394 pTerminator

395 return (Rule (mkSimple syms) tm sty)

396 where

@@ -738,6 +738,7 @@ pTacticsExpr syn = do

738pSimpleExpr syn =

739 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)

740 <|> do lchar '?'; x <- pName; return (PMetavar x)

741+ <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)

741 <|> do reserved "refl"; fc <- pfc;

742 <|> do reserved "refl"; fc <- pfc;

742 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';

743 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';

743 return t)

744 return t)

@@ -786,7 +787,8 @@ bracketed syn =

786 pexp (PRef fc (MN 1000 "ARG"))]))

787 pexp (PRef fc (MN 1000 "ARG"))]))

787

788

788pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)

789pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)

789−pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn

790+pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True })

791+ symbol "=>"; rhs <- pExpr syn

790 return (lhs, rhs)

792 return (lhs, rhs)

791

793

792modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

794modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

@@ -907,10 +909,11 @@ mkType (NS n s) = NS (mkType n) s

907noImp syn = syn { implicitAllowed = False }

909noImp syn = syn { implicitAllowed = False }

908impOK syn = syn { implicitAllowed = True }

910impOK syn = syn { implicitAllowed = True }

909

911

910−pTSig syn = do lchar ':'

912+pTSig syn = do lchar ':'; pTExpr syn

913+

911− cs <- if implicitAllowed syn then pConstList syn else return []

914+pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []

912− sc <- pExpr syn

915+ sc <- pExpr syn

913− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

916+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

914

917

915pLambda syn = do lchar '\\'

918pLambda syn = do lchar '\\'

916 try (do xt <- tyOptDeclList syn

919 try (do xt <- tyOptDeclList syn

@@ -1504,6 +1507,9 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1504 <|> do reserved "exact"; t <- pExpr syn;

1507 <|> do reserved "exact"; t <- pExpr syn;

1505 i <- getState

1508 i <- getState

1506 return $ Exact (desugar syn i t)

1509 return $ Exact (desugar syn i t)

1510+ <|> do reserved "reflect"; t <- pExpr syn;

1511+ i <- getState

1512+ return $ ReflectTac (desugar syn i t)

1507 <|> do reserved "try"; t <- pTactic syn;

1513 <|> do reserved "try"; t <- pTactic syn;

1508 lchar '|';

1514 lchar '|';

1509 t1 <- pTactic syn

1515 t1 <- pTactic syn

src/Idris/Primitives.hs+2−2

@@ -338,9 +338,9 @@ primitives =

338 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

339 (1, LIntStr) total,

340 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

341− (1, LNoOp) total,

341+ (1, LChInt) total,

342 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

343− (1, LNoOp) total,

343+ (1, LIntCh) total,

344 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

345 (1, LIntBig) total,

346 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)

src/Idris/REPL.hs+3−1

@@ -323,7 +323,7 @@ process fn (Prove n')

323process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

324 ctxt <- getContext

325 ist <- get

326− let tm' = simplify ctxt True [] tm

326+ let tm' = hnf ctxt [] tm

327 iputStrLn (show (delab ist tm'))

328process fn TTShell = do ist <- get

329 let shst = initState (tt_ctxt ist)

@@ -420,6 +420,7 @@ parseTarget :: String -> Target

420parseTarget "C" = ViaC

421parseTarget "Java" = ViaJava

422parseTarget "bytecode" = Bytecode

423+parseTarget "javascript" = ToJavaScript

423parseTarget _ = error "unknown target" -- FIXME: partial function

424parseTarget _ = error "unknown target" -- FIXME: partial function

424

425

425parseArgs :: [String] -> [Opt]

426parseArgs :: [String] -> [Opt]

@@ -478,6 +479,7 @@ help =

478 ([":showproof"], "<name>", "Show proof"),

479 ([":showproof"], "<name>", "Show proof"),

479 ([":proofs"], "", "Show available proofs"),

480 ([":proofs"], "", "Show available proofs"),

480 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

481 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

482+ ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),

481 ([":exec",":execute"], "", "Compile to an executable and run"),

483 ([":exec",":execute"], "", "Compile to an executable and run"),

482 ([":?",":h",":help"], "", "Display this help text"),

484 ([":?",":h",":help"], "", "Display this help text"),

483 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),

485 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),

src/Idris/REPLParser.hs+1

@@ -33,6 +33,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

33 <|> try (do cmd ["ttshell"]; eof; return TTShell)

34 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))

35 <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))

36+ <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ToJavaScript f))

36 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

37 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

37 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

38 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

38 <|> try (do cmd ["proofs"]; eof; return Proofs)

39 <|> try (do cmd ["proofs"]; eof; return Proofs)

src/Main.hs+1−1

@@ -92,4 +92,4 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

92 "\t--libdir Show library install directory and exit\n" ++

93 "\t--link Show C library directories and exit (for C linking)\n" ++

94 "\t--include Show C include directories and exit (for C linking)\n" ++

95− "\t--target [target] Type the target: C, Java, bytecode\n"

95+ "\t--target [target] Type the target: C, Java, bytecode, javascript\n"

test/reg008/expectednew file

No changes to the content.

test/reg008/reg008.idrnew file+15

@@ -0,0 +1,15 @@

1+module NatCmp

3+data Cmp : Nat -> Nat -> Type where

4+ cmpLT : (y : _) -> Cmp x (x + S y)

5+ cmpEQ : Cmp x x

6+ cmpGT : (x : _) -> Cmp (y + S x) y

8+total cmp : (x, y : Nat) -> Cmp x y

9+cmp O O = cmpEQ

10+cmp O (S k) = cmpLT _

11+cmp (S k) O = cmpGT _

12+cmp (S x) (S y) with (cmp x y)

13+ cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k

14+ cmp (S x) (S x) | cmpEQ = cmpEQ

15+ cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k

test/reg008/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg008.idr --check

3+rm -f *.ibc

test/reg009/expectednew file

No changes to the content.

test/reg009/reg009.lidrnew file+19

@@ -0,0 +1,19 @@

1+> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect alpha n) -> Bool

2+> isAnyBy _ (_ ** Nil) = False

3+> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)

6+> filterTagP : (p : alpha -> Bool) ->

7+> (as : Vect alpha n) ->

8+> so (isAnyBy p (n ** as)) ->

9+> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O)))

10+> filterTagP p (a :: as) q with (p a)

11+> | True = (_

12+> **

13+> ((a ** believe_me oh)

14+> ::

15+> (fst (getProof (filterTagP p as (believe_me oh)))),

16+> oh

17+> )

18+> )

19+> | False = filterTagP p as (believe_me oh)

test/reg009/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg009.lidr --check

3+rm -f reg009 *.ibc