3c5327f · Idris-dev · git.iko.soy

docs/tutorial/interp.rst+9

compare with master

unifiedsplit

@@ -68,6 +68,15 @@ The full representation of expressions is:

68 Lazy (Expr G a) ->

69 Lazy (Expr G a) -> Expr G a

70

71+The code above makes use of the ``Vect`` and ``Fin`` types from the

72+Idris standard library. We import them because they are not provided

73+in the prelude:

74+

75+.. code-block:: idris

76+

77+ import Data.Vect

78+ import Data.Fin

79+

71Since expressions are indexed by their type, we can read the typing

80Since expressions are indexed by their type, we can read the typing

72rules of the language from the definitions of the constructors. Let us

81rules of the language from the definitions of the constructors. Let us

73look at each constructor in turn.

82look at each constructor in turn.

docs/tutorial/typesfuns.rst+4

@@ -105,6 +105,10 @@ symbols:

105

106 :+-*/=_.?|&><!@$%^~.

107

108+Some operators built from these symbols can't be user defined. These are

109+``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,

110+``==>``, ``\\``, ``%``, ``~``, ``?``, and ``!``.

111+

108Functions

112Functions

109=========

113=========

110

114

idris.cabal+1

@@ -785,6 +785,7 @@ Library

785 , Idris.Core.TT

786 , Idris.Core.Typecheck

787 , Idris.Core.Unify

788+ , Idris.Core.WHNF

788

789

789 , Idris.Elab.Utils

790 , Idris.Elab.Utils

790 , Idris.Elab.Type

791 , Idris.Elab.Type

jsrts/Runtime-common.js+15−12

@@ -63,26 +63,29 @@ var i$CALL = function(fun,args) {

63

64var i$ffiWrap = function(fid,oldbase,myoldbase) {

65 return function() {

66+ var oldstack = i$callstack;

66 i$callstack = [];

67 i$callstack = [];

67

68

68 var res = fid;

69 var res = fid;

69

70

70 for(var i = 0; i < (arguments.length ? arguments.length : 1); ++i) {

71 for(var i = 0; i < (arguments.length ? arguments.length : 1); ++i) {

72+ while (res instanceof i$CON) {

71− i$valstack_top += 1;

73+ i$valstack_top += 1;

72− i$valstack[i$valstack_top] = res;

74+ i$valstack[i$valstack_top] = res;

73− i$valstack[i$valstack_top + 1] = arguments[i];

75+ i$valstack[i$valstack_top + 1] = arguments[i];

74− i$SLIDE(2);

76+ i$SLIDE(2);

75− i$valstack_top = i$valstack_base + 2;

77+ i$valstack_top = i$valstack_base + 2;

76− i$CALL(_idris__123_APPLY0_125_,[oldbase])

78+ i$CALL(_idris__123_APPLY0_125_,[oldbase])

77− while (i$callstack.length) {

79+ while (i$callstack.length) {

78− var func = i$callstack.pop();

80+ var func = i$callstack.pop();

79− var args = i$callstack.pop();

81+ var args = i$callstack.pop();

80− func.apply(this,args);

82+ func.apply(this,args);

83+ }

84+ res = i$ret;

81 }

85 }

82− res = i$ret;

83 }

86 }

84

87

85− i$callstack = i$vm.callstack;

88+ i$callstack = oldstack;

86

89

87 return i$ret;

90 return i$ret;

88 }

91 }

src/IRTS/CodegenC.hs+1−1

@@ -64,7 +64,7 @@ codegenC' defs out exec incs objs libs flags exports iface dbg

64 (if (exec == Executable) then mprog else hi)

65 case exec of

66 MavenProject -> putStrLn ("FAILURE: output type not supported")

67− Raw -> writeFile out cout

67+ Raw -> writeSource out cout

68 _ -> do

69 (tmpn, tmph) <- tempfile

70 hPutStr tmph cout

src/IRTS/CodegenJavaScript.hs+7−6

@@ -132,12 +132,12 @@ codegenJS_all target definitions includes libs filename outputType = do

132 ++ idrRuntime

133 ++ tgtRuntime

134 )

135− TIO.writeFile filename ( T.pack runtime

135+ writeSourceText filename ( T.pack runtime

136− `T.append` T.concat (map compileJS opt)

136+ `T.append` T.concat (map compileJS opt)

137− `T.append` T.concat (map compileJS cons)

137+ `T.append` T.concat (map compileJS cons)

138− `T.append` main

138+ `T.append` main

139− `T.append` invokeMain

139+ `T.append` invokeMain

140− )

140+ )

141 setPermissions filename (emptyPermissions { readable = True

142 , executable = target == Node

143 , writable = True

@@ -1331,6 +1331,7 @@ translateBC info bc

1331 | TAILCALL n <- bc = jsTAILCALL info n

1332 | FOREIGNCALL r _ (FStr n) args

1333 <- bc = jsFOREIGN info r n (map fcall args)

1334+ | FOREIGNCALL _ _ _ _ <- bc = error "JS FFI call not statically known"

1334 | TOPBASE n <- bc = jsTOPBASE info n

1335 | TOPBASE n <- bc = jsTOPBASE info n

1335 | BASETOP n <- bc = jsBASETOP info n

1336 | BASETOP n <- bc = jsBASETOP info n

1336 | STOREOLD <- bc = jsSTOREOLD info

1337 | STOREOLD <- bc = jsSTOREOLD info

src/IRTS/Compiler.hs+1−1

@@ -136,7 +136,7 @@ generate codegen mainmod ir

136 Via "c" -> codegenC ir

137 -- Any external code generator

138 Via cg -> do let cmd = "idris-" ++ cg

139− args = [mainmod, "-o", outputFile ir]

139+ args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir

140 exit <- rawSystem cmd args

141 when (exit /= ExitSuccess) $

142 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)

src/Idris/AbsSyntaxTree.hs+2−1

@@ -387,7 +387,7 @@ data Command = Quit

387 | Universes

388 | LogLvl Int

389 | Spec PTerm

390− | HNF PTerm

390+ | WHNF PTerm

391 | TestInline PTerm

392 | Defn Name

393 | Missing Name

@@ -472,6 +472,7 @@ data Opt = Filename String

472 | DumpDefun String

473 | DumpCases String

474 | UseCodegen Codegen

475+ | CodegenArgs String

475 | OutputTy OutputType

476 | OutputTy OutputType

476 | Extension LanguageExt

477 | Extension LanguageExt

477 | InterpretScript String

478 | InterpretScript String

src/Idris/CmdOptions.hs+2−1

@@ -126,7 +126,8 @@ parseFlags = many $

126 <|> flag' (OutputTy MavenProject) (long "mvn" <> help "Create a maven project (for Java codegen)")

127 <|> (DumpDefun <$> strOption (long "dumpdefuns"))

128 <|> (DumpCases <$> strOption (long "dumpcases"))

129− <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Java, bytecode"))

129+ <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))

130+ <|> (CodegenArgs <$> strOption (long "cg-opt" <> metavar "ARG" <> help "Arguments to pass to code generator"))

130 <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

131 <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

131 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

132 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

132 <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

133 <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

src/Idris/Core/Evaluate.hs+8−1

@@ -2,7 +2,7 @@

2 PatternGuards #-}

3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

4

5−module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,

6 rt_simplify, simplify, specialise, hnf, convEq, convEq',

7 Def(..), CaseInfo(..), CaseDefs(..),

8 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),

@@ -92,6 +92,13 @@ normaliseTrace tr ctxt env t

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

93 quote 0 val) initEval

94

95+toValue :: Context -> Env -> TT Name -> Value

96+toValue ctxt env t

97+ = evalState (eval False ctxt [] (map finalEntry env) t []) initEval

98+

99+quoteTerm :: Value -> TT Name

100+quoteTerm val = evalState (quote 0 val) initEval

101+

95-- Return a specialised name, and an updated list of reductions available,

102-- Return a specialised name, and an updated list of reductions available,

96-- so that the caller can tell how much specialisation was achieved.

103-- so that the caller can tell how much specialisation was achieved.

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

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

src/Idris/Core/TT.hs+1−1

@@ -41,7 +41,7 @@ module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)

41 sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm,

42 substV, sUN, tcname, termSmallerThan, tfail, thead, tnull,

43 toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,

44− uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP) where

44+ uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm) where

45

46-- Work around AMP without CPP

47import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,

src/Idris/Core/WHNF.hsnew file+208

@@ -0,0 +1,208 @@

1+{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3+

4+-- Reduction to Weak Head Normal Form

5+module Idris.Core.WHNF(whnf, WEnv) where

6+

7+import Idris.Core.TT

8+import Idris.Core.CaseTree

9+import Idris.Core.Evaluate hiding (quote)

10+import qualified Idris.Core.Evaluate as Evaluate

11+

12+import Debug.Trace

13+

14+-- A stack entry consists of a term and the environment it is to be

15+-- evaluated in (i.e. it's a thunk)

16+type StackEntry = (Term, WEnv)

17+data WEnv = WEnv Int -- number of free variables

18+ [(Term, WEnv)]

19+ deriving Show

20+

21+type Stack = [StackEntry]

22+

23+-- A WHNF is a top level term evaluated in the empty environment. It is

24+-- always headed by either an irreducible expression, i.e. a constructor,

25+-- a lambda, a constant, or a postulate

26+

27+-- Every 'Term' or 'Type' in this structure is associated with the

28+-- environment it was encountered in, so that when we quote back to a term

29+-- we get the substitutions right.

30+

31+data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- data constructor

32+ | WTCon Int Int Name (Type, WEnv) -- type constructor

33+ | WPRef Name (Type, WEnv) -- irreducible global (e.g. a postulate)

34+ | WBind Name (Binder Term) (Term, WEnv)

35+ | WApp WHNF (Term, WEnv)

36+ | WConstant Const

37+ | WProj WHNF Int

38+ | WType UExp

39+ | WUType Universe

40+ | WErased

41+ | WImpossible

42+

43+-- Reduce a *closed* term to weak head normal form.

44+whnf :: Context -> Term -> Term

45+whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)

46+

47+do_whnf :: Context -> WEnv -> Term -> WHNF

48+do_whnf ctxt env tm = eval env [] tm

49+ where

50+ eval :: WEnv -> Stack -> Term -> WHNF

51+ eval wenv@(WEnv d env) stk (V i)

52+ | i < length env = let (tm, env') = env !! i in

53+ eval env' stk tm

54+ | otherwise = error "Can't happen: WHNF scope error"

55+ eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)

56+ = eval (WEnv d ((v, wenv) : env)) stk sc

57+ eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)

58+ eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)

59+ = eval (WEnv d ((tm, tenv) : env)) stk sc

60+

61+ eval env stk (P nt n ty) = apply env nt n ty stk

62+ eval env stk (App _ f a) = eval env ((a, env) : stk) f

63+ eval env stk (Constant c) = unload (WConstant c) stk

64+

65+ -- Should never happen in compile time code (for now...)

66+ eval env stk (Proj tm i) = unload (WProj (eval env [] tm) i) stk

67+

68+ eval env stk Erased = unload WErased stk

69+ eval env stk Impossible = unload WImpossible stk

70+ eval env stk (TType u) = unload (WType u) stk

71+ eval env stk (UType u) = unload (WUType u) stk

72+

73+ apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF

74+ apply env nt n ty stk

75+ = let wp = case nt of

76+ DCon t a u -> WDCon t a u n (ty, env)

77+ TCon t a -> WTCon t a n (ty, env)

78+ _ -> WPRef n (ty, env)

79+ in

80+ case lookupDefExact n ctxt of

81+ Just (CaseOp ci _ _ _ _ cd) ->

82+ let (ns, tree) = cases_compiletime cd in

83+ case evalCase env ns tree stk of

84+ Just w -> w

85+ Nothing -> unload wp stk

86+ Just (Operator _ i op) ->

87+ if i <= length stk

88+ then case runOp env op (take i stk) (drop i stk) of

89+ Just v -> v

90+ Nothing -> unload wp stk

91+ else unload wp stk

92+ _ -> unload wp stk

93+

94+ unload :: WHNF -> Stack -> WHNF

95+ unload f [] = f

96+ unload f (a : as) = unload (WApp f a) as

97+

98+ runOp :: WEnv -> ([Value] -> Maybe Value) -> Stack -> Stack -> Maybe WHNF

99+ runOp env op stk rest

100+ = do vals <- mapM tmtoValue stk

101+ case op vals of

102+ Just (VConstant c) -> Just $ unload (WConstant c) rest

103+ -- Operators run on values, so we have to convert back

104+ -- and forth. This is pretty ugly, but operators that

105+ -- aren't run on constants are themselves pretty ugly

106+ -- (it's prim__believe_me and prim__syntacticEq, for

107+ -- example) so let's not worry too much...

108+ Just val -> Just $ eval env rest (quoteTerm val)

109+ _ -> Nothing

110+

111+ tmtoValue :: (Term, WEnv) -> Maybe Value

112+ tmtoValue (tm, tenv)

113+ = case eval tenv [] tm of

114+ WConstant c -> Just (VConstant c)

115+ _ -> let tm' = quoteEnv tenv tm in

116+ Just (toValue ctxt [] tm')

117+

118+ evalCase :: WEnv -> [Name] -> SC -> Stack -> Maybe WHNF

119+ evalCase wenv@(WEnv d env) ns tree args

120+ | length ns > length args = Nothing

121+ | otherwise = let args' = take (length ns) args

122+ rest = drop (length ns) args in

123+ do (tm, amap) <- evalTree wenv (zip ns args') tree

124+ let wtm = pToVs (map fst amap) tm

125+ Just $ eval (WEnv d (map snd amap)) rest wtm

126+

127+ evalTree :: WEnv -> [(Name, (Term, WEnv))] -> SC ->

128+ Maybe (Term, [(Name, (Term, WEnv))])

129+ evalTree env amap (STerm tm) = Just (tm, amap)

130+ evalTree env amap (Case _ n alts)

131+ = case lookup n amap of

132+ Just (tm, tenv) -> findAlt env amap

133+ (deconstruct (eval tenv [] tm) []) alts

134+ _ -> Nothing

135+ evalTree _ _ _ = Nothing

136+

137+ deconstruct :: WHNF -> Stack -> (WHNF, Stack)

138+ deconstruct (WApp f arg) stk = deconstruct f (arg : stk)

139+ deconstruct t stk = (t, stk)

140+

141+ findAlt :: WEnv -> [(Name, (Term, WEnv))] -> (WHNF, Stack) ->

142+ [CaseAlt] ->

143+ Maybe (Term, [(Name, (Term, WEnv))])

144+ findAlt env amap (WDCon tag _ _ _ _, args) alts

145+ | Just (ns, sc) <- findTag tag alts

146+ = let amap' = updateAmap (zip ns args) amap in

147+ evalTree env amap' sc

148+ | Just sc <- findDefault alts

149+ = evalTree env amap sc

150+ findAlt env amap (WConstant c, []) alts

151+ | Just sc <- findConst c alts

152+ = evalTree env amap sc

153+ | Just sc <- findDefault alts

154+ = evalTree env amap sc

155+ findAlt _ _ _ _ = Nothing

156+

157+ findTag :: Int -> [CaseAlt] -> Maybe ([Name], SC)

158+ findTag i [] = Nothing

159+ findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)

160+ findTag i (_ : xs) = findTag i xs

161+

162+ findDefault :: [CaseAlt] -> Maybe SC

163+ findDefault [] = Nothing

164+ findDefault (DefaultCase sc : xs) = Just sc

165+ findDefault (_ : xs) = findDefault xs

166+

167+ findConst c [] = Nothing

168+ findConst c (ConstCase c' v : xs) | c == c' = Just v

169+ findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v

170+ findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v

171+ findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v

172+ findConst StrType (ConCase n 4 [] v : xs) = Just v

173+ findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v

174+ findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)

175+ | tag == 7 + fromEnum ity = Just v

176+ findConst c (_ : xs) = findConst c xs

177+

178+ updateAmap newm amap

179+ = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap

180+

181+quote :: WHNF -> Term

182+quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty)

183+quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty)

184+quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)

185+quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)

186+quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a)

187+quote (WConstant c) = Constant c

188+quote (WProj t i) = Proj (quote t) i

189+quote (WType u) = TType u

190+quote (WUType u) = UType u

191+quote WErased = Erased

192+quote WImpossible = Impossible

193+

194+quoteEnv :: WEnv -> Term -> Term

195+quoteEnv (WEnv d ws) tm = qe' d ws tm

196+ where

197+ qe' d ts (V i)

198+ | i < d = V i

199+ | otherwise = let (tm, env) = ts !! (i - d) in

200+ quoteEnv env tm

201+ qe' d ts (Bind n b sc)

202+ = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)

203+ qe' d ts (App c f a)

204+ = App c (qe' d ts f) (qe' d ts a)

205+ qe' d ts (P nt n ty) = P nt n (qe' d ts ty)

206+ qe' d ts (Proj tm i) = Proj (qe' d ts tm) i

207+ qe' d ts tm = tm

208+

src/Idris/Delaborate.hs+1−1

@@ -344,7 +344,7 @@ pprintErr' i (InvalidTCArg n t)

344 text "(Type class arguments must be injective)"

345pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

346 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as)))

347−pprintErr' i (NoValidAlts as) = text "Can't disambiguate since no alternative is valid:" <+>

347+pprintErr' i (NoValidAlts as) = text "Can't disambiguate since no name has a suitable type:" <+>

348 indented (align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as))))

349pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

350pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

src/Idris/Elab/Clause.hs+1−1

@@ -594,7 +594,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

594 rep <- useREPL

595 when rep $ do

596 addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?

597− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))

597+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))

598

599 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

600 -- Elaborate where block

src/Idris/Elab/Type.hs+1−1

@@ -148,7 +148,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

148 rep <- useREPL

149 when rep $ do

150 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

151− addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

151+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

152

153 let (fam, _) = unApply (getRetTy nty')

154 let corec = case fam of

src/Idris/REPL.hs+10−3

@@ -54,6 +54,7 @@ import Idris.Core.Evaluate

54import Idris.Core.Execute (execute)

55import Idris.Core.TT

56import Idris.Core.Unify

57+import Idris.Core.WHNF

57import Idris.Core.Constraints

58import Idris.Core.Constraints

58

59

59import IRTS.Compiler

60import IRTS.Compiler

@@ -595,7 +596,7 @@ idemodeProcess fn (Search ps t) = process fn (Search ps t)

595idemodeProcess fn (Spec t) = process fn (Spec t)

596idemodeProcess fn (Spec t) = process fn (Spec t)

596-- RmProof and AddProof not supported!

597-- RmProof and AddProof not supported!

597idemodeProcess fn (ShowProof n') = process fn (ShowProof n')

598idemodeProcess fn (ShowProof n') = process fn (ShowProof n')

598−idemodeProcess fn (HNF t) = process fn (HNF t)

599+idemodeProcess fn (WHNF t) = process fn (WHNF t)

599--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!

600--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!

600idemodeProcess fn (TestInline t) = process fn (TestInline t)

601idemodeProcess fn (TestInline t) = process fn (TestInline t)

601

602

@@ -1135,11 +1136,11 @@ process fn (Prove mode n')

1135 mapM_ checkDeclTotality (idris_totcheck i)

1136 mapM_ checkDeclTotality (idris_totcheck i)

1136 warnTotality

1137 warnTotality

1137

1138

1138−process fn (HNF t)

1139+process fn (WHNF t)

1139 = do (tm, ty) <- elabVal recinfo ERHS t

1140 = do (tm, ty) <- elabVal recinfo ERHS t

1140 ctxt <- getContext

1141 ctxt <- getContext

1141 ist <- getIState

1142 ist <- getIState

1142− let tm' = hnf ctxt [] tm

1143+ let tm' = whnf ctxt tm

1143 iPrintResult (show (delab ist tm'))

1144 iPrintResult (show (delab ist tm'))

1144process fn (TestInline t)

1145process fn (TestInline t)

1145 = do (tm, ty) <- elabVal recinfo ERHS t

1146 = do (tm, ty) <- elabVal recinfo ERHS t

@@ -1600,6 +1601,8 @@ idrisMain opts =

1600 let cgn = case opt getCodegen opts of

1601 let cgn = case opt getCodegen opts of

1601 [] -> Via "c"

1602 [] -> Via "c"

1602 xs -> last xs

1603 xs -> last xs

1604+ let cgFlags = opt getCodegenArgs opts

1605+

1603 -- Now set/unset specifically chosen optimisations

1606 -- Now set/unset specifically chosen optimisations

1604 sequence_ (opt getOptimisation opts)

1607 sequence_ (opt getOptimisation opts)

1605 script <- case opt getExecScript opts of

1608 script <- case opt getExecScript opts of

@@ -1624,6 +1627,7 @@ idrisMain opts =

1624 setOutputTy outty

1627 setOutputTy outty

1625 setNoBanner nobanner

1628 setNoBanner nobanner

1626 setCodegen cgn

1629 setCodegen cgn

1630+ mapM_ (addFlag cgn) cgFlags

1627 mapM_ makeOption opts

1631 mapM_ makeOption opts

1628 -- if we have the --bytecode flag, drop into the bytecode assembler

1632 -- if we have the --bytecode flag, drop into the bytecode assembler

1629 case bcs of

1633 case bcs of

@@ -1838,6 +1842,9 @@ getCodegen :: Opt -> Maybe Codegen

1838getCodegen (UseCodegen x) = Just x

1842getCodegen (UseCodegen x) = Just x

1839getCodegen _ = Nothing

1843getCodegen _ = Nothing

1840

1844

1845+getCodegenArgs :: Opt -> Maybe String

1846+getCodegenArgs (CodegenArgs args) = Just args

1847+getCodegenArgs _ = Nothing

1841

1848

1842getConsoleWidth :: Opt -> Maybe ConsoleWidth

1849getConsoleWidth :: Opt -> Maybe ConsoleWidth

1843getConsoleWidth (UseConsoleWidth x) = Just x

1850getConsoleWidth (UseConsoleWidth x) = Just x

src/Idris/REPLParser.hs+6−6

@@ -111,7 +111,7 @@ parserCommands =

111

112 , exprArgCmd ["patt"] Pattelab "(Debugging) Elaborate pattern expression"

113 , exprArgCmd ["spec"] Spec "?"

114− , exprArgCmd ["hnf"] HNF "?"

114+ , exprArgCmd ["whnf"] WHNF "(Debugging) Show weak head normal form of an expression"

115 , exprArgCmd ["inline"] TestInline "?"

116 , proofArgCmd ["cs", "casesplit"] CaseSplitAt

117 ":cs <line> <name> splits the pattern variable on the line"

@@ -309,14 +309,14 @@ cmd_execute name = do

309

310cmd_dynamic :: String -> P.IdrisParser (Either String Command)

311cmd_dynamic name = do

312− let emptyArgs = noArgs ListDynamic name

313−

314− let oneArg = do l <- many anyChar

312+ let optArg = do l <- many anyChar

313+ if (l /= "")

315− return $ Right (DynamicLink l)

314+ then return $ Right (DynamicLink l)

315+ else return $ Right ListDynamic

316

317 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

318

319− try emptyArgs <|> try oneArg <|> failure

319+ try optArg <|> failure

320

321cmd_pprint :: String -> P.IdrisParser (Either String Command)

322cmd_pprint name = do

src/Util/System.hs+8−1

@@ -1,9 +1,12 @@

1{-# LANGUAGE CPP #-}

2module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,

3+ writeSource, writeSourceText, readSource,

3− writeSource, readSource, setupBundledCC) where

4+ setupBundledCC) where

4

5

5-- System helper functions.

6-- System helper functions.

6import Control.Monad (when)

7import Control.Monad (when)

8+import qualified Data.Text as T

9+import qualified Data.Text.IO as TIO

7import System.Directory (getTemporaryDirectory

10import System.Directory (getTemporaryDirectory

8 , removeFile

11 , removeFile

9 , removeDirectoryRecursive

12 , removeDirectoryRecursive

@@ -44,6 +47,10 @@ readSource f = do h <- openFile f ReadMode

44writeSource :: FilePath -> String -> IO ()

47writeSource :: FilePath -> String -> IO ()

45writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)

48writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)

46

49

50+-- | Write a utf-8 source file from Text

51+writeSourceText :: FilePath -> T.Text -> IO ()

52+writeSourceText f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> TIO.hPutStr h s)

53+

47withTempdir :: String -> (FilePath -> IO a) -> IO a

54withTempdir :: String -> (FilePath -> IO a) -> IO a

48withTempdir subdir callback

55withTempdir subdir callback

49 = do dir <- getTemporaryDirectory

56 = do dir <- getTemporaryDirectory

test/totality007/expected.msysnew file+5

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

1+Entering directory `.\src'

2+Totality.idr:4:1:

3+Totality.foo is not total as there are missing cases

4+Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

5+Leaving directory `.\src'