add specifier check for cli compilation

Missed a case which is covered now by checking for exceptions where
postOptions is used

add *> <* to Core
This commit is contained in:
MarcelineVQ 2020-09-13 14:20:50 -07:00 committed by G. Allais
parent 7d5ec53b53
commit 1619206d24
6 changed files with 31 additions and 17 deletions

View File

@ -462,6 +462,14 @@ export
(<*>) : Core (a -> b) -> Core a -> Core b
(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]
export
(*>) : Core a -> Core b -> Core b
(*>) (MkCore a) (MkCore b) = MkCore [| a *> b |]
export
(<*) : Core a -> Core b -> Core a
(<*) (MkCore a) (MkCore b) = MkCore [| a <* b |]
export %inline
when : Bool -> Lazy (Core ()) -> Core ()
when True f = f

View File

@ -183,7 +183,8 @@ stMain cgs opts
displayErrors res
pure res
doRepl <- postOptions result opts
doRepl <- catch (postOptions result opts)
(\err => emitError err *> pure False)
if doRepl then
if ide || ideSocket then
if not ideSocket

View File

@ -8,7 +8,6 @@ import Core.Unify
import Utils.Path
import Idris.CommandLine
import Idris.Error
import Idris.REPL
import Idris.Syntax
import Idris.Version
@ -148,10 +147,9 @@ postOptions res (OutputFile outfile :: rest)
postOptions res rest
pure False
postOptions res (ExecFn str :: rest)
= catch (do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
postOptions res rest
pure False)
(\err => do perror err >>= printError; pure False)
= do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
postOptions res rest
pure False
postOptions res (CheckOnly :: rest)
= do postOptions res rest
pure False

View File

@ -2,11 +2,12 @@ module Specifiers
{- This tests both the given specifiers and the error reporting of them.
To this end it tests via:
--exec main -- testing cli
-o foo -- testing cli compilation
--exec main -- testing cli execution
> :exec main -- testing repl
> :exec main -- testing repl execution
> :set eval exec -- repl with eval set to execute
> :set eval exec -- testing repl evaluation with eval set to execute
> main
-}
@ -28,7 +29,6 @@ plusRacketOK : Int -> Int -> Int
%foreign "scheme,racket:+"
plusRacketFail : Int -> Int -> Int
-- We don't actually do any printing this is just to use the specifiers so the
-- failures are exposed.
main : IO ()

View File

@ -1,27 +1,33 @@
The given specifier was not accepted by any backend. Available backends:
Error: The given specifier was not accepted by any backend. Available backends:
chez, racket, node, javascript, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:28:1--34:5
28 | %foreign "scheme,racket:+"
29 | plusRacketFail : Int -> Int -> Int
30 |
Specifiers.idr:29:1--34:5
29 | %foreign "scheme,racket:+"
30 | plusRacketFail : Int -> Int -> Int
31 |
32 | -- We don't actually do any printing this is just to use the specifiers so the
33 | -- failures are exposed.
34 | main : IO ()
Error: The given specifier was not accepted by any backend. Available backends:
chez, racket, node, javascript, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:29:1--34:5
Main> Loaded file Specifiers.idr
Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
chez, racket, node, javascript, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:28:1--34:5
Specifiers.idr:29:1--34:5
Specifiers> [exec] Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
chez, racket, node, javascript, gambit
Some backends have additional specifier rules, refer to their documentation.
Specifiers.idr:28:1--34:5
Specifiers.idr:29:1--34:5
[exec] Specifiers>
Bye for now!

View File

@ -1,4 +1,5 @@
$1 --no-banner --no-color --console-width 0 --cg chez Specifiers.idr --exec main
$1 --no-banner --no-color --console-width 0 --cg chez Specifiers.idr -o build/foo
$1 --no-banner --no-color --console-width 0 --cg chez < input
rm -rf build