mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
This commit is contained in:
parent
419a440dad
commit
c04404a95b
src/Idris
tests/idris2/error/perror030
@ -979,9 +979,6 @@ mutual
|
|||||||
uds' <- traverse (desugarDecl ps) uds
|
uds' <- traverse (desugarDecl ps) uds
|
||||||
update Syn { usingImpl := oldu }
|
update Syn { usingImpl := oldu }
|
||||||
pure (concat uds')
|
pure (concat uds')
|
||||||
desugarDecl ps (PReflect fc tm)
|
|
||||||
= throw (GenericMsg fc "Reflection not implemented yet")
|
|
||||||
-- pure [IReflect fc !(desugar AnyExpr ps tm)]
|
|
||||||
desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
|
desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
|
||||||
= do addDocString tn doc
|
= do addDocString tn doc
|
||||||
let paramNames = map fst params
|
let paramNames = map fst params
|
||||||
|
@ -1835,14 +1835,8 @@ fixDecl fname indents
|
|||||||
|
|
||||||
directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl
|
directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl
|
||||||
directiveDecl fname indents
|
directiveDecl fname indents
|
||||||
= do b <- bounds ((do d <- directive fname indents
|
= do b <- bounds (directive fname indents)
|
||||||
pure (\fc : FC => PDirective fc d))
|
pure (PDirective (boundToFC fname b) b.val)
|
||||||
<|>
|
|
||||||
(do decoratedPragma fname "runElab"
|
|
||||||
tm <- expr pdef fname indents
|
|
||||||
atEnd indents
|
|
||||||
pure (\fc : FC => PReflect fc tm)))
|
|
||||||
pure (b.val (boundToFC fname b))
|
|
||||||
|
|
||||||
-- Declared at the top
|
-- Declared at the top
|
||||||
-- topDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
|
-- topDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
|
||||||
@ -1855,6 +1849,8 @@ topDecl fname indents
|
|||||||
pure [d]
|
pure [d]
|
||||||
<|> do ds <- claims fname indents
|
<|> do ds <- claims fname indents
|
||||||
pure (forget ds)
|
pure (forget ds)
|
||||||
|
<|> do d <- directiveDecl fname indents
|
||||||
|
pure [d]
|
||||||
<|> do d <- implDecl fname indents
|
<|> do d <- implDecl fname indents
|
||||||
pure [d]
|
pure [d]
|
||||||
<|> do d <- definition fname indents
|
<|> do d <- definition fname indents
|
||||||
@ -1880,8 +1876,6 @@ topDecl fname indents
|
|||||||
pure [d]
|
pure [d]
|
||||||
<|> do d <- transformDecl fname indents
|
<|> do d <- transformDecl fname indents
|
||||||
pure [d]
|
pure [d]
|
||||||
<|> do d <- directiveDecl fname indents
|
|
||||||
pure [d]
|
|
||||||
<|> do dstr <- bounds (terminal "Expected CG directive"
|
<|> do dstr <- bounds (terminal "Expected CG directive"
|
||||||
(\case
|
(\case
|
||||||
CGDirective d => Just d
|
CGDirective d => Just d
|
||||||
|
@ -434,7 +434,6 @@ mutual
|
|||||||
List (PDecl' nm) -> PDecl' nm
|
List (PDecl' nm) -> PDecl' nm
|
||||||
PUsing : FC -> List (Maybe Name, PTerm' nm) ->
|
PUsing : FC -> List (Maybe Name, PTerm' nm) ->
|
||||||
List (PDecl' nm) -> PDecl' nm
|
List (PDecl' nm) -> PDecl' nm
|
||||||
PReflect : FC -> PTerm' nm -> PDecl' nm
|
|
||||||
PInterface : FC ->
|
PInterface : FC ->
|
||||||
Visibility ->
|
Visibility ->
|
||||||
(constraints : List (Maybe Name, PTerm' nm)) ->
|
(constraints : List (Maybe Name, PTerm' nm)) ->
|
||||||
@ -482,7 +481,6 @@ mutual
|
|||||||
getPDeclLoc (PData fc _ _ _ _) = fc
|
getPDeclLoc (PData fc _ _ _ _) = fc
|
||||||
getPDeclLoc (PParameters fc _ _) = fc
|
getPDeclLoc (PParameters fc _ _) = fc
|
||||||
getPDeclLoc (PUsing fc _ _) = fc
|
getPDeclLoc (PUsing fc _ _) = fc
|
||||||
getPDeclLoc (PReflect fc _) = fc
|
|
||||||
getPDeclLoc (PInterface fc _ _ _ _ _ _ _ _) = fc
|
getPDeclLoc (PInterface fc _ _ _ _ _ _ _ _) = fc
|
||||||
getPDeclLoc (PImplementation fc _ _ _ _ _ _ _ _ _ _) = fc
|
getPDeclLoc (PImplementation fc _ _ _ _ _ _ _ _ _ _) = fc
|
||||||
getPDeclLoc (PRecord fc _ _ _ _) = fc
|
getPDeclLoc (PRecord fc _ _ _ _) = fc
|
||||||
@ -1055,7 +1053,6 @@ Show PDecl where
|
|||||||
show (PData{}) = "PData"
|
show (PData{}) = "PData"
|
||||||
show (PParameters{}) = "PParameters"
|
show (PParameters{}) = "PParameters"
|
||||||
show (PUsing{}) = "PUsing"
|
show (PUsing{}) = "PUsing"
|
||||||
show (PReflect{}) = "PReflect"
|
|
||||||
show (PInterface{}) = "PInterface"
|
show (PInterface{}) = "PInterface"
|
||||||
show (PImplementation{}) = "PImplementation"
|
show (PImplementation{}) = "PImplementation"
|
||||||
show (PRecord{}) = "PRecord"
|
show (PRecord{}) = "PRecord"
|
||||||
|
@ -240,7 +240,6 @@ mapPTermM f = goPTerm where
|
|||||||
goPDecl (PUsing fc mnts ps) =
|
goPDecl (PUsing fc mnts ps) =
|
||||||
PUsing fc <$> goPairedPTerms mnts
|
PUsing fc <$> goPairedPTerms mnts
|
||||||
<*> goPDecls ps
|
<*> goPDecls ps
|
||||||
goPDecl (PReflect fc t) = PReflect fc <$> goPTerm t
|
|
||||||
goPDecl (PInterface fc v mnts n doc nrts ns mn ps) =
|
goPDecl (PInterface fc v mnts n doc nrts ns mn ps) =
|
||||||
PInterface fc v <$> goPairedPTerms mnts
|
PInterface fc v <$> goPairedPTerms mnts
|
||||||
<*> pure n
|
<*> pure n
|
||||||
@ -523,7 +522,6 @@ mapPTerm f = goPTerm where
|
|||||||
= PParameters fc (go4TupledPTerms nts) (goPDecl <$> ps)
|
= PParameters fc (go4TupledPTerms nts) (goPDecl <$> ps)
|
||||||
goPDecl (PUsing fc mnts ps)
|
goPDecl (PUsing fc mnts ps)
|
||||||
= PUsing fc (goPairedPTerms mnts) (goPDecl <$> ps)
|
= PUsing fc (goPairedPTerms mnts) (goPDecl <$> ps)
|
||||||
goPDecl (PReflect fc t) = PReflect fc $ goPTerm t
|
|
||||||
goPDecl (PInterface fc v mnts n doc nrts ns mn ps)
|
goPDecl (PInterface fc v mnts n doc nrts ns mn ps)
|
||||||
= PInterface fc v (goPairedPTerms mnts) n doc (go3TupledPTerms nrts) ns mn (goPDecl <$> ps)
|
= PInterface fc v (goPairedPTerms mnts) n doc (go3TupledPTerms nrts) ns mn (goPDecl <$> ps)
|
||||||
goPDecl (PImplementation fc v opts p is cs n ts mn ns mps)
|
goPDecl (PImplementation fc v opts p is cs n ts mn ns mps)
|
||||||
|
7
tests/idris2/error/perror030/LoggingParse.idr
Normal file
7
tests/idris2/error/perror030/LoggingParse.idr
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
import Data.Vect
|
||||||
|
|
||||||
|
%logging "elab" 1
|
||||||
|
|
||||||
|
[Named] {n : Nat} -> Show (Vect n a) where
|
||||||
|
show x = "whatever"
|
||||||
|
|
1
tests/idris2/error/perror030/expected
Normal file
1
tests/idris2/error/perror030/expected
Normal file
@ -0,0 +1 @@
|
|||||||
|
1/1: Building LoggingParse (LoggingParse.idr)
|
3
tests/idris2/error/perror030/run
Normal file
3
tests/idris2/error/perror030/run
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
. ../../../testutils.sh
|
||||||
|
|
||||||
|
check LoggingParse.idr
|
Loading…
Reference in New Issue
Block a user