idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:idris-lang/Idris2 into ide-protocol-holes

Browse Source
This commit is contained in:
Ohad Kammar 2020-05-25 07:14:33 +01:00
commit 0de2f6dea8
49 changed files with 862 additions and 481 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1,3 +1,4 @@
idris2docs_venv
*~
*.ibc
*.ttc

4
docs/source/reference/envvars.rst
View File

@ -4,4 +4,6 @@
Environment Variables
*********************
[TODO: Fill in the environment variables recognised by Idris 2]
.. todo::
Fill in the environment variables recognised by Idris 2

2
docs/source/reference/records.rst
View File

@ -14,7 +14,7 @@ Lexical structure
constructor ``RF "foo"``)
* ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
identifier: ``NSIdent ["baz", "bar", "Foo"]``
identifier: ``DotSepIdent ["baz", "bar", "Foo"]``
* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
``.bar``, ``.baz``

10
docs/source/tutorial/miscellany.rst
View File

@ -81,9 +81,9 @@ number as 0), we could write:
.. code-block:: idris
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
and will return the 5th fibonacci number. Note that while this works, this is not the
@ -114,7 +114,9 @@ any other character).
Cumulativity
============
[NOT YET IN IDRIS 2]
.. warning::
NOT YET IN IDRIS 2
Since values can appear in types and *vice versa*, it is natural that
types themselves have types. For example:

6
docs/source/tutorial/starting.rst
View File

@ -28,14 +28,14 @@ You can download the Idris 2 source from the `Idris web site
<https://www.idris-lang.org/pages/download.html>`_ or get the latest
development version from `idris-lang/Idris2
<https://github.com/idris-lang/Idris2>`_ on Github. This includes the Idris 2
source code and the Scheme code code generated from that. Once you have
source code and the Scheme code generated from that. Once you have
unpacked the source, you can install it as follows::
make bootstrap SCHEME=chez
Where `chez` is the executable name of the Chez Scheme compiler. This will
vary from system to system, but is often one of `scheme`, `chezscheme`, or
`chezscheme9.5`. If you are building via Racket, you can install it as
vary from system to system, but is often one of ``scheme``, ``chezscheme``, or
``chezscheme9.5``. If you are building via Racket, you can install it as
follows::
make bootstrap-racket

4
docs/source/tutorial/theorems.rst
View File

@ -361,7 +361,9 @@ total, a function ``f`` must:
Directives and Compiler Flags for Totality
------------------------------------------
[NOTE: Not all of this is implemented yet for Idris 2]
.. warning::
Not all of this is implemented yet for Idris 2
By default, Idris allows all well-typed definitions, whether total or not.
However, it is desirable for functions to be total as far as possible, as this

31
docs/source/tutorial/typesfuns.rst
View File

@ -234,6 +234,37 @@ of how this works in practice:
.. _sect-holes:
Totality and Covering
---------------------
By default, functions in Idris must be ``covering``. That is, there must be
patterns which cover all possible values of the inputs types. For example,
the following definition will give an error:
.. code-block:: idris
fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
This gives an error because ``fromMaybe Nothing`` is not defined. Idris
reports:
::
frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases:
fromMaybe Nothing
You can override this with a ``partial`` annotation:
.. code-block:: idris
partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
However, this is not advisable, and in general you should only do this during
the initial development of a function, or during debugging. If you try to
evaluate ``fromMaybe Nothing`` at run time you will get a run time error.
Holes
-----

4
docs/source/tutorial/views.rst
View File

@ -4,7 +4,9 @@
Views and the “``with``” rule
*****************************
[NOT UPDATED FOR IDRIS 2 YET]
.. warning::
NOT UPDATED FOR IDRIS 2 YET
Dependent pattern matching
==========================

4
docs/source/typedd/typedd.rst
View File

@ -461,4 +461,6 @@ In ``ATM.idr``, add:
Chapter 15
----------
TODO
.. todo::
This chapter.

15
docs/source/updates/updates.rst
View File

@ -425,6 +425,21 @@ can see if we try evaluating ``myShow True`` at the REPL:
In fact, this is how interfaces are elaborated. However, ``%hint`` should be
used with care. Too many hints can lead to a large search space!
Record fields
-------------
Record fields can now be accessed via a ``.``. For example, if you have:
.. code-block:: idris
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
and you have a record ``fred : Person``, then you can use ``fred.firstName``
to access the ``firstName`` field.
Totality and Coverage
---------------------

3
idris2.ipkg
View File

@ -84,9 +84,12 @@ modules =
Idris.Version,
Parser.Lexer.Common,
Parser.Lexer.Package,
Parser.Lexer.Source,
Parser.Rule.Common,
Parser.Rule.Package,
Parser.Rule.Source,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

3
idris2api.ipkg
View File

@ -83,9 +83,12 @@ modules =
Idris.Version,
Parser.Lexer.Common,
Parser.Lexer.Package,
Parser.Lexer.Source,
Parser.Rule.Common,
Parser.Rule.Package,
Parser.Rule.Source,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

8
src/Compiler/Common.idr
View File

@ -145,6 +145,11 @@ getAllDesc (n@(Resolved i) :: rest) arr defs
getAllDesc (n :: rest) arr defs
= getAllDesc rest arr defs
warnIfHole : Name -> NamedDef -> Core ()
warnIfHole n (MkNmError _)
= coreLift $ putStrLn $ "Warning: compiling hole " ++ show n
warnIfHole n _ = pure ()
getNamedDef : {auto c : Ref Ctxt Defs} ->
Name -> Core (Maybe (Name, FC, NamedDef))
getNamedDef n
@ -153,7 +158,8 @@ getNamedDef n
Nothing => pure Nothing
Just def => case namedcompexpr def of
Nothing => pure Nothing
Just d => pure (Just (n, location def, d))
Just d => do warnIfHole n d
pure (Just (n, location def, d))
replaceEntry : {auto c : Ref Ctxt Defs} ->
(Int, Maybe Binary) -> Core ()

2
src/Compiler/CompileExpr.idr
View File

@ -438,7 +438,7 @@ mutual
= toCExpTree n sc
toCExpTree' n (Case _ x scTy [])
= pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
toCExpTree' n (STerm tm) = toCExp n tm
toCExpTree' n (STerm _ tm) = toCExp n tm
toCExpTree' n (Unmatched msg)
= pure $ CCrash emptyFC msg
toCExpTree' n Impossible

198
src/Core/CaseBuilder.idr
View File

@ -188,22 +188,22 @@ take (x :: xs) (p :: ps) = p :: take xs ps
data PatClause : (vars : List Name) -> (todo : List Name) -> Type where
MkPatClause : List Name -> -- names matched so far (from original lhs)
NamedPats vars todo ->
(rhs : Term vars) -> PatClause vars todo
Int -> (rhs : Term vars) -> PatClause vars todo
getNPs : PatClause vars todo -> NamedPats vars todo
getNPs (MkPatClause _ lhs rhs) = lhs
getNPs (MkPatClause _ lhs pid rhs) = lhs
{vars : _} -> {todo : _} -> Show (PatClause vars todo) where
show (MkPatClause _ ps rhs)
show (MkPatClause _ ps pid rhs)
= show ps ++ " => " ++ show rhs
substInClause : {a, vars, todo : _} ->
{auto c : Ref Ctxt Defs} ->
FC -> PatClause vars (a :: todo) ->
Core (PatClause vars (a :: todo))
substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs)
substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs)
= do pats' <- substInPats fc a (mkTerm vars pat) pats
pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') rhs)
pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') pid rhs)
data Partitions : List (PatClause vars todo) -> Type where
ConClauses : {todo, vars, ps : _} ->
@ -244,7 +244,7 @@ clauseType : Phase -> PatClause vars (a :: as) -> ClauseType
-- and don't see later, treat it as a variable
-- Or, if we're compiling for runtime we won't be able to split on it, so
-- also treat it as a variable
clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) rhs)
clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs)
= getClauseType phase arg ty
where
-- used to get the remaining clause types
@ -324,25 +324,25 @@ data Group : List Name -> -- variables in scope
data GroupMatch : ConType -> List Pat -> Group vars todo -> Type where
ConMatch : LengthMatch ps newargs ->
GroupMatch (CName n tag) ps
(ConGroup {newargs} n tag (MkPatClause pvs pats rhs :: rest))
(ConGroup {newargs} n tag (MkPatClause pvs pats pid rhs :: rest))
DelayMatch : GroupMatch CDelay []
(DelayGroup {tyarg} {valarg} (MkPatClause pvs pats rhs :: rest))
(DelayGroup {tyarg} {valarg} (MkPatClause pvs pats pid rhs :: rest))
ConstMatch : GroupMatch (CConst c) []
(ConstGroup c (MkPatClause pvs pats rhs :: rest))
(ConstGroup c (MkPatClause pvs pats pid rhs :: rest))
NoMatch : GroupMatch ct ps g
checkGroupMatch : (c : ConType) -> (ps : List Pat) -> (g : Group vars todo) ->
GroupMatch c ps g
checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats rhs :: rest))
checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats pid rhs :: rest))
= case checkLengthMatch ps newargs of
Nothing => NoMatch
Just prf => case (nameEq x x', decEq tag tag') of
(Just Refl, Yes Refl) => ConMatch prf
_ => NoMatch
checkGroupMatch (CName x tag) ps _ = NoMatch
checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats rhs :: rest))
checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats pid rhs :: rest))
= DelayMatch
checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats rhs :: rest))
checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats pid rhs :: rest))
= case constantEq c c' of
Nothing => NoMatch
Just Refl => ConstMatch
@ -434,14 +434,14 @@ groupCons fc fn pvars cs
addConG : {vars', todo' : _} ->
Name -> (tag : Int) ->
List Pat -> NamedPats vars' todo' ->
(rhs : Term vars') ->
Int -> (rhs : Term vars') ->
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
-- Group all the clauses that begin with the same constructor, and
-- add new pattern arguments for each of that constructor's arguments.
-- The type of 'ConGroup' ensures that we refer to the arguments by
-- the same name in each of the clauses
addConG {vars'} {todo'} n tag pargs pats rhs []
addConG {vars'} {todo'} n tag pargs pats pid rhs []
= do cty <- the (Core (NF vars')) $ if n == UN "->"
then pure $ NBind fc (MN "_" 0) (Pi top Explicit (NType fc)) $
(\d, a => pure $ NBind fc (MN "_" 1) (Pi top Explicit (NErased fc False))
@ -458,11 +458,11 @@ groupCons fc fn pvars cs
let clause = MkPatClause {todo = patnames ++ todo'}
pvars
(newargs ++ pats')
(weakenNs patnames rhs)
pid (weakenNs patnames rhs)
pure [ConGroup n tag [clause]]
addConG {vars'} {todo'} n tag pargs pats rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)
addConG {vars'} {todo'} n tag pargs pats rhs
((ConGroup {newargs} n tag ((MkPatClause pvars ps tm) :: rest)) :: gs)
addConG {vars'} {todo'} n tag pargs pats pid rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)
addConG {vars'} {todo'} n tag pargs pats pid rhs
((ConGroup {newargs} n tag ((MkPatClause pvars ps tid tm) :: rest)) :: gs)
| (ConMatch {newargs} lprf)
= do let newps = newPats pargs lprf ps
let pats' = updatePatNames (updateNames (zip newargs pargs))
@ -470,13 +470,14 @@ groupCons fc fn pvars cs
let newclause : PatClause (newargs ++ vars') (newargs ++ todo')
= MkPatClause pvars
(newps ++ pats')
pid
(weakenNs newargs rhs)
-- put the new clause at the end of the group, since we
-- match the clauses top to bottom.
pure ((ConGroup n tag (MkPatClause pvars ps tm :: rest ++ [newclause]))
pure ((ConGroup n tag (MkPatClause pvars ps tid tm :: rest ++ [newclause]))
:: gs)
addConG n tag pargs pats rhs (g :: gs) | NoMatch
= do gs' <- addConG n tag pargs pats rhs gs
addConG n tag pargs pats pid rhs (g :: gs) | NoMatch
= do gs' <- addConG n tag pargs pats pid rhs gs
pure (g :: gs')
-- This rather ugly special case is to deal with laziness, where Delay
@ -485,10 +486,10 @@ groupCons fc fn pvars cs
-- and compiler)
addDelayG : {vars', todo' : _} ->
Pat -> Pat -> NamedPats vars' todo' ->
(rhs : Term vars') ->
Int -> (rhs : Term vars') ->
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
addDelayG {vars'} {todo'} pty parg pats rhs []
addDelayG {vars'} {todo'} pty parg pats pid rhs []
= do let dty = NBind fc (MN "a" 0) (Pi erased Explicit (NType fc)) $
(\d, a =>
do a' <- evalClosure d a
@ -502,11 +503,11 @@ groupCons fc fn pvars cs
(weakenNs [tyname, argname] pats)
let clause = MkPatClause {todo = tyname :: argname :: todo'}
pvars (newargs ++ pats')
(weakenNs [tyname, argname] rhs)
pid (weakenNs [tyname, argname] rhs)
pure [DelayGroup [clause]]
addDelayG {vars'} {todo'} pty parg pats rhs (g :: gs) with (checkGroupMatch CDelay [] g)
addDelayG {vars'} {todo'} pty parg pats rhs
((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tm) :: rest)) :: gs)
addDelayG {vars'} {todo'} pty parg pats pid rhs (g :: gs) with (checkGroupMatch CDelay [] g)
addDelayG {vars'} {todo'} pty parg pats pid rhs
((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tid tm) :: rest)) :: gs)
| (DelayMatch {tyarg} {valarg})
= do let newps = newPats [pty, parg] (ConsMatch (ConsMatch NilMatch)) ps
let pats' = updatePatNames (updateNames [(tyarg, pty),
@ -514,56 +515,56 @@ groupCons fc fn pvars cs
(weakenNs [tyarg, valarg] pats)
let newclause : PatClause (tyarg :: valarg :: vars')
(tyarg :: valarg :: todo')
= MkPatClause pvars (newps ++ pats')
= MkPatClause pvars (newps ++ pats') pid
(weakenNs [tyarg, valarg] rhs)
pure ((DelayGroup (MkPatClause pvars ps tm :: rest ++ [newclause]))
pure ((DelayGroup (MkPatClause pvars ps tid tm :: rest ++ [newclause]))
:: gs)
addDelayG pty parg pats rhs (g :: gs) | NoMatch
= do gs' <- addDelayG pty parg pats rhs gs
addDelayG pty parg pats pid rhs (g :: gs) | NoMatch
= do gs' <- addDelayG pty parg pats pid rhs gs
pure (g :: gs')
addConstG : {vars', todo' : _} ->
Constant -> NamedPats vars' todo' ->
(rhs : Term vars') ->
Int -> (rhs : Term vars') ->
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
addConstG c pats rhs []
= pure [ConstGroup c [MkPatClause pvars pats rhs]]
addConstG {todo'} {vars'} c pats rhs (g :: gs) with (checkGroupMatch (CConst c) [] g)
addConstG {todo'} {vars'} c pats rhs
((ConstGroup c ((MkPatClause pvars ps tm) :: rest)) :: gs) | ConstMatch
addConstG c pats pid rhs []
= pure [ConstGroup c [MkPatClause pvars pats pid rhs]]
addConstG {todo'} {vars'} c pats pid rhs (g :: gs) with (checkGroupMatch (CConst c) [] g)
addConstG {todo'} {vars'} c pats pid rhs
((ConstGroup c ((MkPatClause pvars ps tid tm) :: rest)) :: gs) | ConstMatch
= let newclause : PatClause vars' todo'
= MkPatClause pvars pats rhs in
= MkPatClause pvars pats pid rhs in
pure ((ConstGroup c
(MkPatClause pvars ps tm :: rest ++ [newclause])) :: gs)
addConstG c pats rhs (g :: gs) | NoMatch
= do gs' <- addConstG c pats rhs gs
(MkPatClause pvars ps tid tm :: rest ++ [newclause])) :: gs)
addConstG c pats pid rhs (g :: gs) | NoMatch
= do gs' <- addConstG c pats pid rhs gs
pure (g :: gs')
addGroup : {vars, todo, idx : _} ->
Pat -> (0 p : IsVar name idx vars) ->
NamedPats vars todo -> Term vars ->
NamedPats vars todo -> Int -> Term vars ->
List (Group vars todo) ->
Core (List (Group vars todo))
-- In 'As' replace the name on the RHS with a reference to the
-- variable we're doing the case split on
addGroup (PAs fc n p) pprf pats rhs acc
= addGroup p pprf pats (substName n (Local fc (Just True) _ pprf) rhs) acc
addGroup (PCon cfc n t a pargs) pprf pats rhs acc
addGroup (PAs fc n p) pprf pats pid rhs acc
= addGroup p pprf pats pid (substName n (Local fc (Just True) _ pprf) rhs) acc
addGroup (PCon cfc n t a pargs) pprf pats pid rhs acc
= if a == length pargs
then addConG n t pargs pats rhs acc
then addConG n t pargs pats pid rhs acc
else throw (CaseCompile cfc fn (NotFullyApplied n))
addGroup (PTyCon _ n a pargs) pprf pats rhs acc
= addConG n 0 pargs pats rhs acc
addGroup (PArrow _ _ s t) pprf pats rhs acc
= addConG (UN "->") 0 [s, t] pats rhs acc
addGroup (PTyCon _ n a pargs) pprf pats pid rhs acc
= addConG n 0 pargs pats pid rhs acc
addGroup (PArrow _ _ s t) pprf pats pid rhs acc
= addConG (UN "->") 0 [s, t] pats pid rhs acc
-- Go inside the delay; we'll flag the case as needing to force its
-- scrutinee (need to check in 'caseGroups below)
addGroup (PDelay _ _ pty parg) pprf pats rhs acc
= addDelayG pty parg pats rhs acc
addGroup (PConst _ c) pprf pats rhs acc
= addConstG c pats rhs acc
addGroup _ pprf pats rhs acc = pure acc -- Can't happen, not a constructor
addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc
= addDelayG pty parg pats pid rhs acc
addGroup (PConst _ c) pprf pats pid rhs acc
= addConstG c pats pid rhs acc
addGroup _ pprf pats pid rhs acc = pure acc -- Can't happen, not a constructor
-- -- FIXME: Is this possible to rule out with a type? Probably.
gc : {a, vars, todo : _} ->
@ -571,8 +572,8 @@ groupCons fc fn pvars cs
List (PatClause vars (a :: todo)) ->
Core (List (Group vars todo))
gc acc [] = pure acc
gc {a} acc ((MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs) :: cs)
= do acc' <- addGroup pat pprf pats rhs acc
gc {a} acc ((MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs) :: cs)
= do acc' <- addGroup pat pprf pats pid rhs acc
gc acc' cs
getFirstPat : NamedPats ns (p :: ps) -> Pat
@ -614,13 +615,10 @@ sameType {ns} fc phase fn env (p :: xs)
sameTypeAs : Phase -> NF ns -> List (ArgType ns) -> Core ()
sameTypeAs _ ty [] = pure ()
sameTypeAs ph ty (Known r t :: xs) =
if ph == RunTime && isErased r
-- Can't match on erased thing
then throw (CaseCompile fc fn (MatchErased (_ ** (env, mkTerm _ (firstPat p)))))
else do defs <- get Ctxt
if headEq ty !(nf defs env t) phase
then sameTypeAs ph ty xs
else throw (CaseCompile fc fn DifferingTypes)
do defs <- get Ctxt
if headEq ty !(nf defs env t) phase
then sameTypeAs ph ty xs
else throw (CaseCompile fc fn DifferingTypes)
sameTypeAs p ty _ = throw (CaseCompile fc fn DifferingTypes)
-- Check whether all the initial patterns are the same, or are all a variable.
@ -731,7 +729,8 @@ moveFirst el nps = getPat el nps :: dropPat el nps
shuffleVars : {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo ->
PatClause vars (name :: dropVar todo el)
shuffleVars el (MkPatClause pvars lhs rhs) = MkPatClause pvars (moveFirst el lhs) rhs
shuffleVars el (MkPatClause pvars lhs pid rhs)
= MkPatClause pvars (moveFirst el lhs) pid rhs
mutual
{- 'PatClause' contains a list of patterns still to process (that's the
@ -759,10 +758,10 @@ mutual
match {todo = []} fc fn phase [] err
= maybe (pure (Unmatched "No patterns"))
pure err
match {todo = []} fc fn phase ((MkPatClause pvars [] (Erased _ True)) :: _) err
match {todo = []} fc fn phase ((MkPatClause pvars [] pid (Erased _ True)) :: _) err
= pure Impossible
match {todo = []} fc fn phase ((MkPatClause pvars [] rhs) :: _) err
= pure $ STerm rhs
match {todo = []} fc fn phase ((MkPatClause pvars [] pid rhs) :: _) err
= pure $ STerm pid rhs
caseGroups : {pvar, vars, todo : _} ->
{auto i : Ref PName Int} ->
@ -804,7 +803,7 @@ mutual
-- the same variable (pprf) for the first argument. If not, the result
-- will be a broken case tree... so we should find a way to express this
-- in the type if we can.
conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs :: rest) err
conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs :: rest) err
= do refinedcs <- traverse (substInClause fc) cs
groups <- groupCons fc fn pvars refinedcs
ty <- case fty of
@ -825,21 +824,21 @@ mutual
where
updateVar : PatClause vars (a :: todo) -> Core (PatClause vars todo)
-- replace the name with the relevant variable on the rhs
updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) rhs)
updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) pid rhs)
= pure $ MkPatClause (n :: pvars)
!(substInPats fc a (Local pfc (Just False) _ prf) pats)
(substName n (Local pfc (Just False) _ prf) rhs)
pid (substName n (Local pfc (Just False) _ prf) rhs)
-- If it's an as pattern, replace the name with the relevant variable on
-- the rhs then continue with the inner pattern
updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) rhs)
updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) pid rhs)
= do pats' <- substInPats fc a (mkTerm _ pat) pats
let rhs' = substName n (Local pfc (Just True) _ prf) rhs
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') rhs')
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') pid rhs')
-- match anything, name won't appear in rhs but need to update
-- LHS pattern types based on what we've learned
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) rhs)
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) pid rhs)
= pure $ MkPatClause pvars
!(substInPats fc a (mkTerm vars pat) pats) rhs
!(substInPats fc a (mkTerm vars pat) pats) pid rhs
mixture : {a, vars, todo : _} ->
{auto i : Ref PName Int} ->
@ -860,17 +859,18 @@ mutual
mkPatClause : {auto c : Ref Ctxt Defs} ->
FC -> Name ->
(args : List Name) -> ClosedTerm -> (List Pat, ClosedTerm) ->
(args : List Name) -> ClosedTerm ->
Int -> (List Pat, ClosedTerm) ->
Core (PatClause args args)
mkPatClause fc fn args ty (ps, rhs)
mkPatClause fc fn args ty pid (ps, rhs)
= maybe (throw (CaseCompile fc fn DifferingArgNumbers))
(\eq =>
do defs <- get Ctxt
nty <- nf defs [] ty
ns <- mkNames args ps eq (Just nty)
pure (MkPatClause [] ns
(rewrite sym (appendNilRightNeutral args) in
(weakenNs args rhs))))
pure (MkPatClause [] ns pid
(rewrite sym (appendNilRightNeutral args) in
(weakenNs args rhs))))
(checkLengthMatch args ps)
where
mkNames : (vars : List Name) -> (ps : List Pat) ->
@ -906,7 +906,7 @@ patCompile fc fn phase ty [] def
def
patCompile fc fn phase ty (p :: ps) def
= do let ns = getNames 0 (fst p)
pats <- traverse (mkPatClause fc fn ns ty) (p :: ps)
pats <- mkPatClausesFrom 0 ns (p :: ps)
log 5 $ "Pattern clauses " ++ show pats
i <- newRef PName (the Int 0)
cases <- match fc fn phase pats
@ -914,6 +914,15 @@ patCompile fc fn phase ty (p :: ps) def
map (TT.weakenNs ns) def)
pure (_ ** cases)
where
mkPatClausesFrom : Int -> (args : List Name) ->
List (List Pat, ClosedTerm) ->
Core (List (PatClause args args))
mkPatClausesFrom i ns [] = pure []
mkPatClausesFrom i ns (p :: ps)
= do p' <- mkPatClause fc fn ns ty i p
ps' <- mkPatClausesFrom (i + 1) ns ps
pure (p' :: ps')
getNames : Int -> List Pat -> List Name
getNames i [] = []
getNames i (x :: xs) = MN "arg" i :: getNames (i + 1) xs
@ -950,16 +959,28 @@ simpleCase fc phase fn ty def clauses
defs <- get Ctxt
patCompile fc fn phase ty ps def
findReached : CaseTree ns -> List Int
findReached (Case _ _ _ alts) = concatMap findRAlts alts
where
findRAlts : CaseAlt ns' -> List Int
findRAlts (ConCase _ _ _ t) = findReached t
findRAlts (DelayCase _ _ t) = findReached t
findRAlts (ConstCase _ t) = findReached t
findRAlts (DefaultCase t) = findReached t
findReached (STerm i _) = [i]
findReached _ = []
-- Returns the case tree, and a list of the clauses that aren't reachable
export
getPMDef : {auto c : Ref Ctxt Defs} ->
FC -> Phase -> Name -> ClosedTerm -> List Clause ->
Core (args ** CaseTree args)
Core (args ** (CaseTree args, List Clause))
-- If there's no clauses, make a definition with the right number of arguments
-- for the type, which we can use in coverage checking to ensure that one of
-- the arguments has an empty type
getPMDef fc phase fn ty []
= do defs <- get Ctxt
pure (!(getArgs 0 !(nf defs [] ty)) ** Unmatched "No clauses")
pure (!(getArgs 0 !(nf defs [] ty)) ** (Unmatched "No clauses", []))
where
getArgs : Int -> NF [] -> Core (List Name)
getArgs i (NBind fc x (Pi _ _ _) sc)
@ -970,8 +991,17 @@ getPMDef fc phase fn ty []
getPMDef fc phase fn ty clauses
= do defs <- get Ctxt
let cs = map (toClosed defs) (labelPat 0 clauses)
simpleCase fc phase fn ty Nothing cs
(_ ** t) <- simpleCase fc phase fn ty Nothing cs
let reached = findReached t
pure (_ ** (t, getUnreachable 0 reached clauses))
where
getUnreachable : Int -> List Int -> List Clause -> List Clause
getUnreachable i is [] = []
getUnreachable i is (c :: cs)
= if i `elem` is
then getUnreachable (i + 1) is cs
else c :: getUnreachable (i + 1) is cs
labelPat : Int -> List a -> List (String, a)
labelPat i [] = []
labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs

14
src/Core/CaseTree.idr
View File

@ -20,7 +20,9 @@ mutual
(scTy : Term vars) -> List (CaseAlt vars) ->
CaseTree vars
||| RHS: no need for further inspection
STerm : Term vars -> CaseTree vars
||| The Int is a clause id that allows us to see which of the
||| initial clauses are reached in the tree
STerm : Int -> Term vars -> CaseTree vars
||| error from a partial match
Unmatched : (msg : String) -> CaseTree vars
||| Absurd context
@ -60,7 +62,7 @@ mutual
show (Case {name} idx prf ty alts)
= "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++
showSep " | " (assert_total (map show alts)) ++ " }"
show (STerm tm) = show tm
show (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
show (Unmatched msg) = "Error: " ++ show msg
show Impossible = "Impossible"
@ -83,7 +85,7 @@ mutual
= i == i
&& length alts == length alts
&& allTrue (zipWith eqAlt alts alts')
eqTree (STerm t) (STerm t') = eqTerm t t'
eqTree (STerm _ t) (STerm _ t') = eqTerm t t'
eqTree (Unmatched _) (Unmatched _) = True
eqTree Impossible Impossible = True
eqTree _ _ = False
@ -118,7 +120,7 @@ mutual
= let MkNVar prf' = insertNVarNames {outer} {inner} {ns} _ prf in
Case _ prf' (insertNames {outer} ns scTy)
(map (insertCaseAltNames {outer} {inner} ns) alts)
insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x)
insertCaseNames {outer} ns (STerm i x) = STerm i (insertNames {outer} ns x)
insertCaseNames ns (Unmatched msg) = Unmatched msg
insertCaseNames ns Impossible = Impossible
@ -146,7 +148,7 @@ thinTree : {outer, inner : _} ->
thinTree n (Case idx prf scTy alts)
= let MkNVar prf' = insertNVar {n} _ prf in
Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
thinTree n (STerm tm) = STerm (thin n tm)
thinTree n (STerm i tm) = STerm i (thin n tm)
thinTree n (Unmatched msg) = Unmatched msg
thinTree n Impossible = Impossible
@ -172,7 +174,7 @@ getNames add ns sc = getSet ns sc
getSet : NameMap Bool -> CaseTree vs -> NameMap Bool
getSet ns (Case _ x ty xs) = getAltSets ns xs
getSet ns (STerm tm) = add ns tm
getSet ns (STerm i tm) = add ns tm
getSet ns (Unmatched msg) = ns
getSet ns Impossible = ns

19
src/Core/Context.idr
View File

@ -617,14 +617,14 @@ mutual
HasNames (CaseTree vars) where
full gam (Case i v ty alts)
= pure $ Case i v !(full gam ty) !(traverse (full gam) alts)
full gam (STerm tm)
= pure $ STerm !(full gam tm)
full gam (STerm i tm)
= pure $ STerm i !(full gam tm)
full gam t = pure t
resolved gam (Case i v ty alts)
= pure $ Case i v !(resolved gam ty) !(traverse (resolved gam) alts)
resolved gam (STerm tm)
= pure $ STerm !(resolved gam tm)
resolved gam (STerm i tm)
= pure $ STerm i !(resolved gam tm)
resolved gam t = pure t
export
@ -859,6 +859,8 @@ record Defs where
-- again
timings : StringMap (Bool, Integer)
-- ^ record of timings from logTimeRecord
warnings : List Warning
-- ^ as yet unreported warnings
-- Label for context references
export
@ -876,7 +878,7 @@ initDefs
= do gam <- initCtxt
pure (MkDefs gam [] ["Main"] [] defaults empty 100
empty empty empty [] [] empty []
empty 5381 [] [] [] [] [] empty empty empty empty)
empty 5381 [] [] [] [] [] empty empty empty empty [])
-- Reset the context, except for the options
export
@ -2178,6 +2180,13 @@ setSession sopts
= do defs <- get Ctxt
put Ctxt (record { options->session = sopts } defs)
export
recordWarning : {auto c : Ref Ctxt Defs} ->
Warning -> Core ()
recordWarning w
= do defs <- get Ctxt
put Ctxt (record { warnings $= (w ::) } defs)
-- Log message with a term, translating back to human readable names first
export
logTerm : {vars : _} ->

12
src/Core/Core.idr
View File

@ -119,7 +119,8 @@ data Error : Type where
GenericMsg : FC -> String -> Error
TTCError : TTCErrorMsg -> Error
FileErr : String -> FileError -> Error
ParseFail : FC -> ParseError -> Error
ParseFail : Show token =>
FC -> ParseError token -> Error
ModuleNotFound : FC -> List String -> Error
CyclicImports : List (List String) -> Error
ForceNeeded : Error
@ -130,6 +131,11 @@ data Error : Type where
InLHS : FC -> Name -> Error -> Error
InRHS : FC -> Name -> Error -> Error
public export
data Warning : Type where
UnreachableClause : {vars : _} ->
FC -> Env Term vars -> Term vars -> Warning
export
Show TTCErrorMsg where
show (Format file ver exp) =
@ -361,6 +367,10 @@ getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
getErrorLoc (InRHS _ _ err) = getErrorLoc err
export
getWarningLoc : Warning -> Maybe FC
getWarningLoc (UnreachableClause fc _ _) = Just fc
-- Core is a wrapper around IO that is specialised for efficiency.
export
record Core t where

4
src/Core/Coverage.idr
View File

@ -168,7 +168,7 @@ emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
emptyRHS fc (STerm s) = STerm (Erased fc False)
emptyRHS fc (STerm i s) = STerm i (Erased fc False)
emptyRHS fc sc = sc
mkAlt : {vars : _} ->
@ -357,7 +357,7 @@ buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
buildArgsAlt not' (c :: cs)
= pure $ !(buildArgAlt not' c) ++ !(buildArgsAlt not' cs)
buildArgs fc defs known not ps (STerm vs)
buildArgs fc defs known not ps (STerm _ vs)
= pure [] -- matched, so return nothing
buildArgs fc defs known not ps (Unmatched msg)
= pure [ps] -- unmatched, so return it

2
src/Core/Hash.idr
View File

@ -152,7 +152,7 @@ mutual
Hashable (CaseTree vars) where
hashWithSalt h (Case idx x scTy xs)
= h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs
hashWithSalt h (STerm x)
hashWithSalt h (STerm _ x)
= h `hashWithSalt` 1 `hashWithSalt` x
hashWithSalt h (Unmatched msg)
= h `hashWithSalt` 2

7
src/Core/LinearCheck.idr
View File

@ -222,8 +222,9 @@ mutual
rig
logC 10 $ do
def <- the (Core String) $ case definition gdef of
PMDef _ _ (STerm tm) _ _ => do tm' <- toFullNames tm
pure (show tm')
PMDef _ _ (STerm _ tm) _ _ =>
do tm' <- toFullNames tm
pure (show tm')
_ => pure ""
pure (show rig ++ ": " ++ show n ++ " " ++ show fc ++ "\n"
++ show def)
@ -614,7 +615,7 @@ mutual
RigCount -> (erase : Bool) -> Env Term vars ->
Name -> Int -> Def -> List (Term vars) ->
Core (Term vars, Glued vars, Usage vars)
expandMeta rig erase env n idx (PMDef _ [] (STerm fn) _ _) args
expandMeta rig erase env n idx (PMDef _ [] (STerm _ fn) _ _) args
= do tm <- substMeta (embed fn) args []
lcheck rig erase env tm
where

2
src/Core/Normalise.idr
View File

@ -326,7 +326,7 @@ parameters (defs : Defs, topopts : EvalOpts)
= do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
let loc' = updateLocal idx (varExtend x) loc xval
findAlt env loc' opts fc stk xval alts def
evalTree env loc opts fc stk (STerm tm) def
evalTree env loc opts fc stk (STerm _ tm) def
= case fuel opts of
Nothing => evalWithOpts defs opts env loc (embed tm) stk
Just Z => def

4
src/Core/TTC.idr
View File

@ -343,7 +343,7 @@ mutual
{vars : _} -> TTC (CaseTree vars) where
toBuf b (Case {name} idx x scTy xs)
= do tag 0; toBuf b name; toBuf b idx; toBuf b xs
toBuf b (STerm x)
toBuf b (STerm _ x)
= do tag 1; toBuf b x
toBuf b (Unmatched msg)
= do tag 2; toBuf b msg
@ -355,7 +355,7 @@ mutual
xs <- fromBuf b
pure (Case {name} idx (mkPrf idx) (Erased emptyFC False) xs)
1 => do x <- fromBuf b
pure (STerm x)
pure (STerm 0 x)
2 => do msg <- fromBuf b
pure (Unmatched msg)
3 => pure Impossible

14
src/Core/Unify.idr
View File

@ -202,7 +202,7 @@ chaseMetas (n :: ns) all
= case lookup n all of
Just _ => chaseMetas ns all
_ => do defs <- get Ctxt
Just (PMDef _ _ (STerm soln) _ _) <-
Just (PMDef _ _ (STerm _ soln) _ _) <-
lookupDefExact n (gamma defs)
| _ => chaseMetas ns (insert n () all)
let sns = keys (getMetas soln)
@ -472,7 +472,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
logTerm 5 "Definition" rhs
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
let newdef = record { definition =
PMDef simpleDef [] (STerm rhs) (STerm rhs) []
PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) []
} mdef
addDef (Resolved mref) newdef
removeHole mref
@ -1359,7 +1359,7 @@ retryGuess mode smode (hid, (loc, hname))
handleUnify
(do tm <- search loc rig (smode == Defaults) depth defining
(type def) []
let gdef = record { definition = PMDef defaultPI [] (STerm tm) (STerm tm) [] } def
let gdef = record { definition = PMDef defaultPI [] (STerm 0 tm) (STerm 0 tm) [] } def
logTermNF 5 ("Solved " ++ show hname) [] tm
addDef (Resolved hid) gdef
removeGuess hid
@ -1390,7 +1390,7 @@ retryGuess mode smode (hid, (loc, hname))
logTerm 5 "Retry Delay" tm
pure $ delayMeta r envb !(getTerm ty) tm
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] (STerm tm') (STerm tm') [] } def
[] (STerm 0 tm') (STerm 0 tm') [] } def
logTerm 5 ("Resolved " ++ show hname) tm'
addDef (Resolved hid) gdef
removeGuess hid
@ -1416,7 +1416,7 @@ retryGuess mode smode (hid, (loc, hname))
-- proper definition and remove it from the
-- hole list
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] (STerm tm) (STerm tm) [] } def
[] (STerm 0 tm) (STerm 0 tm) [] } def
logTerm 5 ("Resolved " ++ show hname) tm
addDef (Resolved hid) gdef
removeGuess hid
@ -1479,7 +1479,7 @@ checkArgsSame : {auto u : Ref UST UState} ->
checkArgsSame [] = pure False
checkArgsSame (x :: xs)
= do defs <- get Ctxt
Just (PMDef _ [] (STerm def) _ _) <-
Just (PMDef _ [] (STerm 0 def) _ _) <-
lookupDefExact (Resolved x) (gamma defs)
| _ => checkArgsSame xs
s <- anySame def xs
@ -1491,7 +1491,7 @@ checkArgsSame (x :: xs)
anySame tm [] = pure False
anySame tm (t :: ts)
= do defs <- get Ctxt
Just (PMDef _ [] (STerm def) _ _) <-
Just (PMDef _ [] (STerm 0 def) _ _) <-
lookupDefExact (Resolved t) (gamma defs)
| _ => anySame tm ts
if !(convert defs [] tm def)

15
src/Idris/Error.idr
View File

@ -258,6 +258,13 @@ perror (InRHS fc n err)
= pure $ "While processing right hand side of " ++ !(prettyName n) ++
" at " ++ show fc ++ ":\n" ++ !(perror err)
export
pwarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Warning -> Core String
pwarning (UnreachableClause fc env tm)
= pure $ "Warning: unreachable clause: " ++ !(pshow env tm)
export
display : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -265,3 +272,11 @@ display : {auto c : Ref Ctxt Defs} ->
display err
= pure $ maybe "" (\f => show f ++ ":") (getErrorLoc err) ++
!(perror err)
export
displayWarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Warning -> Core String
displayWarning w
= pure $ maybe "" (\f => show f ++ ":") (getWarningLoc w) ++
!(pwarning w)

28
src/Idris/IDEMode/Parser.idr
View File

@ -5,31 +5,30 @@ module Idris.IDEMode.Parser
import Idris.IDEMode.Commands
import Text.Parser
import Data.List
import Data.Strings
import Parser.Lexer.Source
import Parser.Source
import Text.Lexer
import Text.Parser
import Utils.Either
import Utils.String
import Data.List
import Data.Strings
%hide Text.Lexer.symbols
%hide Parser.Lexer.Source.symbols
symbols : List String
symbols = ["(", ":", ")"]
ideTokens : TokenMap SourceToken
ideTokens : TokenMap Token
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(identAllowDashes, \x => NSIdent [x]),
[(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(identAllowDashes, \x => Ident x),
(space, Comment)]
idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
idelex : String -> Either (Int, Int, String) (List (TokenData Token))
idelex str
= case lex ideTokens str of
-- Add the EndInput token so that we'll have a line and column
@ -38,12 +37,12 @@ idelex str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData SourceToken -> Bool
notComment : TokenData Token -> Bool
notComment t = case tok t of
Comment _ => False
_ => True
sexp : SourceRule SExp
sexp : Rule SExp
sexp
= do symbol ":"; exactIdent "True"
pure (BoolAtom True)
@ -60,15 +59,14 @@ sexp
symbol ")"
pure (SExpList xs)
ideParser : {e : _} ->
String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
ideParser : {e : _} -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
ideParser str p
= do toks <- mapError LexFail $ idelex str
parsed <- mapError mapParseError $ parse p toks
parsed <- mapError toGenericParsingError $ parse p toks
Right (fst parsed)
export
parseSExp : String -> Either ParseError SExp
parseSExp : String -> Either (ParseError Token) SExp
parseSExp inp
= ideParser inp (do c <- sexp; eoi; pure c)

7
src/Idris/ModTree.idr
View File

@ -184,11 +184,14 @@ buildMod loc num len mod
": Building " ++ showMod ++
" (" ++ src ++ ")"
[] <- process {u} {m} msg src
| errs => do traverse emitError errs
| errs => do emitWarnings
traverse emitError errs
pure (ferrs ++ errs)
emitWarnings
traverse_ emitError ferrs
pure ferrs
else do traverse_ emitError ferrs
else do emitWarnings
traverse_ emitError ferrs
pure ferrs
where
getEithers : List (Either a b) -> (List a, List b)

77
src/Idris/Package.idr
View File

@ -15,6 +15,12 @@ import Data.Strings
import Data.StringTrie
import Data.These
import Parser.Package
import System
import Text.Parser
import Utils.Binary
import Utils.String
import Idris.CommandLine
import Idris.ModTree
import Idris.ProcessIdr
@ -23,13 +29,6 @@ import Idris.REPLOpts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import Parser.Lexer.Source
import Parser.Source
import Utils.Binary
import System
import Text.Parser
import IdrisPaths
%default covering
@ -114,7 +113,7 @@ data DescField : Type where
PPreclean : FC -> String -> DescField
PPostclean : FC -> String -> DescField
field : String -> SourceRule DescField
field : String -> Rule DescField
field fname
= strField PVersion "version"
<|> strField PAuthors "authors"
@ -134,43 +133,41 @@ field fname
<|> strField PPostinstall "postinstall"
<|> strField PPreclean "preclean"
<|> strField PPostclean "postclean"
<|> do exactIdent "depends"; symbol "="
ds <- sepBy1 (symbol ",") unqualifiedName
<|> do exactProperty "depends"
equals
ds <- sep packageName
pure (PDepends ds)
<|> do exactIdent "modules"; symbol "="
ms <- sepBy1 (symbol ",")
(do start <- location
ns <- nsIdent
end <- location
Parser.Core.pure (MkFC fname start end, ns))
Parser.Core.pure (PModules ms)
<|> do exactIdent "main"; symbol "="
<|> do exactProperty "modules"
equals
ms <- sep (do start <- location
m <- moduleIdent
end <- location
pure (MkFC fname start end, m))
pure (PModules ms)
<|> do exactProperty "main"
equals
start <- location
m <- nsIdent
m <- namespacedIdent
end <- location
Parser.Core.pure (PMainMod (MkFC fname start end) m)
<|> do exactIdent "executable"; symbol "="
e <- unqualifiedName
Parser.Core.pure (PExec e)
pure (PMainMod (MkFC fname start end) m)
<|> do exactProperty "executable"
equals
e <- (stringLit <|> packageName)
pure (PExec e)
where
getStr : (FC -> String -> DescField) -> FC ->
String -> Constant -> SourceEmptyRule DescField
getStr p fc fld (Str s) = pure (p fc s)
getStr p fc fld _ = fail $ fld ++ " field must be a string"
strField : (FC -> String -> DescField) -> String -> SourceRule DescField
strField p f
strField : (FC -> String -> DescField) -> String -> Rule DescField
strField fieldConstructor fieldName
= do start <- location
exactIdent f
symbol "="
c <- constant
exactProperty fieldName
equals
str <- stringLit
end <- location
getStr p (MkFC fname start end) f c
pure $ fieldConstructor (MkFC fname start end) str
parsePkgDesc : String -> SourceRule (String, List DescField)
parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
= do exactIdent "package"
name <- unqualifiedName
= do exactProperty "package"
name <- packageName
fields <- many (field fname)
pure (name, fields)
@ -425,6 +422,12 @@ clean pkg
delete $ ttFile ++ ".ttc"
delete $ ttFile ++ ".ttm"
getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
getParseErrorLoc fname (LitFail _) = MkFC fname (0, 0) (0, 0) -- TODO: Remove this unused case
getParseErrorLoc fname _ = replFC
-- Just load the 'Main' module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->

216
src/Idris/Parser.idr
View File

@ -14,7 +14,7 @@ import Data.Strings
%default covering
-- Forward declare since they're used in the parser
topDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
topDecl : FileName -> IndentInfo -> Rule (List PDecl)
collectDefs : List PDecl -> List PDecl
-- Some context for the parser
@ -46,7 +46,7 @@ plhs = MkParseOpts False False
%hide Prelude.pure
%hide Core.Core.pure
atom : FileName -> SourceRule PTerm
atom : FileName -> Rule PTerm
atom fname
= do start <- location
x <- constant
@ -85,30 +85,30 @@ atom fname
end <- location
pure (PRef (MkFC fname start end) x)
whereBlock : FileName -> Int -> SourceRule (List PDecl)
whereBlock : FileName -> Int -> Rule (List PDecl)
whereBlock fname col
= do keyword "where"
ds <- blockAfter col (topDecl fname)
pure (collectDefs (concat ds))
-- Expect a keyword, but if we get anything else it's a fatal error
commitKeyword : IndentInfo -> String -> SourceRule ()
commitKeyword : IndentInfo -> String -> Rule ()
commitKeyword indents req
= do mustContinue indents (Just req)
keyword req
mustContinue indents Nothing
commitSymbol : String -> SourceRule ()
commitSymbol : String -> Rule ()
commitSymbol req
= symbol req
<|> fatalError ("Expected '" ++ req ++ "'")
continueWith : IndentInfo -> String -> SourceRule ()
continueWith : IndentInfo -> String -> Rule ()
continueWith indents req
= do mustContinue indents (Just req)
symbol req
iOperator : SourceRule Name
iOperator : Rule Name
iOperator
= operator
<|> do symbol "`"
@ -122,7 +122,7 @@ data ArgType
| WithArg PTerm
mutual
appExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
appExpr q fname indents
= case_ fname indents
<|> lambdaCase fname indents
@ -153,7 +153,7 @@ mutual
applyExpImp start end f (WithArg exp :: args)
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
argExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule ArgType
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType
argExpr q fname indents
= do continue indents
arg <- simpleExpr fname indents
@ -170,7 +170,7 @@ mutual
pure (WithArg arg)
else fail "| not allowed here"
implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, PTerm)
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm)
implicitArg fname indents
= do start <- location
symbol "{"
@ -189,7 +189,7 @@ mutual
symbol "}"
pure (Nothing, tm)
with_ : FileName -> IndentInfo -> SourceRule PTerm
with_ : FileName -> IndentInfo -> Rule PTerm
with_ fname indents
= do start <- location
keyword "with"
@ -199,12 +199,12 @@ mutual
rhs <- expr pdef fname indents
pure (PWithUnambigNames (MkFC fname start end) ns rhs)
where
singleName : SourceRule (List Name)
singleName : Rule (List Name)
singleName = do
n <- name
pure [n]
nameList : SourceRule (List Name)
nameList : Rule (List Name)
nameList = do
symbol "["
commit
@ -212,7 +212,7 @@ mutual
symbol "]"
pure ns
opExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
opExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
opExpr q fname indents
= do start <- location
l <- appExpr q fname indents
@ -232,7 +232,7 @@ mutual
pure (POp (MkFC fname start end) op l r))
<|> pure l
dpair : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
dpair : FileName -> FilePos -> IndentInfo -> Rule PTerm
dpair fname start indents
= do x <- unqualifiedName
symbol ":"
@ -255,7 +255,7 @@ mutual
(PImplicit (MkFC fname start end))
rest)
bracketedExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
bracketedExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
bracketedExpr fname start indents
-- left section. This may also be a prefix operator, but we'll sort
-- that out when desugaring: if the operator is infix, treat it as a
@ -287,7 +287,7 @@ mutual
getInitRange [x, y] = pure (x, Just y)
getInitRange _ = fatalError "Invalid list range syntax"
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> SourceRule PTerm
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> Rule PTerm
listRange fname start indents xs
= do symbol "]"
end <- location
@ -301,7 +301,7 @@ mutual
rstate <- getInitRange xs
pure (PRange fc (fst rstate) (snd rstate) y)
listExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
listExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
listExpr fname start indents
= do ret <- expr pnowith fname indents
symbol "|"
@ -317,7 +317,7 @@ mutual
pure (PList (MkFC fname start end) xs))
-- A pair, dependent pair, or just a single expression
tuple : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PTerm
tuple : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PTerm
tuple fname start indents e
= do rest <- some (do symbol ","
estart <- location
@ -337,7 +337,7 @@ mutual
mergePairs end ((estart, exp) :: rest)
= PPair (MkFC fname estart end) exp (mergePairs end rest)
simpleExpr : FileName -> IndentInfo -> SourceRule PTerm
simpleExpr : FileName -> IndentInfo -> Rule PTerm
simpleExpr fname indents
= do
start <- location
@ -353,7 +353,7 @@ mutual
[] => root
fs => PRecordFieldAccess (MkFC fname start end) root recFields
simplerExpr : FileName -> IndentInfo -> SourceRule PTerm
simplerExpr : FileName -> IndentInfo -> Rule PTerm
simplerExpr fname indents
= do start <- location
x <- unqualifiedName
@ -429,7 +429,7 @@ mutual
= PPi fc rig p n ty (pibindAll fc p rest scope)
bindList : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, PTerm, PTerm))
Rule (List (RigCount, PTerm, PTerm))
bindList fname start indents
= sepBy1 (symbol ",")
(do rigc <- multiplicity
@ -442,7 +442,7 @@ mutual
pure (rig, pat, ty))
pibindListName : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Name, PTerm))
Rule (List (RigCount, Name, PTerm))
pibindListName fname start indents
= do rigc <- multiplicity
ns <- sepBy1 (symbol ",") unqualifiedName
@ -460,12 +460,12 @@ mutual
pure (rig, n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Maybe Name, PTerm))
Rule (List (RigCount, Maybe Name, PTerm))
pibindList fname start indents
= do params <- pibindListName fname start indents
pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
bindSymbol : SourceRule (PiInfo PTerm)
bindSymbol : Rule (PiInfo PTerm)
bindSymbol
= do symbol "->"
pure Explicit
@ -473,7 +473,7 @@ mutual
pure AutoImplicit
explicitPi : FileName -> IndentInfo -> SourceRule PTerm
explicitPi : FileName -> IndentInfo -> Rule PTerm
explicitPi fname indents
= do start <- location
symbol "("
@ -484,7 +484,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) exp binders scope)
autoImplicitPi : FileName -> IndentInfo -> SourceRule PTerm
autoImplicitPi : FileName -> IndentInfo -> Rule PTerm
autoImplicitPi fname indents
= do start <- location
symbol "{"
@ -497,7 +497,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
defaultImplicitPi : FileName -> IndentInfo -> SourceRule PTerm
defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm
defaultImplicitPi fname indents
= do start <- location
symbol "{"
@ -511,7 +511,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope)
forall_ : FileName -> IndentInfo -> SourceRule PTerm
forall_ : FileName -> IndentInfo -> Rule PTerm
forall_ fname indents
= do start <- location
keyword "forall"
@ -527,7 +527,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> SourceRule PTerm
implicitPi : FileName -> IndentInfo -> Rule PTerm
implicitPi fname indents
= do start <- location
symbol "{"
@ -538,7 +538,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
lam : FileName -> IndentInfo -> SourceRule PTerm
lam : FileName -> IndentInfo -> Rule PTerm
lam fname indents
= do start <- location
symbol "\\"
@ -555,7 +555,7 @@ mutual
= PLam fc rig Explicit pat ty (bindAll fc rest scope)
letBinder : FileName -> IndentInfo ->
SourceRule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
letBinder fname indents
= do start <- location
rigc <- multiplicity
@ -594,7 +594,7 @@ mutual
= let fc = MkFC fname start end in
DoLetPat fc pat ty val alts :: buildDoLets fname rest
let_ : FileName -> IndentInfo -> SourceRule PTerm
let_ : FileName -> IndentInfo -> Rule PTerm
let_ fname indents
= do start <- location
keyword "let"
@ -613,7 +613,7 @@ mutual
end <- location
pure (PLocal (MkFC fname start end) (collectDefs (concat ds)) scope)
case_ : FileName -> IndentInfo -> SourceRule PTerm
case_ : FileName -> IndentInfo -> Rule PTerm
case_ fname indents
= do start <- location
keyword "case"
@ -623,7 +623,7 @@ mutual
end <- location
pure (PCase (MkFC fname start end) scr alts)
lambdaCase : FileName -> IndentInfo -> SourceRule PTerm
lambdaCase : FileName -> IndentInfo -> Rule PTerm
lambdaCase fname indents
= do start <- location
symbol "\\" *> keyword "case"
@ -638,13 +638,13 @@ mutual
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
PCase fc (PRef fcCase n) alts)
caseAlt : FileName -> IndentInfo -> SourceRule PClause
caseAlt : FileName -> IndentInfo -> Rule PClause
caseAlt fname indents
= do start <- location
lhs <- opExpr plhs fname indents
caseRHS fname start indents lhs
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PClause
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PClause
caseRHS fname start indents lhs
= do symbol "=>"
mustContinue indents Nothing
@ -657,7 +657,7 @@ mutual
end <- location
pure (MkImpossible (MkFC fname start end) lhs)
if_ : FileName -> IndentInfo -> SourceRule PTerm
if_ : FileName -> IndentInfo -> Rule PTerm
if_ fname indents
= do start <- location
keyword "if"
@ -670,7 +670,7 @@ mutual
end <- location
pure (PIfThenElse (MkFC fname start end) x t e)
record_ : FileName -> IndentInfo -> SourceRule PTerm
record_ : FileName -> IndentInfo -> Rule PTerm
record_ fname indents
= do start <- location
keyword "record"
@ -681,7 +681,7 @@ mutual
end <- location
pure (PUpdate (MkFC fname start end) fs)
field : FileName -> IndentInfo -> SourceRule PFieldUpdate
field : FileName -> IndentInfo -> Rule PFieldUpdate
field fname indents
= do path <- map fieldName <$> [| name :: many recFieldCompat |]
upd <- (do symbol "="; pure PSetField)
@ -697,10 +697,10 @@ mutual
-- this allows the dotted syntax .field
-- but also the arrowed syntax ->field for compatibility with Idris 1
recFieldCompat : SourceRule Name
recFieldCompat : Rule Name
recFieldCompat = recField <|> (symbol "->" *> name)
rewrite_ : FileName -> IndentInfo -> SourceRule PTerm
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ fname indents
= do start <- location
keyword "rewrite"
@ -710,7 +710,7 @@ mutual
end <- location
pure (PRewrite (MkFC fname start end) rule tm)
doBlock : FileName -> IndentInfo -> SourceRule PTerm
doBlock : FileName -> IndentInfo -> Rule PTerm
doBlock fname indents
= do start <- location
keyword "do"
@ -728,7 +728,7 @@ mutual
else fail "Not a pattern variable"
validPatternVar _ = fail "Not a pattern variable"
doAct : FileName -> IndentInfo -> SourceRule (List PDo)
doAct : FileName -> IndentInfo -> Rule (List PDo)
doAct fname indents
= do start <- location
n <- name
@ -768,12 +768,12 @@ mutual
end <- location
pure [DoBindPat (MkFC fname start end) e val alts])
patAlt : FileName -> IndentInfo -> SourceRule PClause
patAlt : FileName -> IndentInfo -> Rule PClause
patAlt fname indents
= do symbol "|"
caseAlt fname indents
lazy : FileName -> IndentInfo -> SourceRule PTerm
lazy : FileName -> IndentInfo -> Rule PTerm
lazy fname indents
= do start <- location
exactIdent "Lazy"
@ -796,7 +796,7 @@ mutual
end <- location
pure (PForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> SourceRule PTerm
binder : FileName -> IndentInfo -> Rule PTerm
binder fname indents
= let_ fname indents
<|> autoImplicitPi fname indents
@ -806,7 +806,7 @@ mutual
<|> explicitPi fname indents
<|> lam fname indents
typeExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
typeExpr q fname indents
= do start <- location
arg <- opExpr q fname indents
@ -825,10 +825,10 @@ mutual
(mkPi start end a as)
export
expr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
expr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
expr = typeExpr
visOption : SourceRule Visibility
visOption : Rule Visibility
visOption
= do keyword "public"
keyword "export"
@ -843,7 +843,7 @@ visibility
= visOption
<|> pure Private
tyDecl : FileName -> IndentInfo -> SourceRule PTypeDecl
tyDecl : FileName -> IndentInfo -> Rule PTypeDecl
tyDecl fname indents
= do start <- location
n <- name
@ -857,7 +857,7 @@ tyDecl fname indents
mutual
parseRHS : (withArgs : Nat) ->
FileName -> FilePos -> Int ->
IndentInfo -> (lhs : PTerm) -> SourceRule PClause
IndentInfo -> (lhs : PTerm) -> Rule PClause
parseRHS withArgs fname start col indents lhs
= do symbol "="
mustWork $
@ -882,7 +882,7 @@ mutual
ifThenElse True t e = t
ifThenElse False t e = e
clause : Nat -> FileName -> IndentInfo -> SourceRule PClause
clause : Nat -> FileName -> IndentInfo -> Rule PClause
clause withArgs fname indents
= do start <- location
col <- column
@ -898,7 +898,7 @@ mutual
applyArgs f [] = f
applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args
parseWithArg : SourceRule (FC, PTerm)
parseWithArg : Rule (FC, PTerm)
parseWithArg
= do symbol "|"
start <- location
@ -927,7 +927,7 @@ mkDataConType fc ret (WithArg a :: xs)
= PImplicit fc -- This can't happen because we parse constructors without
-- withOK set
simpleCon : FileName -> PTerm -> IndentInfo -> SourceRule PTypeDecl
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon fname ret indents
= do start <- location
cname <- name
@ -937,7 +937,7 @@ simpleCon fname ret indents
pure (let cfc = MkFC fname start end in
MkPTy cfc cname (mkDataConType cfc ret params))
simpleData : FileName -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl
simpleData : FileName -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
simpleData fname start n indents
= do params <- many name
tyend <- location
@ -951,7 +951,7 @@ simpleData fname start n indents
pure (MkPData (MkFC fname start end) n
(mkTyConType tyfc params) [] cons)
dataOpt : SourceRule DataOpt
dataOpt : Rule DataOpt
dataOpt
= do exactIdent "noHints"
pure NoHints
@ -980,14 +980,14 @@ dataBody fname mincol start n indents ty
end <- location
pure (MkPData (MkFC fname start end) n ty opts cs)
gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl
gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
gadtData fname mincol start n indents
= do symbol ":"
commit
ty <- expr pdef fname indents
dataBody fname mincol start n indents ty
dataDeclBody : FileName -> IndentInfo -> SourceRule PDataDecl
dataDeclBody : FileName -> IndentInfo -> Rule PDataDecl
dataDeclBody fname indents
= do start <- location
col <- column
@ -996,7 +996,7 @@ dataDeclBody fname indents
simpleData fname start n indents
<|> gadtData fname col start n indents
dataDecl : FileName -> IndentInfo -> SourceRule PDecl
dataDecl : FileName -> IndentInfo -> Rule PDecl
dataDecl fname indents
= do start <- location
vis <- visibility
@ -1011,19 +1011,19 @@ stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str)))))
drop c [] = []
drop c (c' :: xs) = if c == c' then drop c xs else c' :: xs
onoff : SourceRule Bool
onoff : Rule Bool
onoff
= do exactIdent "on"
pure True
<|> do exactIdent "off"
pure False
extension : SourceRule LangExt
extension : Rule LangExt
extension
= do exactIdent "Borrowing"
pure Borrowing
totalityOpt : SourceRule TotalReq
totalityOpt : Rule TotalReq
totalityOpt
= do keyword "partial"
pure PartialOK
@ -1032,7 +1032,7 @@ totalityOpt
<|> do keyword "covering"
pure CoveringOnly
directive : FileName -> IndentInfo -> SourceRule Directive
directive : FileName -> IndentInfo -> Rule Directive
directive fname indents
= do pragma "hide"
n <- name
@ -1107,21 +1107,21 @@ directive fname indents
atEnd indents
pure (DefaultTotality tot)
fix : SourceRule Fixity
fix : Rule Fixity
fix
= do keyword "infixl"; pure InfixL
<|> do keyword "infixr"; pure InfixR
<|> do keyword "infix"; pure Infix
<|> do keyword "prefix"; pure Prefix
namespaceHead : SourceRule (List String)
namespaceHead : Rule (List String)
namespaceHead
= do keyword "namespace"
commit
ns <- nsIdent
ns <- namespacedIdent
pure ns
namespaceDecl : FileName -> IndentInfo -> SourceRule PDecl
namespaceDecl : FileName -> IndentInfo -> Rule PDecl
namespaceDecl fname indents
= do start <- location
ns <- namespaceHead
@ -1129,7 +1129,7 @@ namespaceDecl fname indents
ds <- assert_total (nonEmptyBlock (topDecl fname))
pure (PNamespace (MkFC fname start end) ns (concat ds))
transformDecl : FileName -> IndentInfo -> SourceRule PDecl
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl fname indents
= do start <- location
pragma "transform"
@ -1140,7 +1140,7 @@ transformDecl fname indents
end <- location
pure (PTransform (MkFC fname start end) n lhs rhs)
mutualDecls : FileName -> IndentInfo -> SourceRule PDecl
mutualDecls : FileName -> IndentInfo -> Rule PDecl
mutualDecls fname indents
= do start <- location
keyword "mutual"
@ -1149,7 +1149,7 @@ mutualDecls fname indents
end <- location
pure (PMutual (MkFC fname start end) (concat ds))
paramDecls : FileName -> IndentInfo -> SourceRule PDecl
paramDecls : FileName -> IndentInfo -> Rule PDecl
paramDecls fname indents
= do start <- location
keyword "parameters"
@ -1165,7 +1165,7 @@ paramDecls fname indents
end <- location
pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds)))
usingDecls : FileName -> IndentInfo -> SourceRule PDecl
usingDecls : FileName -> IndentInfo -> Rule PDecl
usingDecls fname indents
= do start <- location
keyword "using"
@ -1183,11 +1183,11 @@ usingDecls fname indents
end <- location
pure (PUsing (MkFC fname start end) us (collectDefs (concat ds)))
fnOpt : SourceRule PFnOpt
fnOpt : Rule PFnOpt
fnOpt = do x <- totalityOpt
pure $ IFnOpt (Totality x)
fnDirectOpt : FileName -> SourceRule PFnOpt
fnDirectOpt : FileName -> Rule PFnOpt
fnDirectOpt fname
= do pragma "hint"
pure $ IFnOpt (Hint True)
@ -1212,7 +1212,7 @@ fnDirectOpt fname
cs <- block (expr pdef fname)
pure $ PForeign cs
visOpt : FileName -> SourceRule (Either Visibility PFnOpt)
visOpt : FileName -> Rule (Either Visibility PFnOpt)
visOpt fname
= do vis <- visOption
pure (Left vis)
@ -1264,7 +1264,7 @@ implBinds fname indents
pure ((n, rig, tm) :: more)
<|> pure []
ifaceParam : FileName -> IndentInfo -> SourceRule (Name, PTerm)
ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm)
ifaceParam fname indents
= do symbol "("
n <- name
@ -1277,7 +1277,7 @@ ifaceParam fname indents
end <- location
pure (n, PInfer (MkFC fname start end))
ifaceDecl : FileName -> IndentInfo -> SourceRule PDecl
ifaceDecl : FileName -> IndentInfo -> Rule PDecl
ifaceDecl fname indents
= do start <- location
vis <- visibility
@ -1298,7 +1298,7 @@ ifaceDecl fname indents
pure (PInterface (MkFC fname start end)
vis cons n params det dc (collectDefs (concat body)))
implDecl : FileName -> IndentInfo -> SourceRule PDecl
implDecl : FileName -> IndentInfo -> Rule PDecl
implDecl fname indents
= do start <- location
visOpts <- many (visOpt fname)
@ -1325,7 +1325,7 @@ implDecl fname indents
vis opts Single impls cons n params iname nusing
(map (collectDefs . concat) body))
fieldDecl : FileName -> IndentInfo -> SourceRule (List PField)
fieldDecl : FileName -> IndentInfo -> Rule (List PField)
fieldDecl fname indents
= do symbol "{"
commit
@ -1337,7 +1337,7 @@ fieldDecl fname indents
atEnd indents
pure fs
where
fieldBody : PiInfo PTerm -> SourceRule (List PField)
fieldBody : PiInfo PTerm -> Rule (List PField)
fieldBody p
= do start <- location
m <- multiplicity
@ -1349,7 +1349,7 @@ fieldDecl fname indents
end <- location
pure (map (\n => MkField (MkFC fname start end)
rig p n ty) ns)
recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam fname indents
= do symbol "("
start <- location
@ -1374,7 +1374,7 @@ recordParam fname indents
end <- location
pure [(n, top, Explicit, PInfer (MkFC fname start end))]
recordDecl : FileName -> IndentInfo -> SourceRule PDecl
recordDecl : FileName -> IndentInfo -> Rule PDecl
recordDecl fname indents
= do start <- location
vis <- visibility
@ -1389,13 +1389,13 @@ recordDecl fname indents
pure (PRecord (MkFC fname start end)
vis n params (fst dcflds) (concat (snd dcflds)))
where
ctor : IndentInfo -> SourceRule Name
ctor : IndentInfo -> Rule Name
ctor idt = do exactIdent "constructor"
n <- name
atEnd idt
pure n
claim : FileName -> IndentInfo -> SourceRule PDecl
claim : FileName -> IndentInfo -> Rule PDecl
claim fname indents
= do start <- location
visOpts <- many (visOpt fname)
@ -1407,14 +1407,14 @@ claim fname indents
end <- location
pure (PClaim (MkFC fname start end) rig vis opts cl)
definition : FileName -> IndentInfo -> SourceRule PDecl
definition : FileName -> IndentInfo -> Rule PDecl
definition fname indents
= do start <- location
nd <- clause 0 fname indents
end <- location
pure (PDef (MkFC fname start end) [nd])
fixDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
fixDecl : FileName -> IndentInfo -> Rule (List PDecl)
fixDecl fname indents
= do start <- location
fixity <- fix
@ -1424,7 +1424,7 @@ fixDecl fname indents
end <- location
pure (map (PFixity (MkFC fname start end) fixity (fromInteger prec)) ops)
directiveDecl : FileName -> IndentInfo -> SourceRule PDecl
directiveDecl : FileName -> IndentInfo -> Rule PDecl
directiveDecl fname indents
= do start <- location
(do d <- directive fname indents
@ -1438,7 +1438,7 @@ directiveDecl fname indents
pure (PReflect (MkFC fname start end) tm))
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
-- topDecl : FileName -> IndentInfo -> Rule (List PDecl)
topDecl fname indents
= do d <- dataDecl fname indents
pure [d]
@ -1507,15 +1507,15 @@ collectDefs (d :: ds)
= d :: collectDefs ds
export
import_ : FileName -> IndentInfo -> SourceRule Import
import_ : FileName -> IndentInfo -> Rule Import
import_ fname indents
= do start <- location
keyword "import"
reexp <- option False (do keyword "public"
pure True)
ns <- nsIdent
ns <- namespacedIdent
nsAs <- option ns (do exactIdent "as"
nsIdent)
namespacedIdent)
end <- location
atEnd indents
pure (MkImport (MkFC fname start end) reexp ns nsAs)
@ -1526,7 +1526,7 @@ prog fname
= do start <- location
nspace <- option ["Main"]
(do keyword "module"
nsIdent)
namespacedIdent)
end <- location
imports <- block (import_ fname)
ds <- block (topDecl fname)
@ -1539,13 +1539,13 @@ progHdr fname
= do start <- location
nspace <- option ["Main"]
(do keyword "module"
nsIdent)
namespacedIdent)
end <- location
imports <- block (import_ fname)
pure (MkModule (MkFC fname start end)
nspace imports [])
parseMode : SourceRule REPLEval
parseMode : Rule REPLEval
parseMode
= do exactIdent "typecheck"
pure EvalTC
@ -1560,7 +1560,7 @@ parseMode
<|> do exactIdent "exec"
pure Execute
setVarOption : SourceRule REPLOpt
setVarOption : Rule REPLOpt
setVarOption
= do exactIdent "eval"
mode <- parseMode
@ -1572,7 +1572,7 @@ setVarOption
c <- unqualifiedName
pure (CG c)
setOption : Bool -> SourceRule REPLOpt
setOption : Bool -> Rule REPLOpt
setOption set
= do exactIdent "showimplicits"
pure (ShowImplicits set)
@ -1582,7 +1582,7 @@ setOption set
pure (ShowTypes set)
<|> if set then setVarOption else fatalError "Unrecognised option"
replCmd : List String -> SourceRule ()
replCmd : List String -> Rule ()
replCmd [] = fail "Unrecognised command"
replCmd (c :: cs)
= exactIdent c
@ -1590,7 +1590,7 @@ replCmd (c :: cs)
<|> replCmd cs
export
editCmd : SourceRule EditCmd
editCmd : Rule EditCmd
editCmd
= do replCmd ["typeat"]
line <- intLit
@ -1676,7 +1676,7 @@ data ParseCmd : Type where
ParseIdentCmd : String -> ParseCmd
CommandDefinition : Type
CommandDefinition = (List String, CmdArg, String, SourceRule REPLCmd)
CommandDefinition = (List String, CmdArg, String, Rule REPLCmd)
CommandTable : Type
CommandTable = List CommandDefinition
@ -1686,7 +1686,7 @@ extractNames (ParseREPLCmd names) = names
extractNames (ParseKeywordCmd keyword) = [keyword]
extractNames (ParseIdentCmd ident) = [ident]
runParseCmd : ParseCmd -> SourceRule ()
runParseCmd : ParseCmd -> Rule ()
runParseCmd (ParseREPLCmd names) = replCmd names
runParseCmd (ParseKeywordCmd keyword') = keyword keyword'
runParseCmd (ParseIdentCmd ident) = exactIdent ident
@ -1697,7 +1697,7 @@ noArgCmd parseCmd command doc = (names, NoArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1709,7 +1709,7 @@ nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1722,7 +1722,7 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1735,7 +1735,7 @@ optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1748,7 +1748,7 @@ numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1761,7 +1761,7 @@ compileArgsCmd parseCmd command doc = (names, FileArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1797,11 +1797,11 @@ help = (["<expr>"], NoArg, "Evaluate an expression") ::
map (\ (names, args, text, _) =>
(map (":" ++) names, args, text)) parserCommandsForHelp
nonEmptyCommand : SourceRule REPLCmd
nonEmptyCommand : Rule REPLCmd
nonEmptyCommand =
choice (map (\ (_, _, _, parser) => parser) parserCommandsForHelp)
eval : SourceRule REPLCmd
eval : Rule REPLCmd
eval = do
tm <- expr pdef "(interactive)" init
pure (Eval tm)

4
src/Idris/ProcessIdr.idr
View File

@ -177,7 +177,7 @@ modTime fname
pure (cast t)
export
getParseErrorLoc : String -> ParseError -> FC
getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0)
@ -195,7 +195,7 @@ readHeader path
where
-- Stop at the first :, that's definitely not part of the header, to
-- save lexing the whole file unnecessarily
isColon : TokenData SourceToken -> Bool
isColon : TokenData Token -> Bool
isColon t
= case tok t of
Symbol ":" => True

4
src/Idris/REPL.idr
View File

@ -327,7 +327,7 @@ processEdit (ExprSearch upd line name hints all)
if upd
then updateFile (proofSearch name res (integerToNat (cast (line - 1))))
else pure $ DisplayEdit [res]
[(n, nidx, PMDef pi [] (STerm tm) _ _)] =>
[(n, nidx, PMDef pi [] (STerm _ tm) _ _)] =>
case holeInfo pi of
NotHole => pure $ EditError "Not a searchable hole"
SolvedHole locs =>
@ -677,7 +677,7 @@ parseCmd : SourceEmptyRule (Maybe REPLCmd)
parseCmd = do c <- command; eoi; pure $ Just c
export
parseRepl : String -> Either ParseError (Maybe REPLCmd)
parseRepl : String -> Either (ParseError Token) (Maybe REPLCmd)
parseRepl inp
= case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd)

39
src/Idris/REPLCommon.idr
View File

@ -11,6 +11,7 @@ import Idris.IDEMode.Commands
import public Idris.REPLOpts
import Idris.Syntax
import Data.List
-- Output informational messages, unless quiet flag is set
export
@ -74,6 +75,44 @@ emitError err
addOne : (Int, Int) -> (Int, Int)
addOne (l, c) = (l + 1, c + 1)
export
emitWarning : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
{auto s : Ref Syn SyntaxInfo} ->
Warning -> Core ()
emitWarning w
= do opts <- get ROpts
case idemode opts of
REPL _ =>
do msg <- displayWarning w
coreLift $ putStrLn msg
IDEMode i _ f =>
do msg <- pwarning w
case getWarningLoc w of
Nothing => iputStrLn msg
Just fc =>
send f (SExpList [SymbolAtom "warning",
SExpList [toSExp (file fc),
toSExp (addOne (startPos fc)),
toSExp (addOne (endPos fc)),
toSExp msg,
-- highlighting; currently blank
SExpList []],
toSExp i])
where
addOne : (Int, Int) -> (Int, Int)
addOne (l, c) = (l + 1, c + 1)
export
emitWarnings : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
{auto s : Ref Syn SyntaxInfo} ->
Core ()
emitWarnings
= do defs <- get Ctxt
traverse_ emitWarning (reverse (warnings defs))
put Ctxt (record { warnings = [] } defs)
getFCLine : FC -> Int
getFCLine fc = fst (startPos fc)

27
src/Parser/Lexer/Common.idr
View File

@ -18,15 +18,13 @@ comment
-- There are multiple variants.
public export
data Flavour = Capitalised | AllowDashes | Normal
data Flavour = AllowDashes | Capitalised | Normal
export
isIdentStart : Flavour -> Char -> Bool
isIdentStart _ '_' = True
isIdentStart Capitalised x = isUpper x || x > chr 160
isIdentStart _ x = isAlpha x || x > chr 160
export
isIdentTrailing : Flavour -> Char -> Bool
isIdentTrailing AllowDashes '-' = True
isIdentTrailing _ '\'' = True
@ -45,3 +43,26 @@ ident : Flavour -> Lexer
ident flavour =
(pred $ isIdentStart flavour) <+>
(many . pred $ isIdentTrailing flavour)
export
isIdentNormal : String -> Bool
isIdentNormal = isIdent Normal
export
identNormal : Lexer
identNormal = ident Normal
export
identAllowDashes : Lexer
identAllowDashes = ident AllowDashes
namespaceIdent : Lexer
namespaceIdent = ident Capitalised <+> many (is '.' <+> ident Capitalised <+> expect (is '.'))
export
namespacedIdent : Lexer
namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal)
export
spacesOrNewlines : Lexer
spacesOrNewlines = some (space <|> newline)

65
src/Parser/Lexer/Package.idr Normal file
View File

@ -0,0 +1,65 @@
module Parser.Lexer.Package
import public Parser.Lexer.Common
import public Text.Lexer
import public Text.Parser
import Data.List
import Data.Strings
import Data.String.Extra
import Utils.String
%default total
public export
data Token
= Comment String
| EndOfInput
| Equals
| DotSepIdent (List String)
| Separator
| Space
| StringLit String
public export
Show Token where
show (Comment str) = "Comment: " ++ str
show EndOfInput = "EndOfInput"
show Equals = "Equals"
show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep dsid
show Separator = "Separator"
show Space = "Space"
show (StringLit s) = "StringLit: " ++ s
equals : Lexer
equals = is '='
separator : Lexer
separator = is ','
rawTokens : TokenMap Token
rawTokens =
[ (equals, const Equals)
, (comment, Comment . drop 2)
, (namespacedIdent, DotSepIdent . splitNamespace)
, (identAllowDashes, DotSepIdent . pure)
, (separator, const Separator)
, (spacesOrNewlines, const Space)
, (stringLit, \s => StringLit (stripQuotes s))
]
where
splitNamespace : String -> List String
splitNamespace = Data.Strings.split (== '.')
export
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex str =
case lexTo (const False) rawTokens str of
(tokenData, (l, c, "")) =>
Right $ (filter (useful . tok) tokenData) ++ [MkToken l c EndOfInput]
(_, fail) => Left fail
where
useful : Token -> Bool
useful (Comment c) = False
useful Space = False
useful _ = True

115
src/Parser/Lexer/Source.idr
View File

@ -12,46 +12,50 @@ import Utils.String
%default total
public export
data SourceToken
= NSIdent (List String)
| HoleIdent String
| Literal Integer
| StrLit String
| CharLit String
data Token
-- Literals
= CharLit String
| DoubleLit Double
| IntegerLit Integer
| StringLit String
-- Identifiers
| HoleIdent String
| Ident String
| DotSepIdent (List String)
| RecordField String
| Symbol String
| Keyword String
| Unrecognised String
-- Comments
| Comment String
| DocComment String
-- Special
| CGDirective String
| RecordField String
| Pragma String
| EndInput
| Keyword String
| Pragma String
| Unrecognised String
export
Show SourceToken where
show (HoleIdent x) = "hole identifier " ++ x
show (Literal x) = "literal " ++ show x
show (StrLit x) = "string " ++ show x
Show Token where
-- Literals
show (CharLit x) = "character " ++ show x
show (DoubleLit x) = "double " ++ show x
show (IntegerLit x) = "literal " ++ show x
show (StringLit x) = "string " ++ show x
-- Identifiers
show (HoleIdent x) = "hole identifier " ++ x
show (Ident x) = "identifier " ++ x
show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (reverse xs)
show (RecordField x) = "record field " ++ x
show (Symbol x) = "symbol " ++ x
show (Keyword x) = x
show (Unrecognised x) = "Unrecognised " ++ x
-- Comments
show (Comment _) = "comment"
show (DocComment _) = "doc comment"
-- Special
show (CGDirective x) = "CGDirective " ++ x
show (RecordField x) = "record field " ++ x
show (Pragma x) = "pragma " ++ x
show EndInput = "end of input"
show (NSIdent [x]) = "identifier " ++ x
show (NSIdent xs) = "namespaced identifier " ++ dotSep (reverse xs)
where
dotSep : List String -> String
dotSep [] = ""
dotSep [x] = x
dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]
show (Keyword x) = x
show (Pragma x) = "pragma " ++ x
show (Unrecognised x) = "Unrecognised " ++ x
mutual
||| The mutually defined functions represent different states in a
@ -102,29 +106,14 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1
docComment : Lexer
docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')
export
isIdentNormal : String -> Bool
isIdentNormal = isIdent Normal
export
identNormal : Lexer
identNormal = ident Normal
export
identAllowDashes : Lexer
identAllowDashes = ident AllowDashes
holeIdent : Lexer
holeIdent = is '?' <+> ident Normal
nsIdent : Lexer
nsIdent = ident Capitalised <+> many (is '.' <+> ident Normal)
holeIdent = is '?' <+> identNormal
recField : Lexer
recField = is '.' <+> ident Normal
recField = is '.' <+> identNormal
pragma : Lexer
pragma = is '%' <+> ident Normal
pragma = is '%' <+> identNormal
doubleLit : Lexer
doubleLit
@ -142,7 +131,7 @@ cgDirective
is '}')
<|> many (isNot '\n'))
mkDirective : String -> SourceToken
mkDirective : String -> Token
mkDirective str = CGDirective (trim (substr 3 (length str) str))
-- Reserved words
@ -171,7 +160,6 @@ symbols
"(", ")", "{", "}", "[", "]", ",", ";", "_",
"`(", "`"]
export
isOpChar : Char -> Bool
isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
@ -205,7 +193,7 @@ fromOctLit str
Nothing => 0 -- can't happen if the literal lexed correctly
Just n => cast n
rawTokens : TokenMap SourceToken
rawTokens : TokenMap Token
rawTokens =
[(comment, Comment),
(blockComment, Comment),
@ -214,31 +202,30 @@ rawTokens =
(holeIdent, \x => HoleIdent (assert_total (strTail x)))] ++
map (\x => (exact x, Symbol)) symbols ++
[(doubleLit, \x => DoubleLit (cast x)),
(hexLit, \x => Literal (fromHexLit x)),
(octLit, \x => Literal (fromOctLit x)),
(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(hexLit, \x => IntegerLit (fromHexLit x)),
(octLit, \x => IntegerLit (fromOctLit x)),
(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(charLit, \x => CharLit (stripQuotes x)),
(recField, \x => RecordField (assert_total $ strTail x)),
(nsIdent, parseNSIdent),
(ident Normal, parseIdent),
(namespacedIdent, parseNamespace),
(identNormal, parseIdent),
(pragma, \x => Pragma (assert_total $ strTail x)),
(space, Comment),
(validSymbol, Symbol),
(symbol, Unrecognised)]
where
parseNSIdent : String -> SourceToken
parseNSIdent = NSIdent . reverse . split (== '.')
parseIdent : String -> SourceToken
parseIdent x =
if x `elem` keywords
then Keyword x
else NSIdent [x]
parseIdent : String -> Token
parseIdent x = if x `elem` keywords then Keyword x
else Ident x
parseNamespace : String -> Token
parseNamespace ns = case Data.List.reverse . split (== '.') $ ns of
[ident] => parseIdent ident
ns => DotSepIdent ns
export
lexTo : (TokenData SourceToken -> Bool) ->
String -> Either (Int, Int, String) (List (TokenData SourceToken))
lexTo : (TokenData Token -> Bool) ->
String -> Either (Int, Int, String) (List (TokenData Token))
lexTo pred str
= case lexTo pred rawTokens str of
-- Add the EndInput token so that we'll have a line and column
@ -247,12 +234,12 @@ lexTo pred str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData SourceToken -> Bool
notComment : TokenData Token -> Bool
notComment t = case tok t of
Comment _ => False
DocComment _ => False -- TODO!
_ => True
export
lex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex = lexTo (const False)

24
src/Parser/Package.idr Normal file
View File

@ -0,0 +1,24 @@
module Parser.Package
import public Parser.Lexer.Package
import public Parser.Rule.Package
import public Text.Lexer
import public Text.Parser
import public Parser.Support
import System.File
import Utils.Either
export
runParser : String -> Rule ty -> Either (ParseError Token) ty
runParser str p
= do toks <- mapError LexFail $ lex str
parsed <- mapError toGenericParsingError $ parse p toks
Right (fst parsed)
export
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
= do Right str <- readFile fn
| Left err => pure (Left (FileFail err))
pure (runParser str p)

79
src/Parser/Rule/Package.idr Normal file
View File

@ -0,0 +1,79 @@
module Parser.Rule.Package
import public Parser.Lexer.Package
import public Parser.Rule.Common
import Data.List
%default total
public export
Rule : Type -> Type
Rule = Rule Token
public export
PackageEmptyRule : Type -> Type
PackageEmptyRule = EmptyRule Token
export
equals : Rule ()
equals = terminal "Expected equals"
(\x => case tok x of
Equals => Just ()
_ => Nothing)
export
eoi : Rule ()
eoi = terminal "Expected end of input"
(\x => case tok x of
EndOfInput => Just ()
_ => Nothing)
export
exactProperty : String -> Rule String
exactProperty p = terminal ("Expected property " ++ p)
(\x => case tok x of
DotSepIdent [p'] =>
if p == p' then Just p
else Nothing
_ => Nothing)
export
stringLit : Rule String
stringLit = terminal "Expected string"
(\x => case tok x of
StringLit str => Just str
_ => Nothing)
export
namespacedIdent : Rule (List String)
namespacedIdent = terminal "Expected namespaced identifier"
(\x => case tok x of
DotSepIdent nsid => Just $ reverse nsid
_ => Nothing)
export
moduleIdent : Rule (List String)
moduleIdent = terminal "Expected module identifier"
(\x => case tok x of
DotSepIdent m => Just $ reverse m
_ => Nothing)
export
packageName : Rule String
packageName = terminal "Expected package name"
(\x => case tok x of
DotSepIdent [str] =>
if isIdent AllowDashes str then Just str
else Nothing
_ => Nothing)
sep' : Rule ()
sep' = terminal "Expected separator"
(\x => case tok x of
Separator => Just ()
_ => Nothing)
export
sep : Rule t -> Rule (List t)
sep rule = sepBy1 sep' rule

97
src/Parser/Rule/Source.idr
View File

@ -9,12 +9,12 @@ import Core.TT
%default total
public export
SourceRule : Type -> Type
SourceRule = Rule SourceToken
Rule : Type -> Type
Rule = Rule Token
public export
SourceEmptyRule : Type -> Type
SourceEmptyRule = EmptyRule SourceToken
SourceEmptyRule = EmptyRule Token
export
eoi : SourceEmptyRule ()
@ -22,48 +22,48 @@ eoi
= do nextIs "Expected end of input" (isEOI . tok)
pure ()
where
isEOI : SourceToken -> Bool
isEOI : Token -> Bool
isEOI EndInput = True
isEOI _ = False
export
constant : SourceRule Constant
constant : Rule Constant
constant
= terminal "Expected constant"
(\x => case tok x of
Literal i => Just (BI i)
StrLit s => case escape s of
Nothing => Nothing
Just s' => Just (Str s')
CharLit c => case getCharLit c of
Nothing => Nothing
Just c' => Just (Ch c')
DoubleLit d => Just (Db d)
NSIdent ["Int"] => Just IntType
NSIdent ["Integer"] => Just IntegerType
NSIdent ["String"] => Just StringType
NSIdent ["Char"] => Just CharType
NSIdent ["Double"] => Just DoubleType
DoubleLit d => Just (Db d)
IntegerLit i => Just (BI i)
StringLit s => case escape s of
Nothing => Nothing
Just s' => Just (Str s')
Ident "Char" => Just CharType
Ident "Double" => Just DoubleType
Ident "Int" => Just IntType
Ident "Integer" => Just IntegerType
Ident "String" => Just StringType
_ => Nothing)
export
intLit : SourceRule Integer
intLit : Rule Integer
intLit
= terminal "Expected integer literal"
(\x => case tok x of
Literal i => Just i
IntegerLit i => Just i
_ => Nothing)
export
strLit : SourceRule String
strLit : Rule String
strLit
= terminal "Expected string literal"
(\x => case tok x of
StrLit s => Just s
StringLit s => Just s
_ => Nothing)
export
recField : SourceRule Name
recField : Rule Name
recField
= terminal "Expected record field"
(\x => case tok x of
@ -71,7 +71,7 @@ recField
_ => Nothing)
export
symbol : String -> SourceRule ()
symbol : String -> Rule ()
symbol req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
@ -80,7 +80,7 @@ symbol req
_ => Nothing)
export
keyword : String -> SourceRule ()
keyword : String -> Rule ()
keyword req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
@ -89,16 +89,16 @@ keyword req
_ => Nothing)
export
exactIdent : String -> SourceRule ()
exactIdent : String -> Rule ()
exactIdent req
= terminal ("Expected " ++ req)
(\x => case tok x of
NSIdent [s] => if s == req then Just ()
else Nothing
Ident s => if s == req then Just ()
else Nothing
_ => Nothing)
export
pragma : String -> SourceRule ()
pragma : String -> Rule ()
pragma n =
terminal ("Expected pragma " ++ n)
(\x => case tok x of
@ -109,7 +109,7 @@ pragma n =
_ => Nothing)
export
operator : SourceRule Name
operator : Rule Name
operator
= terminal "Expected operator"
(\x => case tok x of
@ -119,27 +119,28 @@ operator
else Just (UN s)
_ => Nothing)
identPart : SourceRule String
identPart : Rule String
identPart
= terminal "Expected name"
(\x => case tok x of
NSIdent [str] => Just str
Ident str => Just str
_ => Nothing)
export
nsIdent : SourceRule (List String)
nsIdent
namespacedIdent : Rule (List String)
namespacedIdent
= terminal "Expected namespaced name"
(\x => case tok x of
NSIdent ns => Just ns
DotSepIdent ns => Just ns
Ident i => Just $ [i]
_ => Nothing)
export
unqualifiedName : SourceRule String
unqualifiedName : Rule String
unqualifiedName = identPart
export
holeName : SourceRule String
holeName : Rule String
holeName
= terminal "Expected hole name"
(\x => case tok x of
@ -152,15 +153,15 @@ reservedNames
"Lazy", "Inf", "Force", "Delay"]
export
name : SourceRule Name
name : Rule Name
name = opNonNS <|> do
ns <- nsIdent
ns <- namespacedIdent
opNS ns <|> nameNS ns
where
reserved : String -> Bool
reserved n = n `elem` reservedNames
nameNS : List String -> Grammar (TokenData SourceToken) False Name
nameNS : List String -> SourceEmptyRule Name
nameNS [] = pure $ UN "IMPOSSIBLE"
nameNS [x] =
if reserved x
@ -171,10 +172,10 @@ name = opNonNS <|> do
then fail $ "can't use reserved name " ++ x
else pure $ NS xs (UN x)
opNonNS : SourceRule Name
opNonNS : Rule Name
opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
opNS : List String -> SourceRule Name
opNS : List String -> Rule Name
opNS ns = do
symbol ".("
n <- (operator <|> recField)
@ -238,7 +239,7 @@ checkValid (AfterPos x) c = if c >= x
checkValid EndOfBlock c = fail "End of block"
||| Any token which indicates the end of a statement/block
isTerminator : SourceToken -> Bool
isTerminator : Token -> Bool
isTerminator (Symbol ",") = True
isTerminator (Symbol "]") = True
isTerminator (Symbol ";") = True
@ -318,8 +319,8 @@ terminator valid laststart
afterDedent EndOfBlock col = pure EndOfBlock
-- Parse an entry in a block
blockEntry : ValidIndent -> (IndentInfo -> SourceRule ty) ->
SourceRule (ty, ValidIndent)
blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
Rule (ty, ValidIndent)
blockEntry valid rule
= do col <- column
checkValid valid col
@ -327,7 +328,7 @@ blockEntry valid rule
valid' <- terminator valid col
pure (p, valid')
blockEntries : ValidIndent -> (IndentInfo -> SourceRule ty) ->
blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
SourceEmptyRule (List ty)
blockEntries valid rule
= do eoi; pure []
@ -337,7 +338,7 @@ blockEntries valid rule
<|> pure []
export
block : (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty)
block : (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty)
block item
= do symbol "{"
commit
@ -353,7 +354,7 @@ block item
||| by curly braces). `rule` is a function of the actual indentation
||| level.
export
blockAfter : Int -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty)
blockAfter : Int -> (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty)
blockAfter mincol item
= do symbol "{"
commit
@ -366,7 +367,7 @@ blockAfter mincol item
else blockEntries (AtPos col) item
export
blockWithOptHeaderAfter : Int -> (IndentInfo -> SourceRule hd) -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> SourceEmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter {ty} mincol header item
= do symbol "{"
commit
@ -379,7 +380,7 @@ blockWithOptHeaderAfter {ty} mincol header item
ps <- blockEntries (AtPos col) item
pure (map fst hidt, ps)
where
restOfBlock : Maybe (hd, ValidIndent) -> SourceRule (Maybe hd, List ty)
restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
symbol "}"
pure (Just h, ps)
@ -388,7 +389,7 @@ blockWithOptHeaderAfter {ty} mincol header item
pure (Nothing, ps)
export
nonEmptyBlock : (IndentInfo -> SourceRule ty) -> SourceRule (List ty)
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
nonEmptyBlock item
= do symbol "{"
commit

14
src/Parser/Source.idr
View File

@ -3,8 +3,6 @@ module Parser.Source
import public Parser.Lexer.Source
import public Parser.Rule.Source
import public Parser.Unlit
import public Text.Lexer
import public Text.Parser
import System.File
import Utils.Either
@ -13,21 +11,21 @@ import Utils.Either
export
runParserTo : {e : _} ->
Maybe LiterateStyle -> (TokenData SourceToken -> Bool) ->
String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
Maybe LiterateStyle -> (TokenData Token -> Bool) ->
String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
runParserTo lit pred str p
= do str <- mapError LitFail $ unlit lit str
toks <- mapError LexFail $ lexTo pred str
parsed <- mapError mapParseError $ parse p toks
parsed <- mapError toGenericParsingError $ parse p toks
Right (fst parsed)
export
runParser : {e : _} ->
Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
runParser lit = runParserTo lit (const False)
export covering -- readFile might not terminate
parseFile : (fn : String) -> SourceRule ty -> IO (Either ParseError ty)
export covering
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
= do Right str <- readFile fn
| Left err => pure (Left (FileFail err))

18
src/Parser/Support.idr
View File

@ -1,6 +1,5 @@
module Parser.Support
import public Parser.Lexer.Source
import public Text.Lexer
import public Text.Parser
@ -13,13 +12,14 @@ import System.File
%default total
public export
data ParseError = ParseFail String (Maybe (Int, Int)) (List SourceToken)
| LexFail (Int, Int, String)
| FileFail FileError
| LitFail LiterateError
data ParseError tok
= ParseFail String (Maybe (Int, Int)) (List tok)
| LexFail (Int, Int, String)
| FileFail FileError
| LitFail LiterateError
export
Show ParseError where
Show tok => Show (ParseError tok) where
show (ParseFail err loc toks)
= "Parse error: " ++ err ++ " (next tokens: "
++ show (take 10 toks) ++ ")"
@ -31,9 +31,9 @@ Show ParseError where
= "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str
export
mapParseError : ParseError (TokenData SourceToken) -> ParseError
mapParseError (Error err []) = ParseFail err Nothing []
mapParseError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts))
toGenericParsingError : ParsingError (TokenData token) -> ParseError token
toGenericParsingError (Error err []) = ParseFail err Nothing []
toGenericParsingError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts))
export
hex : Char -> Maybe Int

2
src/TTImp/Elab/Delayed.idr
View File

@ -222,7 +222,7 @@ retryDelayed' errmode acc (d@(_, i, elab) :: ds)
let ds' = reverse (delayedElab ust) ++ ds
updateDef (Resolved i) (const (Just
(PMDef (MkPMDefInfo NotHole True) [] (STerm tm) (STerm tm) [])))
(PMDef (MkPMDefInfo NotHole True) [] (STerm 0 tm) (STerm 0 tm) [])))
logTerm 5 ("Resolved delayed hole " ++ show i) tm
logTermNF 5 ("Resolved delayed hole NF " ++ show i) [] tm
removeHole i

98
src/TTImp/Parser.idr
View File

@ -12,7 +12,7 @@ import Data.List
import Data.List.Views
import Data.Strings
topDecl : FileName -> IndentInfo -> SourceRule ImpDecl
topDecl : FileName -> IndentInfo -> Rule ImpDecl
-- All the clauses get parsed as one-clause definitions. Collect any
-- neighbouring clauses with the same function name into one definition.
export
@ -26,7 +26,7 @@ collectDefs : List ImpDecl -> List ImpDecl
%hide Lexer.Core.(<|>)
%hide Prelude.(<|>)
atom : FileName -> SourceRule RawImp
atom : FileName -> Rule RawImp
atom fname
= do start <- location
x <- constant
@ -62,7 +62,7 @@ atom fname
end <- location
pure (IHole (MkFC fname start end) x)
visOption : SourceRule Visibility
visOption : Rule Visibility
visOption
= do keyword "public"
keyword "export"
@ -77,7 +77,7 @@ visibility
= visOption
<|> pure Private
totalityOpt : SourceRule TotalReq
totalityOpt : Rule TotalReq
totalityOpt
= do keyword "partial"
pure PartialOK
@ -86,11 +86,11 @@ totalityOpt
<|> do keyword "covering"
pure CoveringOnly
fnOpt : SourceRule FnOpt
fnOpt : Rule FnOpt
fnOpt = do x <- totalityOpt
pure $ Totality x
fnDirectOpt : SourceRule FnOpt
fnDirectOpt : Rule FnOpt
fnDirectOpt
= do pragma "hint"
pure (Hint True)
@ -105,7 +105,7 @@ fnDirectOpt
<|> do pragma "extern"
pure ExternFn
visOpt : SourceRule (Either Visibility FnOpt)
visOpt : Rule (Either Visibility FnOpt)
visOpt
= do vis <- visOption
pure (Left vis)
@ -127,7 +127,7 @@ getRight : Either a b -> Maybe b
getRight (Left _) = Nothing
getRight (Right v) = Just v
bindSymbol : SourceRule (PiInfo RawImp)
bindSymbol : Rule (PiInfo RawImp)
bindSymbol
= do symbol "->"
pure Explicit
@ -135,7 +135,7 @@ bindSymbol
pure AutoImplicit
mutual
appExpr : FileName -> IndentInfo -> SourceRule RawImp
appExpr : FileName -> IndentInfo -> Rule RawImp
appExpr fname indents
= case_ fname indents
<|> lazy fname indents
@ -155,7 +155,7 @@ mutual
= applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args
argExpr : FileName -> IndentInfo ->
SourceRule (Either RawImp (Maybe Name, RawImp))
Rule (Either RawImp (Maybe Name, RawImp))
argExpr fname indents
= do continue indents
arg <- simpleExpr fname indents
@ -164,7 +164,7 @@ mutual
arg <- implicitArg fname indents
pure (Right arg)
implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, RawImp)
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, RawImp)
implicitArg fname indents
= do start <- location
symbol "{"
@ -183,7 +183,7 @@ mutual
symbol "}"
pure (Nothing, tm)
as : FileName -> IndentInfo -> SourceRule RawImp
as : FileName -> IndentInfo -> Rule RawImp
as fname indents
= do start <- location
x <- unqualifiedName
@ -192,7 +192,7 @@ mutual
end <- location
pure (IAs (MkFC fname start end) UseRight (UN x) pat)
simpleExpr : FileName -> IndentInfo -> SourceRule RawImp
simpleExpr : FileName -> IndentInfo -> Rule RawImp
simpleExpr fname indents
= as fname indents
<|> atom fname
@ -223,7 +223,7 @@ mutual
= IPi fc rig p n ty (pibindAll fc p rest scope)
bindList : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Name, RawImp))
Rule (List (RigCount, Name, RawImp))
bindList fname start indents
= sepBy1 (symbol ",")
(do rigc <- multiplicity
@ -238,7 +238,7 @@ mutual
pibindListName : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Name, RawImp))
Rule (List (RigCount, Name, RawImp))
pibindListName fname start indents
= do rigc <- multiplicity
ns <- sepBy1 (symbol ",") unqualifiedName
@ -256,13 +256,13 @@ mutual
pure (rig, n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Maybe Name, RawImp))
Rule (List (RigCount, Maybe Name, RawImp))
pibindList fname start indents
= do params <- pibindListName fname start indents
pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
autoImplicitPi : FileName -> IndentInfo -> SourceRule RawImp
autoImplicitPi : FileName -> IndentInfo -> Rule RawImp
autoImplicitPi fname indents
= do start <- location
symbol "{"
@ -275,7 +275,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
forall_ : FileName -> IndentInfo -> SourceRule RawImp
forall_ : FileName -> IndentInfo -> Rule RawImp
forall_ fname indents
= do start <- location
keyword "forall"
@ -290,7 +290,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> SourceRule RawImp
implicitPi : FileName -> IndentInfo -> Rule RawImp
implicitPi fname indents
= do start <- location
symbol "{"
@ -301,7 +301,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
explicitPi : FileName -> IndentInfo -> SourceRule RawImp
explicitPi : FileName -> IndentInfo -> Rule RawImp
explicitPi fname indents
= do start <- location
symbol "("
@ -312,7 +312,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) exp binders scope)
lam : FileName -> IndentInfo -> SourceRule RawImp
lam : FileName -> IndentInfo -> Rule RawImp
lam fname indents
= do start <- location
symbol "\\"
@ -328,7 +328,7 @@ mutual
bindAll fc ((rig, n, ty) :: rest) scope
= ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)
let_ : FileName -> IndentInfo -> SourceRule RawImp
let_ : FileName -> IndentInfo -> Rule RawImp
let_ fname indents
= do start <- location
keyword "let"
@ -353,7 +353,7 @@ mutual
end <- location
pure (ILocal (MkFC fname start end) (collectDefs ds) scope)
case_ : FileName -> IndentInfo -> SourceRule RawImp
case_ : FileName -> IndentInfo -> Rule RawImp
case_ fname indents
= do start <- location
keyword "case"
@ -364,14 +364,14 @@ mutual
pure (let fc = MkFC fname start end in
ICase fc scr (Implicit fc False) alts)
caseAlt : FileName -> IndentInfo -> SourceRule ImpClause
caseAlt : FileName -> IndentInfo -> Rule ImpClause
caseAlt fname indents
= do start <- location
lhs <- appExpr fname indents
caseRHS fname indents start lhs
caseRHS : FileName -> IndentInfo -> (Int, Int) -> RawImp ->
SourceRule ImpClause
Rule ImpClause
caseRHS fname indents start lhs
= do symbol "=>"
continue indents
@ -384,7 +384,7 @@ mutual
end <- location
pure (ImpossibleClause (MkFC fname start end) lhs)
record_ : FileName -> IndentInfo -> SourceRule RawImp
record_ : FileName -> IndentInfo -> Rule RawImp
record_ fname indents
= do start <- location
keyword "record"
@ -396,7 +396,7 @@ mutual
end <- location
pure (IUpdate (MkFC fname start end) fs sc)
field : FileName -> IndentInfo -> SourceRule IFieldUpdate
field : FileName -> IndentInfo -> Rule IFieldUpdate
field fname indents
= do path <- sepBy1 (symbol "->") unqualifiedName
upd <- (do symbol "="; pure ISetField)
@ -405,7 +405,7 @@ mutual
val <- appExpr fname indents
pure (upd path val)
rewrite_ : FileName -> IndentInfo -> SourceRule RawImp
rewrite_ : FileName -> IndentInfo -> Rule RawImp
rewrite_ fname indents
= do start <- location
keyword "rewrite"
@ -415,7 +415,7 @@ mutual
end <- location
pure (IRewrite (MkFC fname start end) rule tm)
lazy : FileName -> IndentInfo -> SourceRule RawImp
lazy : FileName -> IndentInfo -> Rule RawImp
lazy fname indents
= do start <- location
exactIdent "Lazy"
@ -439,7 +439,7 @@ mutual
pure (IForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> SourceRule RawImp
binder : FileName -> IndentInfo -> Rule RawImp
binder fname indents
= autoImplicitPi fname indents
<|> forall_ fname indents
@ -448,7 +448,7 @@ mutual
<|> lam fname indents
<|> let_ fname indents
typeExpr : FileName -> IndentInfo -> SourceRule RawImp
typeExpr : FileName -> IndentInfo -> Rule RawImp
typeExpr fname indents
= do start <- location
arg <- appExpr fname indents
@ -467,10 +467,10 @@ mutual
(mkPi start end a as)
export
expr : FileName -> IndentInfo -> SourceRule RawImp
expr : FileName -> IndentInfo -> Rule RawImp
expr = typeExpr
tyDecl : FileName -> IndentInfo -> SourceRule ImpTy
tyDecl : FileName -> IndentInfo -> Rule ImpTy
tyDecl fname indents
= do start <- location
n <- name
@ -483,7 +483,7 @@ tyDecl fname indents
mutual
parseRHS : (withArgs : Nat) ->
FileName -> IndentInfo -> (Int, Int) -> RawImp ->
SourceRule (Name, ImpClause)
Rule (Name, ImpClause)
parseRHS withArgs fname indents start lhs
= do symbol "="
commit
@ -518,7 +518,7 @@ mutual
ifThenElse True t e = t
ifThenElse False t e = e
clause : Nat -> FileName -> IndentInfo -> SourceRule (Name, ImpClause)
clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause)
clause withArgs fname indents
= do start <- location
lhs <- expr fname indents
@ -531,7 +531,7 @@ mutual
applyArgs f [] = f
applyArgs f ((fc, a) :: args) = applyArgs (IApp fc f a) args
parseWithArg : SourceRule (FC, RawImp)
parseWithArg : Rule (FC, RawImp)
parseWithArg
= do symbol "|"
start <- location
@ -539,14 +539,14 @@ mutual
end <- location
pure (MkFC fname start end, tm)
definition : FileName -> IndentInfo -> SourceRule ImpDecl
definition : FileName -> IndentInfo -> Rule ImpDecl
definition fname indents
= do start <- location
nd <- clause 0 fname indents
end <- location
pure (IDef (MkFC fname start end) (fst nd) [snd nd])
dataOpt : SourceRule DataOpt
dataOpt : Rule DataOpt
dataOpt
= do exactIdent "noHints"
pure NoHints
@ -556,7 +556,7 @@ dataOpt
ns <- some name
pure (SearchBy ns)
dataDecl : FileName -> IndentInfo -> SourceRule ImpData
dataDecl : FileName -> IndentInfo -> Rule ImpData
dataDecl fname indents
= do start <- location
keyword "data"
@ -572,7 +572,7 @@ dataDecl fname indents
end <- location
pure (MkImpData (MkFC fname start end) n ty opts cs)
recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam fname indents
= do symbol "("
start <- location
@ -597,7 +597,7 @@ recordParam fname indents
end <- location
pure [(n, top, Explicit, Implicit (MkFC fname start end) False)]
fieldDecl : FileName -> IndentInfo -> SourceRule (List IField)
fieldDecl : FileName -> IndentInfo -> Rule (List IField)
fieldDecl fname indents
= do symbol "{"
commit
@ -609,7 +609,7 @@ fieldDecl fname indents
atEnd indents
pure fs
where
fieldBody : PiInfo RawImp -> SourceRule (List IField)
fieldBody : PiInfo RawImp -> Rule (List IField)
fieldBody p
= do start <- location
ns <- sepBy1 (symbol ",") unqualifiedName
@ -619,7 +619,7 @@ fieldDecl fname indents
pure (map (\n => MkIField (MkFC fname start end)
linear p (UN n) ty) ns)
recordDecl : FileName -> IndentInfo -> SourceRule ImpDecl
recordDecl : FileName -> IndentInfo -> Rule ImpDecl
recordDecl fname indents
= do start <- location
vis <- visibility
@ -638,14 +638,14 @@ recordDecl fname indents
IRecord fc Nothing vis
(MkImpRecord fc n params dc (concat flds)))
namespaceDecl : SourceRule (List String)
namespaceDecl : Rule (List String)
namespaceDecl
= do keyword "namespace"
commit
ns <- nsIdent
ns <- namespacedIdent
pure ns
directive : FileName -> IndentInfo -> SourceRule ImpDecl
directive : FileName -> IndentInfo -> Rule ImpDecl
directive fname indents
= do pragma "logging"
commit
@ -672,7 +672,7 @@ directive fname indents
IPragma (\c, nest, env => setRewrite {c} fc eq rw))
-}
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> SourceRule ImpDecl
-- topDecl : FileName -> IndentInfo -> Rule ImpDecl
topDecl fname indents
= do start <- location
vis <- visibility
@ -720,14 +720,14 @@ collectDefs (d :: ds)
-- full programs
export
prog : FileName -> SourceRule (List ImpDecl)
prog : FileName -> Rule (List ImpDecl)
prog fname
= do ds <- nonEmptyBlock (topDecl fname)
pure (collectDefs ds)
-- TTImp REPL commands
export
command : SourceRule ImpREPL
command : Rule ImpREPL
command
= do symbol ":"; exactIdent "t"
tm <- expr "(repl)" init

15
src/TTImp/ProcessDef.idr
View File

@ -650,7 +650,7 @@ mkRunTime fc n
MissingCases _ => addErrorCase clauses_init
_ => clauses_init
(rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty clauses
(rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses
log 5 $ show cov ++ ":\nRuntime tree for " ++ show (fullname gdef) ++ ": " ++ show tree_rt
let Just Refl = nameListEq cargs rargs
@ -715,6 +715,11 @@ toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
toPats (MkClause {vars} env lhs rhs)
= (_ ** (env, lhs, rhs))
warnUnreachable : {auto c : Ref Ctxt Defs} ->
Clause -> Core ()
warnUnreachable (MkClause env lhs rhs)
= recordWarning (UnreachableClause (getLoc lhs) env lhs)
export
processDef : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -738,7 +743,10 @@ processDef opts nest env fc n_in cs_in
cs <- traverse (checkClause mult hashit nidx opts nest env) cs_in
let pats = map toPats (rights cs)
(cargs ** tree_ct) <- getPMDef fc CompileTime n ty (rights cs)
(cargs ** (tree_ct, unreachable)) <-
getPMDef fc CompileTime n ty (rights cs)
traverse_ warnUnreachable unreachable
logC 2 (do t <- toFullNames tree_ct
pure ("Case tree for " ++ show n ++ ": " ++ show t))
@ -842,7 +850,8 @@ processDef opts nest env fc n_in cs_in
checkCoverage n ty mult cs
= do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
let covcs = mapMaybe id covcs'
(_ ** ctree) <- getPMDef fc CompileTime (Resolved n) ty covcs
(_ ** (ctree, _)) <-
getPMDef fc CompileTime (Resolved n) ty covcs
log 3 $ "Working from " ++ show !(toFullNames ctree)
missCase <- if any catchAll covcs
then do log 3 $ "Catch all case in " ++ show n

4
src/Text/Parser/Core.idr
View File

@ -272,14 +272,14 @@ mutual
-- doParse _ _ _ = Failure True True "Help the coverage checker!" []
public export
data ParseError tok = Error String (List tok)
data ParsingError tok = Error String (List tok)
||| Parse a list of tokens according to the given grammar. If successful,
||| returns a pair of the parse result and the unparsed tokens (the remaining
||| input).
export
parse : {c : Bool} -> (act : Grammar tok c ty) -> (xs : List tok) ->
Either (ParseError tok) (ty, List tok)
Either (ParsingError tok) (ty, List tok)
parse act xs
= case doParse False act xs of
Failure _ _ msg ts => Left (Error msg ts)

6
src/Utils/String.idr
View File

@ -2,6 +2,12 @@ module Utils.String
%default total
export
dotSep : List String -> String
dotSep [] = ""
dotSep [x] = x
dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]
export
stripQuotes : (str : String) -> String
stripQuotes str = prim__strSubstr 1 (lengthInt - 2) str

1
tests/Main.idr
View File

@ -43,6 +43,7 @@ idrisTests
-- Coverage checking
"coverage001", "coverage002", "coverage003", "coverage004",
"coverage005", "coverage006", "coverage007", "coverage008",
"coverage009",
-- Error messages
"error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009", "error010",

3
tests/idris2/coverage009/expected Normal file
View File

@ -0,0 +1,3 @@
1/1: Building unreachable (unreachable.idr)
unreachable.idr:3:1--3:18:Warning: unreachable clause: foo Nothing True
unreachable.idr:5:1--5:19:Warning: unreachable clause: foo Nothing False

3
tests/idris2/coverage009/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check unreachable.idr
rm -rf build

5
tests/idris2/coverage009/unreachable.idr Normal file
View File

@ -0,0 +1,5 @@
foo : Maybe Int -> Bool -> Int
foo Nothing _ = 42
foo Nothing True = 94
foo (Just x) _ = x
foo Nothing False = 42