git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master' into error-reflection
7ae55f9David Christiansen
README+2
compare with master
unifiedsplit
@@ -12,3 +12,5 @@ To run the tests, type 'make test' which will execute the test suite, and
12Idris has buildtime dependencies on the C libraries llvm-3.3 and libffi. Be sure these are compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc).
12Idris has buildtime dependencies on the C libraries llvm-3.3 and libffi. Be sure these are compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc).
13
13
14Idris has a runtime dependency on libgmp, and on Boehm GC (libgc) when using the LLVM codegen. These are needed for linking into compiled programs, so be sure these are compiled for Idris's default target architecture (usually 64 bit on x86_64 systems).
14Idris has a runtime dependency on libgmp, and on Boehm GC (libgc) when using the LLVM codegen. These are needed for linking into compiled programs, so be sure these are compiled for Idris's default target architecture (usually 64 bit on x86_64 systems).
15+
16+The Idris wiki contains instructions for building on various platforms and for getting involved with development. It is located at https://github.com/idris-lang/Idris-dev/wiki .
Setup.hs+117−137
@@ -20,158 +20,138 @@ import qualified Data.Text.IO as TIO
20
20
21-- After Idris is built, we need to check and install the prelude and other libs
21-- After Idris is built, we need to check and install the prelude and other libs
22
22
23−make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"
23+-- -----------------------------------------------------------------------------
24+-- Idris Command Path
24
25
25−#ifdef mingw32_HOST_OS
26-- make on mingw32 exepects unix style separators
26-- make on mingw32 exepects unix style separators
27+#ifdef mingw32_HOST_OS
27(<//>) = (Px.</>)
28(<//>) = (Px.</>)
28−idrisCmd local = Px.joinPath $ splitDirectories $
29+idrisCmd local = Px.joinPath $ splitDirectories $ ".." <//> buildDir local <//> "idris" <//> "idris"
29− ".." <//> buildDir local <//> "idris" <//> "idris"
30−rtsDir local = Px.joinPath $ splitDirectories $
31− ".." <//> buildDir local <//> "rts" <//> "libidris_rts"
32#else
30#else
33idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
31idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
34−rtsDir local = ".." </> buildDir local </> "rts" </> "libidris_rts"
35#endif
32#endif
36
33
37−cleanStdLib verbosity
34+-- -----------------------------------------------------------------------------
38− = do make verbosity [ "-C", "lib", "clean", "IDRIS=idris" ]
35+-- Make Commands
39− make verbosity [ "-C", "effects", "clean", "IDRIS=idris" ]
36+
40− make verbosity [ "-C", "javascript", "clean", "IDRIS=idris" ]
37+make verbosity =
41−
38+ P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"
42−cleanJavaPom verbosity
39+
43− = do execPomExists <- doesFileExist ("java" </> "executable_pom.xml")
40+-- -----------------------------------------------------------------------------
44− when execPomExists $ removeFile ("java" </> "executable_pom.xml")
41+-- Flags
45−
42+
46−cleanLLVMLib verbosity = make verbosity ["-C", "llvm", "clean"]
43+usesLLVM :: S.ConfigFlags -> Bool
47−
44+usesLLVM flags =
48−installStdLib pkg local withoutEffects verbosity copy
49− = do let dirs = L.absoluteInstallDirs pkg local copy
50− let idir = datadir dirs
51− let icmd = idrisCmd local
52− putStrLn $ "Installing libraries in " ++ idir
53− make verbosity
54− [ "-C", "lib", "install"
55− , "TARGET=" ++ idir
56− , "IDRIS=" ++ icmd
57− ]
58− unless withoutEffects $
59− make verbosity
60− [ "-C", "effects", "install"
61− , "TARGET=" ++ idir
62− , "IDRIS=" ++ icmd
63− ]
64− make verbosity
65− [ "-C", "javascript", "install"
66− , "TARGET=" ++ idir
67− , "IDRIS=" ++ icmd
68− ]
69− let idirRts = idir </> "rts"
70− putStrLn $ "Installing run time system in " ++ idirRts
71− make verbosity
72− [ "-C", "rts", "install"
73− , "TARGET=" ++ idirRts
74− , "IDRIS=" ++ icmd
75− ]
76−
77−installLLVMLib verbosity pkg local copy =
78− let idir = datadir $ L.absoluteInstallDirs pkg local copy in
79− make verbosity ["-C", "llvm", "install", "TARGET=" ++ idir </> "llvm"]
80−
81−buildLLVMLib verbosity = make verbosity ["-C", "llvm", "all"]
82−
83−installJavaPom pkg local verbosity copy version = do
84− putStrLn $ "Installing java pom template"
85− let dir = datadir $ L.absoluteInstallDirs pkg local copy
86− copyFile ("java" </> "executable_pom.xml") (dir </> "executable_pom.xml")
87−
88−-- This is a hack. I don't know how to tell cabal that a data file needs
89−-- installing but shouldn't be in the distribution. And it won't make the
90−-- distribution if it's not there, so instead I just delete
91−-- the file after configure.
92−
93−removeLibIdris local verbosity
94− = do let icmd = idrisCmd local
95− make verbosity
96− [ "-C", "rts", "clean"
97− , "IDRIS=" ++ icmd
98− ]
99−
100−checkStdLib local withoutEffects verbosity
101− = do let icmd = idrisCmd local
102− putStrLn $ "Building libraries..."
103− make verbosity
104− [ "-C", "lib", "check"
105− , "IDRIS=" ++ icmd
106− ]
107− unless withoutEffects $
108− make verbosity
109− [ "-C", "effects", "check"
110− , "IDRIS=" ++ icmd
111− ]
112− make verbosity
113− [ "-C", "javascript", "check"
114− , "IDRIS=" ++ icmd
115− ]
116− make verbosity
117− [ "-C", "rts", "check"
118− , "IDRIS=" ++ icmd
119− ]
120−
121−llvmFlag flags =
122 case lookup (FlagName "llvm") (S.configConfigurationsFlags flags) of
45 case lookup (FlagName "llvm") (S.configConfigurationsFlags flags) of
123 Just True -> True
46 Just True -> True
124 Just False -> False
47 Just False -> False
125 Nothing -> True
48 Nothing -> True
126
49
127−noEffectsFlag flags =
50+usesEffects :: S.ConfigFlags -> Bool
51+usesEffects flags =
128− case lookup (FlagName "noeffects") (S.configConfigurationsFlags flags) of
52+ case lookup (FlagName "effects") (S.configConfigurationsFlags flags) of
129 Just True -> True
53 Just True -> True
130 Just False -> False
54 Just False -> False
131− Nothing -> False
55+ Nothing -> True
56+
57+-- -----------------------------------------------------------------------------
58+-- Clean
59+
60+idrisClean _ flags _ _ = do
61+ cleanStdLib
62+ cleanLLVM
63+ where
64+ verbosity = S.fromFlag $ S.cleanVerbosity flags
65+
66+ cleanStdLib = do
67+ makeClean "lib"
68+ makeClean "effects"
69+ makeClean "javascript"
70+
71+ cleanLLVM = makeClean "llvm"
72+
73+ makeClean dir = make verbosity [ "-C", dir, "clean", "IDRIS=idris" ]
74+
75+
76+-- -----------------------------------------------------------------------------
77+-- Configure
78+
79+idrisConfigure _ flags _ local = do
80+ configureRTS
81+ where
82+ verbosity = S.fromFlag $ S.configVerbosity flags
83+ version = pkgVersion . package $ localPkgDescr local
84+
85+ -- This is a hack. I don't know how to tell cabal that a data file needs
86+ -- installing but shouldn't be in the distribution. And it won't make the
87+ -- distribution if it's not there, so instead I just delete
88+ -- the file after configure.
89+ configureRTS = make verbosity ["-C", "rts", "clean"]
90+
91+-- -----------------------------------------------------------------------------
92+-- Build
93+
94+idrisBuild _ flags _ local = do
95+ buildStdLib
96+ buildRTS
97+ when (usesLLVM $ configFlags local) buildLLVM
98+ where
99+ verbosity = S.fromFlag $ S.buildVerbosity flags
100+
101+ buildStdLib = do
102+ putStrLn "Building libraries..."
103+ makeBuild "lib"
104+ when (usesEffects $ configFlags local) $ makeBuild "effects"
105+ makeBuild "javascript"
106+ where
107+ makeBuild dir = make verbosity [ "-C", dir, "build" , "IDRIS=" ++ idrisCmd local]
108+
109+ buildRTS = make verbosity ["-C", "rts", "build"]
110+
111+ buildLLVM = make verbosity ["-C", "llvm", "build"]
112+
113+-- -----------------------------------------------------------------------------
114+-- Copy/Install
115+
116+idrisInstall verbosity copy pkg local = do
117+ installStdLib
118+ installRTS
119+ when (usesLLVM $ configFlags local) installLLVM
120+ where
121+ target = datadir $ L.absoluteInstallDirs pkg local copy
122+
123+ installStdLib = do
124+ putStrLn $ "Installing libraries in " ++ target
125+ makeInstall "lib" target
126+ when (usesEffects $ configFlags local) $ makeInstall "effects" target
127+ makeInstall "javascript" target
128+
129+ installRTS = do
130+ let target' = target </> "rts"
131+ putStrLn $ "Installing run time system in " ++ target'
132+ makeInstall "rts" target'
133+
134+ installLLVM = do
135+ let target' = target </> "llvm"
136+ putStrLn $ "Installing LLVM library in " ++ target
137+ makeInstall "llvm" target
138+
139+ makeInstall src target =
140+ make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local]
132
141
133−preparePoms version
142+-- -----------------------------------------------------------------------------
134− = do execPomTemplate <- TIO.readFile ("java" </> "executable_pom_template.xml")
143+-- Main
135− TIO.writeFile ("java" </> "executable_pom.xml") (insertVersion execPomTemplate)
136− where
137− insertVersion template =
138− T.replace (T.pack "$RTS-VERSION$") (T.pack $ display version) template
139
144
140-- Install libraries during both copy and install
145-- Install libraries during both copy and install
141-- See http://hackage.haskell.org/trac/hackage/ticket/718
146-- See http://hackage.haskell.org/trac/hackage/ticket/718
142−main = do
143− defaultMainWithHooks $ simpleUserHooks
147+main = defaultMainWithHooks $ simpleUserHooks
148+ { postClean = idrisClean
149+ , postConf = idrisConfigure
150+ , postBuild = idrisBuild
144− { postCopy = \ _ flags pkg lbi -> do
151+ , postCopy = \_ flags pkg local ->
145− let verb = S.fromFlag $ S.copyVerbosity flags
152+ idrisInstall (S.fromFlag $ S.copyVerbosity flags)
146− let withoutEffects = noEffectsFlag $ configFlags lbi
147− installStdLib pkg lbi withoutEffects verb
148− (S.fromFlag $ S.copyDest flags)
149− installJavaPom pkg lbi verb
150− (S.fromFlag $ S.copyDest flags)
153+ (S.fromFlag $ S.copyDest flags) pkg local
151− (pkgVersion . package $ localPkgDescr lbi)
152− when (llvmFlag $ configFlags lbi)
153− (installLLVMLib verb pkg lbi (S.fromFlag $ S.copyDest flags))
154− , postInst = \ _ flags pkg lbi -> do
154+ , postInst = \_ flags pkg local ->
155− let verb = (S.fromFlag $ S.installVerbosity flags)
155+ idrisInstall (S.fromFlag $ S.installVerbosity flags)
156− let withoutEffects = noEffectsFlag $ configFlags lbi
157− installStdLib pkg lbi withoutEffects verb
158− NoCopyDest
159− installJavaPom pkg lbi verb
160− NoCopyDest
156+ NoCopyDest pkg local
161− (pkgVersion . package $ localPkgDescr lbi)
162− when (llvmFlag $ configFlags lbi)
163− (installLLVMLib verb pkg lbi NoCopyDest)
164− , postConf = \ _ flags _ lbi -> do
165− removeLibIdris lbi (S.fromFlag $ S.configVerbosity flags)
166− preparePoms . pkgVersion . package $ localPkgDescr lbi
167− , postClean = \ _ flags _ _ -> do
168− let verb = S.fromFlag $ S.cleanVerbosity flags
169− cleanStdLib verb
170− cleanLLVMLib verb
171− cleanJavaPom verb
172− , postBuild = \ _ flags _ lbi -> do
173− let verb = S.fromFlag $ S.buildVerbosity flags
174− when (llvmFlag $ configFlags lbi) (buildLLVMLib verb)
175− let withoutEffects = noEffectsFlag $ configFlags lbi
176− checkStdLib lbi withoutEffects verb
177− }
157+ }
effects/Makefile+5−4
@@ -1,13 +1,14 @@
1+IDRIS := idris
1
2
2−check: .PHONY
3+build: .PHONY
3 $(IDRIS) --build effects.ipkg
4 $(IDRIS) --build effects.ipkg
4
5
5−recheck: clean check
6+clean: .PHONY
7+ $(IDRIS) --clean effects.ipkg
6
8
7install:
9install:
8 $(IDRIS) --install effects.ipkg
10 $(IDRIS) --install effects.ipkg
9
11
10−clean: .PHONY
12+rebuild: clean build
11− $(IDRIS) --clean effects.ipkg
12
13
13.PHONY:
14.PHONY:
idris.cabal+166−79
@@ -14,7 +14,8 @@ Description: Idris is a general purpose language with full dependent types.
14 Dependent types allow types to be predicated on values,
14 Dependent types allow types to be predicated on values,
15 meaning that some aspects of a program's behaviour can be
15 meaning that some aspects of a program's behaviour can be
16 specified precisely in the type. The language is closely
16 specified precisely in the type. The language is closely
17− related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/documentation>.
17+ related to Epigram and Agda. There is a tutorial at
18+ <http://www.idris-lang.org/documentation>.
18 Features include:
19 Features include:
19 .
20 .
20 * Full dependent types with dependent pattern matching
21 * Full dependent types with dependent pattern matching
@@ -43,38 +44,60 @@ Description: Idris is a general purpose language with full dependent types.
43
44
44Cabal-Version: >= 1.6
45Cabal-Version: >= 1.6
45
46
46−
47Build-type: Custom
47Build-type: Custom
48
48
49−
49+Data-files: js/Runtime-browser.js
50−Data-files: rts/idris_rts.h rts/idris_gc.h rts/idris_stdfgn.h
51− rts/idris_main.c rts/idris_gmp.h
52− rts/libtest.c
53 js/Runtime-common.js
50 js/Runtime-common.js
54 js/Runtime-node.js
51 js/Runtime-node.js
55− js/Runtime-browser.js
52+ rts/idris_gc.h
53+ rts/idris_gmp.h
54+ rts/idris_main.c
55+ rts/idris_rts.h
56+ rts/idris_stdfgn.h
57+ rts/libtest.c
58+
56−Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
59+Extra-source-files:
60+ Makefile
61+ config.mk
62+
63+ rts/*.c
64+ rts/*.h
65+ rts/Makefile
66+
67+ lib/base.ipkg
68+ lib/*.idr
57− lib/Network/*.idr lib/Control/*.idr
69+ lib/Control/*.idr
58− lib/Control/Monad/*.idr lib/Language/*.idr
70+ lib/Control/Monad/*.idr
59− lib/Language/Reflection/*.idr
60− lib/System/Concurrency/*.idr
61− lib/Data/*.idr lib/Debug/*.idr
71+ lib/Data/*.idr
62 lib/Data/Vect/*.idr
72 lib/Data/Vect/*.idr
73+ lib/Debug/*.idr
63 lib/Decidable/*.idr
74 lib/Decidable/*.idr
64− tutorial/examples/*.idr lib/base.ipkg
75+ lib/Language/*.idr
65− effects/Makefile effects/*.idr effects/Effect/*.idr
76+ lib/Language/Reflection/*.idr
77+ lib/Makefile
78+ lib/Network/*.idr
79+ lib/Prelude/*.idr
80+ lib/System/Concurrency/*.idr
81+
82+ effects/Makefile
66 effects/effects.ipkg
83 effects/effects.ipkg
67− javascript/Makefile
84+ effects/Effect/*.idr
68− javascript/JavaScript/*.idr
85+ effects/*.idr
86+
87+ java/*.xml
88+
69 javascript/*.idr
89 javascript/*.idr
90+ javascript/JavaScript/*.idr
91+ javascript/Makefile
70 javascript/javascript.ipkg
92 javascript/javascript.ipkg
71− config.mk
93+
72− rts/*.c rts/*.h rts/Makefile
73− llvm/*.c llvm/Makefile
74 js/*.js
94 js/*.js
75− java/*.xml
76
95
96+ llvm/*.c
77− Makefile
97+ llvm/Makefile
98+
99+ tutorial/examples/*.idr
100+
78 test/Makefile
101 test/Makefile
79 test/runtest.pl
102 test/runtest.pl
80 test/reg001/run
103 test/reg001/run
@@ -237,76 +260,140 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
237 test/test031/*.idr
260 test/test031/*.idr
238 test/test031/expected
261 test/test031/expected
239
262
240−
241source-repository head
263source-repository head
242 type: git
264 type: git
243 location: git://github.com/edwinb/Idris-dev.git
265 location: git://github.com/edwinb/Idris-dev.git
244
266
245−Flag NoEffects
267+Flag Effects
246− Description: Do not build the effects package
268+ Description: Build the effects package
247− Default: False
269+ Default: True
248
270
249Flag LLVM
271Flag LLVM
250 Description: Build the LLVM backend
272 Description: Build the LLVM backend
251 Default: True
273 Default: True
252 manual: True
274 manual: True
253
275
254−Executable idris
276+Executable idris
255− Main-is: Main.hs
277+ Main-is: Main.hs
256− hs-source-dirs: src
278+ hs-source-dirs: src
257− Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck,
279+ Other-modules:
280+ Core.CaseTree
281+ , Core.Constraints
282+ , Core.CoreParser
283+ , Core.Elaborate
284+ , Core.Evaluate
285+ , Core.Execute
258− Core.ProofShell, Core.ProofState, Core.CoreParser,
286+ , Core.ProofShell
287+ , Core.ProofState
259− Core.ShellParser, Core.Unify, Core.Elaborate,
288+ , Core.ShellParser
260− Core.CaseTree, Core.Constraints,
289+ , Core.TT
290+ , Core.Typecheck
291+ , Core.Unify
292+
293+ , Idris.AbsSyntax
294+ , Idris.AbsSyntaxTree
295+ , Idris.Chaser
296+ , Idris.Colours
297+ , Idris.Completion
298+ , Idris.Coverage
299+ , Idris.DSL
300+ , Idris.DataOpts
301+ , Idris.Delaborate
302+ , Idris.Docs
303+ , Idris.ElabDecls
304+ , Idris.ElabTerm
305+ , Idris.Error
306+ , Idris.Help
307+ , Idris.IBC
308+ , Idris.IdeSlave
309+ , Idris.Imports
310+ , Idris.Inliner
311+ , Idris.Parser
312+ , Idris.PartialEval
313+ , Idris.Primitives
314+ , Idris.Prover
315+ , Idris.Providers
316+ , Idris.REPL
317+ , Idris.REPLParser
318+ , Idris.Transforms
319+ , Idris.Unlit
320+ , Idris.UnusedArgs
321+
322+ , IRTS.BCImp
323+ , IRTS.Bytecode
324+ , IRTS.CodegenC
325+ , IRTS.CodegenCommon
326+ , IRTS.CodegenJava
327+ , IRTS.CodegenJavaScript
328+ , IRTS.Compiler
329+ , IRTS.Defunctionalise
330+ , IRTS.DumpBC
331+ , IRTS.Inliner
332+ , IRTS.Java.ASTBuilding
333+ , IRTS.Java.JTypes
334+ , IRTS.Java.Mangling
335+ , IRTS.LParser
336+ , IRTS.Lang
337+ , IRTS.Simplified
338+
339+ , Util.Pretty
340+ , Util.System
341+ , Util.DynamicLinker
261
342
262− Idris.AbsSyntax, Idris.AbsSyntaxTree, Idris.Colours,
343+ , Pkg.Package
263− Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL,
344+ , Pkg.PParser
264− Idris.REPLParser, Idris.ElabDecls, Idris.Error,
265− Idris.Delaborate, Idris.Primitives, Idris.Imports,
266− Idris.Prover, Idris.ElabTerm,
267− Idris.Coverage, Idris.IBC, Idris.Unlit,
268− Idris.DataOpts, Idris.Transforms, Idris.DSL,
269− Idris.UnusedArgs, Idris.Docs, Idris.Completion,
270− Idris.PartialEval, Idris.Providers, Idris.Chaser,
271− Idris.Inliner,
272
345
273− Util.Pretty, Util.System, Util.DynamicLinker,
346+ -- Auto Generated
274− Pkg.Package, Pkg.PParser,
347+ Paths_idris
275
348
276− IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
349+ Build-depends: base >=4 && <5
277− IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,
350+ , Cabal
278− IRTS.Compiler, IRTS.CodegenJava, IRTS.Java.ASTBuilding,
351+ , ansi-terminal
279− IRTS.Java.JTypes, IRTS.Java.Mangling, IRTS.BCImp,
352+ , binary
280− IRTS.CodegenJavaScript,
353+ , bytestring
281− IRTS.CodegenCommon, IRTS.DumpBC
354+ , containers
355+ , directory
356+ , directory >= 1.2
357+ , filepath
358+ , haskeline >= 0.7
359+ , language-java >= 0.2.2
360+ , libffi
361+ , mtl
362+ , parsec >= 3
363+ , parsers >= 0.9
364+ , pretty
365+ , process
366+ , split
367+ , text
368+ , time >= 1.4
369+ , transformers
370+ , trifecta >= 1.1
371+ , unordered-containers
372+ , utf8-string
373+ , vector
374+ , vector-binary-instances
282
375
283− Paths_idris
376+ Extensions: MultiParamTypeClasses
377+ , FunctionalDependencies
378+ , FlexibleInstances
379+ , TemplateHaskell
284
380
285− Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal,
381+ ghc-prof-options: -auto-all -caf-all
286− haskeline>=0.7, split, directory>=1.2,
382+ ghc-options: -rtsopts
287− time>=1.4,
288− containers, process, transformers, filepath,
289− directory, binary, bytestring, text, pretty,
290− language-java>=0.2.2, libffi,
291− vector, vector-binary-instances, ansi-terminal,
292− utf8-string, unordered-containers, parsers>=0.9, trifecta>=1.1
293
383
294− Extensions: MultiParamTypeClasses, FunctionalDependencies,
295− FlexibleInstances, TemplateHaskell
296− ghc-prof-options: -auto-all -caf-all
297− ghc-options: -rtsopts
298− if os(linux)
384+ if os(linux)
299− cpp-options: -DLINUX
385+ cpp-options: -DLINUX
300− build-depends: unix
386+ build-depends: unix
301− if os(darwin)
387+ if os(darwin)
302− cpp-options: -DMACOSX
388+ cpp-options: -DMACOSX
303− build-depends: unix
389+ build-depends: unix
304− if os(windows)
390+ if os(windows)
305− cpp-options: -DWINDOWS
391+ cpp-options: -DWINDOWS
306− build-depends: Win32
392+ build-depends: Win32
307− if flag(LLVM)
393+ if flag(LLVM)
308− other-modules: IRTS.CodegenLLVM
394+ other-modules: IRTS.CodegenLLVM
309− cpp-options: -DIDRIS_LLVM
395+ cpp-options: -DIDRIS_LLVM
310− build-depends: llvm-general==3.3.8.*, llvm-general-pure==3.3.8.*
396+ build-depends: llvm-general == 3.3.8.*
397+ , llvm-general-pure == 3.3.8.*
311− else
398+ else
312− other-modules: Util.LLVMStubs
399+ other-modules: Util.LLVMStubs
javascript/Makefile+4−3
@@ -1,13 +1,14 @@
1+IDRIS := idris
1
2
2−check: .PHONY
3+build: .PHONY
3 $(IDRIS) --build javascript.ipkg
4 $(IDRIS) --build javascript.ipkg
4
5
5−recheck: clean check
6−
7install:
6install:
8 $(IDRIS) --install javascript.ipkg
7 $(IDRIS) --install javascript.ipkg
9
8
10clean: .PHONY
9clean: .PHONY
11 $(IDRIS) --clean javascript.ipkg
10 $(IDRIS) --clean javascript.ipkg
12
11
12+rebuild: clean build
13+
13.PHONY:
14.PHONY:
lib/Makefile+5−4
@@ -1,16 +1,17 @@
1+IDRIS := idris
1
2
2−check: .PHONY
3+build: .PHONY
3 $(IDRIS) --build base.ipkg
4 $(IDRIS) --build base.ipkg
4
5
5−recheck: clean check
6−
7install:
6install:
8 $(IDRIS) --install base.ipkg
7 $(IDRIS) --install base.ipkg
9
8
10clean: .PHONY
9clean: .PHONY
11 $(IDRIS) --clean base.ipkg
10 $(IDRIS) --clean base.ipkg
12
11
12+rebuild: clean build
13+
13linecount: .PHONY
14linecount: .PHONY
14− wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Data/*.idr Control/Monad/*.idr Control/*.idr
15+ find . -name '*.idr' | xargs wc -l
15
16
16.PHONY:
17.PHONY:
llvm/Makefile+1−1
@@ -5,7 +5,7 @@ SOURCES=defs.c
5OBJECTS=$(SOURCES:.c=.o)
5OBJECTS=$(SOURCES:.c=.o)
6LIB=libidris_rts.a
6LIB=libidris_rts.a
7
7
8−all: $(SOURCES) $(LIB)
8+build: $(SOURCES) $(LIB)
9
9
10$(LIB): $(OBJECTS)
10$(LIB): $(OBJECTS)
11 ar r $@ $(OBJECTS)
11 ar r $@ $(OBJECTS)
rts/Makefile+1−1
@@ -9,7 +9,7 @@ endif
9
9
10LIBTARGET = libidris_rts.a
10LIBTARGET = libidris_rts.a
11
11
12−check : $(LIBTARGET) $(DYLIBTARGET)
12+build: $(LIBTARGET) $(DYLIBTARGET)
13
13
14$(LIBTARGET) : $(OBJS)
14$(LIBTARGET) : $(OBJS)
15 ar r $(LIBTARGET) $(OBJS)
15 ar r $(LIBTARGET) $(OBJS)
src/Idris/Delaborate.hs+1−1
@@ -11,7 +11,7 @@ import Core.Evaluate
11
11
12import Debug.Trace
12import Debug.Trace
13
13
14−bugaddr = "https://github.com/edwinb/Idris-dev/issues"
14+bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
15
15
16delab :: IState -> Term -> PTerm
16delab :: IState -> Term -> PTerm
17delab i tm = delab' i tm False
17delab i tm = delab' i tm False
src/Idris/Parser.hs+201−211
@@ -89,8 +89,8 @@ isDocCommentMarker _ = False
89 -}
89 -}
90singleLineComment :: MonadicParsing m => m ()
90singleLineComment :: MonadicParsing m => m ()
91singleLineComment = try (string "--" *> satisfy isEol *> pure ())
91singleLineComment = try (string "--" *> satisfy isEol *> pure ())
92− <|> try (string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ())
92+ <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ()
93− <?> "single-line comment"
93+ <?> ""
94
94
95{- | Consumes a multi-line comment
95{- | Consumes a multi-line comment
96 MultiLineComment_t ::=
96 MultiLineComment_t ::=
@@ -107,14 +107,14 @@ singleLineComment = try (string "--" *> satisfy isEol *> pure ())
107
107
108multiLineComment :: MonadicParsing m => m ()
108multiLineComment :: MonadicParsing m => m ()
109multiLineComment = try (string "{-" *> (string "-}") *> pure ())
109multiLineComment = try (string "{-" *> (string "-}") *> pure ())
110− <|> try (string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars)
110+ <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
111− <?> "multi-line comment"
111+ <?> ""
112 where inCommentChars :: MonadicParsing m => m ()
112 where inCommentChars :: MonadicParsing m => m ()
113− inCommentChars = try (string "-}" *> pure ())
113+ inCommentChars = string "-}" *> pure ()
114− <|> try (multiLineComment *> inCommentChars)
114+ <|> try (multiLineComment) *> inCommentChars
115− <|> try (docComment '|' *> inCommentChars)
115+ <|> try (docComment '|') *> inCommentChars
116− <|> try (docComment '^' *> inCommentChars)
116+ <|> try (docComment '^') *> inCommentChars
117− <|> try (skipSome (noneOf startEnd) *> inCommentChars)
117+ <|> skipSome (noneOf startEnd) *> inCommentChars
118 <|> oneOf startEnd *> inCommentChars
118 <|> oneOf startEnd *> inCommentChars
119 <?> "end of comment"
119 <?> "end of comment"
120 startEnd :: String
120 startEnd :: String
@@ -131,7 +131,7 @@ docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; ret
131 where docComment' :: MonadicParsing m => Char -> m String
131 where docComment' :: MonadicParsing m => Char -> m String
132 docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
132 docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
133 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
133 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
134− <?> "documentation comment"
134+ <?> ""
135
135
136-- | Consumes whitespace (and comments)
136-- | Consumes whitespace (and comments)
137whiteSpace :: MonadicParsing m => m ()
137whiteSpace :: MonadicParsing m => m ()
@@ -555,9 +555,9 @@ decl syn = do notEndBlock
555 <|> instance_ syn
555 <|> instance_ syn
556 <|> do d <- dsl syn; return [d]
556 <|> do d <- dsl syn; return [d]
557 <|> directive syn
557 <|> directive syn
558− <|> try(provider syn)
558+ <|> provider syn
559 <|> transform syn
559 <|> transform syn
560− <|> try(do import_; fail "imports must be at top of file")
560+ <|> do import_; fail "imports must be at top of file"
561 <?> "declaration"
561 <?> "declaration"
562 declBody' :: IdrisParser [PDecl]
562 declBody' :: IdrisParser [PDecl]
563 declBody' = do d <- decl' syn
563 declBody' = do d <- decl' syn
@@ -575,11 +575,11 @@ Decl' ::=
575 ;
575 ;
576-}
576-}
577decl' :: SyntaxInfo -> IdrisParser PDecl
577decl' :: SyntaxInfo -> IdrisParser PDecl
578−decl' syn = try fixity
578+decl' syn = fixity
579+ <|> syntaxDecl syn
579− <|> try (fnDecl' syn)
580+ <|> fnDecl' syn
580− <|> try (data_ syn)
581+ <|> data_ syn
581− <|> try (record syn)
582+ <|> record syn
582− <|> try (syntaxDecl syn)
583 <?> "declaration"
583 <?> "declaration"
584
584
585{- | Parses a syntax extension declaration (and adds the rule to parser state)
585{- | Parses a syntax extension declaration (and adds the rule to parser state)
@@ -615,10 +615,12 @@ SyntaxSym ::= '[' Name_t ']'
615-}
615-}
616syntaxRule :: SyntaxInfo -> IdrisParser Syntax
616syntaxRule :: SyntaxInfo -> IdrisParser Syntax
617syntaxRule syn
617syntaxRule syn
618+ = do sty <- try (do
618− = do pushIndent
619+ pushIndent
619− sty <- option AnySyntax (do reserved "term"; return TermSyntax
620+ sty <- option AnySyntax (do reserved "term"; return TermSyntax
620 <|> do reserved "pattern"; return PatternSyntax)
621 <|> do reserved "pattern"; return PatternSyntax)
621− reserved "syntax"
622+ reserved "syntax"
623+ return sty)
622 syms <- some syntaxSym
624 syms <- some syntaxSym
623 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
625 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
624 let ns = mapMaybe getName syms
626 let ns = mapMaybe getName syms
@@ -699,9 +701,9 @@ fnDecl' syn = try (do doc <- option "" (docComment '|')
699 terminator
701 terminator
700 addAcc n acc
702 addAcc n acc
701 return (PTy doc syn fc opts' n ty))
703 return (PTy doc syn fc opts' n ty))
702− <|> try (postulate syn)
704+ <|> postulate syn
705+ <|> caf syn
703− <|> try (pattern syn)
706+ <|> pattern syn
704− <|> try (caf syn)
705 <?> "function declaration"
707 <?> "function declaration"
706
708
707
709
@@ -727,12 +729,12 @@ fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
727fnOpts opts
729fnOpts opts
728 = do reserved "total"; fnOpts (TotalFn : opts)
730 = do reserved "total"; fnOpts (TotalFn : opts)
729 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
731 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
730− <|> try (do lchar '%'; reserved "export"; c <- stringLiteral;
732+ <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
731− fnOpts (CExport c : opts))
733+ fnOpts (CExport c : opts)
732− <|> try (do lchar '%'; reserved "assert_total";
734+ <|> do try (lchar '%' *> reserved "assert_total");
733− fnOpts (AssertTotal : opts))
735+ fnOpts (AssertTotal : opts)
734− <|> try (do lchar '%'; reserved "reflection";
736+ <|> do try (lchar '%' *> reserved "reflection");
735− fnOpts (Reflection : opts))
737+ fnOpts (Reflection : opts)
736 <|> do lchar '%'; reserved "specialise";
738 <|> do lchar '%'; reserved "specialise";
737 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
739 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
738 fnOpts (Specialise ns : opts)
740 fnOpts (Specialise ns : opts)
@@ -775,9 +777,10 @@ Postulate ::=
775 ;
777 ;
776-}
778-}
777postulate :: SyntaxInfo -> IdrisParser PDecl
779postulate :: SyntaxInfo -> IdrisParser PDecl
778−postulate syn = do doc <- option "" (docComment '|')
780+postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
779− pushIndent
781+ pushIndent
780− reserved "postulate"
782+ reserved "postulate"
783+ return doc
781 ist <- get
784 ist <- get
782 let initOpts = if default_total ist
785 let initOpts = if default_total ist
783 then [TotalFn]
786 then [TotalFn]
@@ -902,10 +905,10 @@ FixityType ::=
902 ;
905 ;
903 -}
906 -}
904fixityType :: IdrisParser (Int -> Fixity)
907fixityType :: IdrisParser (Int -> Fixity)
905−fixityType = try (do reserved "infixl"; return Infixl)
908+fixityType = do reserved "infixl"; return Infixl
906− <|> try (do reserved "infixr"; return Infixr)
909+ <|> do reserved "infixr"; return Infixr
907− <|> try (do reserved "infix"; return InfixN)
910+ <|> do reserved "infix"; return InfixN
908− <|> try (do reserved "prefix"; return PrefixN)
911+ <|> do reserved "prefix"; return PrefixN
909 <?> "fixity type"
912 <?> "fixity type"
910
913
911{- |Parses a methods block (for type classes and instances)
914{- |Parses a methods block (for type classes and instances)
@@ -931,8 +934,10 @@ Class ::=
931 ;
934 ;
932-}
935-}
933class_ :: SyntaxInfo -> IdrisParser [PDecl]
936class_ :: SyntaxInfo -> IdrisParser [PDecl]
937+class_ syn = do (doc, acc) <- try (do
934−class_ syn = do doc <- option "" (docComment '|')
938+ doc <- option "" (docComment '|')
935− acc <- optional accessibility
939+ acc <- optional accessibility
940+ return (doc, acc))
936 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
941 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
937 let n = expandNS syn n_in
942 let n = expandNS syn n_in
938 cs <- many carg
943 cs <- many carg
@@ -1441,8 +1446,8 @@ Arg ::=
1441 ;
1446 ;
1442-}
1447-}
1443arg :: SyntaxInfo -> IdrisParser PArg
1448arg :: SyntaxInfo -> IdrisParser PArg
1444−arg syn = try (implicitArg syn)
1449+arg syn = implicitArg syn
1445− <|> try (constraintArg syn)
1450+ <|> constraintArg syn
1446 <|> do e <- simpleExpr syn
1451 <|> do e <- simpleExpr syn
1447 return (pexp e)
1452 return (pexp e)
1448 <?> "function argument"
1453 <?> "function argument"
@@ -1847,9 +1852,9 @@ do_ syn
1847 fc <- getFC
1852 fc <- getFC
1848 e <- expr syn;
1853 e <- expr syn;
1849 return (DoBindP fc i e))
1854 return (DoBindP fc i e))
1850− <|> try (do e <- expr syn
1855+ <|> do e <- expr syn
1851− fc <- getFC
1856+ fc <- getFC
1852− return (DoExp fc e))
1857+ return (DoExp fc e)
1853 <?> "do block expression"
1858 <?> "do block expression"
1854
1859
1855{- |Parses an expression in idiom brackets
1860{- |Parses an expression in idiom brackets
@@ -1922,9 +1927,11 @@ Record ::=
1922 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
1927 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
1923-}
1928-}
1924record :: SyntaxInfo -> IdrisParser PDecl
1929record :: SyntaxInfo -> IdrisParser PDecl
1930+record syn = do (doc, acc) <- try (do
1925−record syn = do doc <- option "" (docComment '|')
1931+ doc <- option "" (docComment '|')
1926− acc <- optional accessibility
1932+ acc <- optional accessibility
1927− reserved "record"
1933+ reserved "record"
1934+ return (doc, acc))
1928 fc <- getFC
1935 fc <- getFC
1929 tyn_in <- fnName
1936 tyn_in <- fnName
1930 ty <- typeSig (allowImp syn)
1937 ty <- typeSig (allowImp syn)
@@ -2152,116 +2159,108 @@ rhs syn n = do lchar '='; expr syn
2152 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
2159 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
2153
2160
2154{- |Parses a function clause
2161{- |Parses a function clause
2155−Clause ::= FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHS WhereOrTerminator
2162+RHSOrWithBlock ::= RHS WhereOrTerminator
2163+ | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2164+ ;
2165+Clause ::= WExpr+ RHSOrWithBlock
2156 | SimpleExpr '<==' FnName RHS WhereOrTerminator
2166 | SimpleExpr '<==' FnName RHS WhereOrTerminator
2157− | WExpr+ RHS WhereOrTerminator
2167+ | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
2158− | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2168+ | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
2159− | WExpr+ 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2160− | ArgExpr Operator ArgExpr WExpr* RHS WhereOrTerminator
2161− | ArgExpr Operator ArgExpr WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2162 ;
2169 ;
2163ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
2170ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
2164WhereOrTerminator ::= WhereBlock | Terminator;
2171WhereOrTerminator ::= WhereBlock | Terminator;
2165-}
2172-}
2166clause :: SyntaxInfo -> IdrisParser PClause
2173clause :: SyntaxInfo -> IdrisParser PClause
2167clause syn
2174clause syn
2168− = try (do pushIndent
2169− n_in <- fnName; let n = expandNS syn n_in
2170− cargs <- many (constraintArg syn)
2171− fc <- getFC
2172− args <- many (try (implicitArg (syn { inPattern = True } ))
2173− <|> (fmap pexp (argExpr syn)))
2174− wargs <- many (wExpr syn)
2175− r <- rhs syn n
2176− ist <- get
2177− let ctxt = tt_ctxt ist
2178− let wsyn = syn { syn_namespace = [] }
2179− (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2180− popIndent
2181− return x,
2182− do terminator
2183− return ([], [])]
2184− let capp = PApp fc (PRef fc n)
2185− (cargs ++ args)
2186− ist <- get
2187− put (ist { lastParse = Just n })
2188− return $ PClause fc n capp wargs r wheres)
2189− <|> try (do pushIndent
2175+ = do wargs <- try (do pushIndent; some (wExpr syn))
2190− ty <- simpleExpr syn
2176+ fc <- getFC
2191− symbol "<=="
2192− fc <- getFC
2193− n_in <- fnName; let n = expandNS syn n_in
2194− r <- rhs syn n
2195− ist <- get
2196− let ctxt = tt_ctxt ist
2197− let wsyn = syn { syn_namespace = [] }
2198− (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2199− popIndent
2200− return x,
2201− do terminator
2202− return ([], [])]
2203− let capp = PLet (MN 0 "match")
2204− ty
2205− (PMatchApp fc n)
2206− (PRef fc (MN 0 "match"))
2207− ist <- get
2208− put (ist { lastParse = Just n })
2209− return $ PClause fc n capp [] r wheres)
2210− <|> try (do pushIndent
2211− wargs <- some (wExpr syn)
2212− ist <- get
2177+ ist <- get
2213− n <- case lastParse ist of
2178+ n <- case lastParse ist of
2214− Just t -> return t
2179+ Just t -> return t
2215− Nothing -> fail "Invalid clause"
2180+ Nothing -> fail "Invalid clause"
2216− fc <- getFC
2217− r <- rhs syn n
2181+ (do r <- rhs syn n
2218− let ctxt = tt_ctxt ist
2182+ let ctxt = tt_ctxt ist
2219− let wsyn = syn { syn_namespace = [] }
2183+ let wsyn = syn { syn_namespace = [] }
2220− (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2184+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2221− popIndent
2185+ popIndent
2222− return x,
2186+ return x,
2223− do terminator
2187+ do terminator
2224− return ([], [])]
2188+ return ([], [])]
2225− return $ PClauseR fc wargs r wheres)
2189+ return $ PClauseR fc wargs r wheres) <|> (do
2226−
2190+ popIndent
2227− <|> try (do pushIndent
2228− n_in <- fnName; let n = expandNS syn n_in
2229− cargs <- many (constraintArg syn)
2230− fc <- getFC
2231− args <- many (try (implicitArg (syn { inPattern = True } ))
2232− <|> (fmap pexp (argExpr syn)))
2233− wargs <- many (wExpr syn)
2234− let capp = PApp fc (PRef fc n)
2235− (cargs ++ args)
2236− ist <- get
2237− put (ist { lastParse = Just n })
2238− reserved "with"
2191+ reserved "with"
2239− wval <- simpleExpr syn
2192+ wval <- simpleExpr syn
2240− openBlock
2193+ openBlock
2241− ds <- some $ fnDecl syn
2194+ ds <- some $ fnDecl syn
2242− let withs = map (fillLHSD n capp wargs) $ concat ds
2195+ let withs = concat ds
2243− closeBlock
2196+ closeBlock
2197+ return $ PWithR fc wargs wval withs)
2198+ <|> do ty <- try (do pushIndent
2199+ ty <- simpleExpr syn
2200+ symbol "<=="
2201+ return ty)
2202+ fc <- getFC
2203+ n_in <- fnName; let n = expandNS syn n_in
2204+ r <- rhs syn n
2205+ ist <- get
2206+ let ctxt = tt_ctxt ist
2207+ let wsyn = syn { syn_namespace = [] }
2208+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2209+ popIndent
2210+ return x,
2211+ do terminator
2212+ return ([], [])]
2213+ let capp = PLet (MN 0 "match")
2214+ ty
2215+ (PMatchApp fc n)
2216+ (PRef fc (MN 0 "match"))
2217+ ist <- get
2218+ put (ist { lastParse = Just n })
2219+ return $ PClause fc n capp [] r wheres
2220+ <|> do (l, op) <- try (do
2221+ pushIndent
2222+ l <- argExpr syn
2223+ op <- operator
2224+ when (op == "=" || op == "?=" ) (fail "infix clause definition with \"=\" and \"?=\" not supported ")
2225+ return (l, op))
2226+ let n = expandNS syn (UN op)
2227+ r <- argExpr syn
2228+ fc <- getFC
2229+ wargs <- many (wExpr syn)
2230+ (do rs <- rhs syn n
2231+ let wsyn = syn { syn_namespace = [] }
2232+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2233+ popIndent
2234+ return x,
2235+ do terminator
2236+ return ([], [])]
2237+ ist <- get
2238+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2239+ put (ist { lastParse = Just n })
2240+ return $ PClause fc n capp wargs rs wheres) <|> (do
2244 popIndent
2241 popIndent
2245− return $ PWith fc n capp wargs wval withs)
2246−
2247− <|> try (do wargs <- some (wExpr syn)
2248− fc <- getFC
2249 reserved "with"
2242 reserved "with"
2250 wval <- simpleExpr syn
2243 wval <- simpleExpr syn
2251 openBlock
2244 openBlock
2252 ds <- some $ fnDecl syn
2245 ds <- some $ fnDecl syn
2253− let withs = concat ds
2254 closeBlock
2246 closeBlock
2247+ ist <- get
2248+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2249+ let withs = map (fillLHSD n capp wargs) $ concat ds
2250+ put (ist { lastParse = Just n })
2255− return $ PWithR fc wargs wval withs)
2251+ return $ PWith fc n capp wargs wval withs)
2256−
2257− <|> try(do pushIndent
2252+ <|> do pushIndent
2258− l <- argExpr syn
2259− op <- operator
2260− let n = expandNS syn (UN op)
2253+ n_in <- fnName; let n = expandNS syn n_in
2261− r <- argExpr syn
2254+ cargs <- many (constraintArg syn)
2262− fc <- getFC
2255+ fc <- getFC
2256+ args <- many (try (implicitArg (syn { inPattern = True } ))
2257+ <|> (fmap pexp (argExpr syn)))
2263− wargs <- many (wExpr syn)
2258+ wargs <- many (wExpr syn)
2259+ let capp = PApp fc (PRef fc n)
2260+ (cargs ++ args)
2264− rs <- rhs syn n
2261+ (do r <- rhs syn n
2262+ ist <- get
2263+ let ctxt = tt_ctxt ist
2265 let wsyn = syn { syn_namespace = [] }
2264 let wsyn = syn { syn_namespace = [] }
2266 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2265 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2267 popIndent
2266 popIndent
@@ -2269,26 +2268,18 @@ clause syn
2269 do terminator
2268 do terminator
2270 return ([], [])]
2269 return ([], [])]
2271 ist <- get
2270 ist <- get
2272− let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2273 put (ist { lastParse = Just n })
2271 put (ist { lastParse = Just n })
2274− return $ PClause fc n capp wargs rs wheres)
2272+ return $ PClause fc n capp wargs r wheres) <|> (do
2275−
2276− <|> do l <- argExpr syn
2277− op <- operator
2278− let n = expandNS syn (UN op)
2279− r <- argExpr syn
2280− fc <- getFC
2281− wargs <- many (wExpr syn)
2282− reserved "with"
2273+ reserved "with"
2274+ ist <- get
2275+ put (ist { lastParse = Just n })
2283− wval <- simpleExpr syn
2276+ wval <- simpleExpr syn
2284− openBlock
2277+ openBlock
2285− ds <- some $ fnDecl syn
2278+ ds <- some $ fnDecl syn
2286− closeBlock
2287− ist <- get
2288− let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2289− let withs = map (fillLHSD n capp wargs) $ concat ds
2279+ let withs = map (fillLHSD n capp wargs) $ concat ds
2290− put (ist { lastParse = Just n })
2280+ closeBlock
2281+ popIndent
2291− return $ PWith fc n capp wargs wval withs
2282+ return $ PWith fc n capp wargs wval withs)
2292 <?> "function clause"
2283 <?> "function clause"
2293 where
2284 where
2294 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
2285 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
@@ -2332,13 +2323,13 @@ Codegen ::= 'C'
2332 ;
2323 ;
2333-}
2324-}
2334codegen_ :: IdrisParser Codegen
2325codegen_ :: IdrisParser Codegen
2335−codegen_ = try (do reserved "C"; return ViaC)
2326+codegen_ = do reserved "C"; return ViaC
2336− <|> try (do reserved "Java"; return ViaJava)
2327+ <|> do reserved "Java"; return ViaJava
2337− <|> try (do reserved "JavaScript"; return ViaJavaScript)
2328+ <|> do reserved "JavaScript"; return ViaJavaScript
2338− <|> try (do reserved "Node"; return ViaNode)
2329+ <|> do reserved "Node"; return ViaNode
2339− <|> try (do reserved "LLVM"; return ViaLLVM)
2330+ <|> do reserved "LLVM"; return ViaLLVM
2340− <|> try (do reserved "Bytecode"; return Bytecode)
2331+ <|> do reserved "Bytecode"; return Bytecode
2341− <?> "code generation language"
2332+ <?> "code generation language"
2342
2333
2343{- |Parses a compiler directive
2334{- |Parses a compiler directive
2344StringList ::=
2335StringList ::=
@@ -2363,45 +2354,45 @@ Directive' ::= 'lib' CodeGen String_t
2363 ;
2354 ;
2364-}
2355-}
2365directive :: SyntaxInfo -> IdrisParser [PDecl]
2356directive :: SyntaxInfo -> IdrisParser [PDecl]
2366−directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- stringLiteral;
2357+directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
2367− return [PDirective (do addLib cgn lib
2358+ return [PDirective (do addLib cgn lib
2368− addIBC (IBCLib cgn lib))])
2359+ addIBC (IBCLib cgn lib))]
2369− <|> try (do lchar '%'; reserved "link"; cgn <- codegen_; obj <- stringLiteral;
2360+ <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
2370− return [PDirective (do dirs <- allImportDirs
2361+ return [PDirective (do dirs <- allImportDirs
2371− o <- liftIO $ findInPath dirs obj
2362+ o <- liftIO $ findInPath dirs obj
2372− addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2363+ addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2373− addObjectFile cgn o)])
2364+ addObjectFile cgn o)]
2374− <|> try (do lchar '%'; reserved "flag"; cgn <- codegen_;
2365+ <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
2375− flag <- stringLiteral
2366+ flag <- stringLiteral
2376− return [PDirective (do addIBC (IBCCGFlag cgn flag)
2367+ return [PDirective (do addIBC (IBCCGFlag cgn flag)
2377− addFlag cgn flag)])
2368+ addFlag cgn flag)]
2378− <|> try (do lchar '%'; reserved "include"; cgn <- codegen_; hdr <- stringLiteral;
2369+ <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
2379− return [PDirective (do addHdr cgn hdr
2370+ return [PDirective (do addHdr cgn hdr
2380− addIBC (IBCHeader cgn hdr))])
2371+ addIBC (IBCHeader cgn hdr))]
2381− <|> try (do lchar '%'; reserved "hide"; n <- iName []
2372+ <|> do try (lchar '%' *> reserved "hide"); n <- iName []
2382− return [PDirective (do setAccessibility n Hidden
2373+ return [PDirective (do setAccessibility n Hidden
2383− addIBC (IBCAccess n Hidden))])
2374+ addIBC (IBCAccess n Hidden))]
2384− <|> try (do lchar '%'; reserved "freeze"; n <- iName []
2375+ <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
2385− return [PDirective (do setAccessibility n Frozen
2376+ return [PDirective (do setAccessibility n Frozen
2386− addIBC (IBCAccess n Frozen))])
2377+ addIBC (IBCAccess n Frozen))]
2387− <|> try (do lchar '%'; reserved "access"; acc <- accessibility
2378+ <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
2388− return [PDirective (do i <- get
2379+ return [PDirective (do i <- get
2389− put(i { default_access = acc }))])
2380+ put(i { default_access = acc }))]
2390− <|> try (do lchar '%'; reserved "default"; tot <- totality
2381+ <|> do try (lchar '%' *> reserved "default"); tot <- totality
2391− i <- get
2382+ i <- get
2392− put (i { default_total = tot } )
2383+ put (i { default_total = tot } )
2393− return [PDirective (do i <- get
2384+ return [PDirective (do i <- get
2394− put(i { default_total = tot }))])
2385+ put(i { default_total = tot }))]
2395− <|> try (do lchar '%'; reserved "logging"; i <- natural;
2386+ <|> do try (lchar '%' *> reserved "logging"); i <- natural;
2396− return [PDirective (setLogLevel (fromInteger i))])
2387+ return [PDirective (setLogLevel (fromInteger i))]
2397− <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 stringLiteral (lchar ',');
2388+ <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
2398− return [PDirective (do added <- addDyLib libs
2389+ return [PDirective (do added <- addDyLib libs
2399− case added of
2390+ case added of
2400− Left lib -> addIBC (IBCDyLib (lib_name lib))
2391+ Left lib -> addIBC (IBCDyLib (lib_name lib))
2401− Right msg ->
2392+ Right msg ->
2402− fail $ msg)])
2393+ fail $ msg)]
2403− <|> try (do lchar '%'; reserved "language"; ext <- pLangExt;
2394+ <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
2404− return [PDirective (addLangExt ext)])
2395+ return [PDirective (addLangExt ext)]
2405 <?> "directive"
2396 <?> "directive"
2406
2397
2407pLangExt :: IdrisParser LanguageExt
2398pLangExt :: IdrisParser LanguageExt
@@ -2420,7 +2411,7 @@ totality
2420Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
2411Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
2421 -}
2412 -}
2422provider :: SyntaxInfo -> IdrisParser [PDecl]
2413provider :: SyntaxInfo -> IdrisParser [PDecl]
2423−provider syn = do lchar '%'; reserved "provide";
2414+provider syn = do try (lchar '%' *> reserved "provide");
2424 lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2415 lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2425 fc <- getFC
2416 fc <- getFC
2426 reserved "with"
2417 reserved "with"
@@ -2432,7 +2423,7 @@ provider syn = do lchar '%'; reserved "provide";
2432Transform ::= '%' 'transform' Expr '==>' Expr
2423Transform ::= '%' 'transform' Expr '==>' Expr
2433-}
2424-}
2434transform :: SyntaxInfo -> IdrisParser [PDecl]
2425transform :: SyntaxInfo -> IdrisParser [PDecl]
2435−transform syn = do lchar '%'; reserved "transform";
2426+transform syn = do try (lchar '%' *> reserved "transform")
2436 -- leave it unchecked, until we work out what this should
2427 -- leave it unchecked, until we work out what this should
2437 -- actually mean...
2428 -- actually mean...
2438-- safety <- option True (do reserved "unsafe"
2429-- safety <- option True (do reserved "unsafe"
@@ -2774,4 +2765,3 @@ addHides xs = do i <- getIState
2774
2765
2775 doHide (n, a) = do setAccessibility n a
2766 doHide (n, a) = do setAccessibility n a
2776 addIBC (IBCAccess n a)
2767 addIBC (IBCAccess n a)
2777−