mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-23 14:18:02 +03:00
[ fix ] Data and Type Constructor tags for :di (#3395)
* [ fix ] Data and Type Constructor tags for :di * [ doc ] update changelog * [ test ] add a test case * [ test ] fix test output in basic039
This commit is contained in:
parent
536c7bff6f
commit
f840d1b771
@ -42,6 +42,7 @@ This CHANGELOG describes the history of already-released versions. Please see [C
|
||||
and `Force`.
|
||||
* Adds `--no-cse` command-line option to disable common subexpression elimination
|
||||
for code generation debugging.
|
||||
* Fixes a confusion between data and type constructors in the `:di` command.
|
||||
|
||||
### Backend changes
|
||||
|
||||
|
@ -125,7 +125,7 @@ prettyCDef (MkFun args exp) = reAnnotate Syntax $
|
||||
keyword "\\" <++> concatWith (\ x, y => x <+> keyword "," <++> y) (map prettyName args)
|
||||
<++> fatArrow <++> prettyCExp exp
|
||||
prettyCDef (MkCon mtag arity nt)
|
||||
= vcat $ header (maybe "Data" (const "Type") mtag <++> "Constructor") :: map (indent 2)
|
||||
= vcat $ header (maybe "Type" (const "Data") mtag <++> "Constructor") :: map (indent 2)
|
||||
( maybe [] (\ tag => ["tag:" <++> byShow tag]) mtag ++
|
||||
[ "arity:" <++> byShow arity ] ++
|
||||
maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
|
||||
|
@ -4,7 +4,7 @@ Data constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
newtype by: (False, 0)
|
||||
Compiled: Type Constructor:
|
||||
Compiled: Data Constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
newtype by: 0
|
||||
@ -13,7 +13,7 @@ Main> Main.MkBar
|
||||
Data constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
Compiled: Type Constructor:
|
||||
Compiled: Data Constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
Flags: contype [record]
|
||||
|
18
tests/idris2/repl/repl007/expected
Normal file
18
tests/idris2/repl/repl007/expected
Normal file
@ -0,0 +1,18 @@
|
||||
Main> Prelude.Basics.Bool
|
||||
Type constructor:
|
||||
tag: 100
|
||||
arity: 0
|
||||
parameter positions: []
|
||||
constructors: Prelude.Basics.False, Prelude.Basics.True
|
||||
Compiled: Type Constructor:
|
||||
arity: 0
|
||||
Main> Prelude.Basics.True
|
||||
Data constructor:
|
||||
tag: 1
|
||||
arity: 0
|
||||
Compiled: Data Constructor:
|
||||
tag: 1
|
||||
arity: 0
|
||||
Flags: contype [enum 2]
|
||||
Main>
|
||||
Bye for now!
|
2
tests/idris2/repl/repl007/input
Normal file
2
tests/idris2/repl/repl007/input
Normal file
@ -0,0 +1,2 @@
|
||||
:di Bool
|
||||
:di True
|
3
tests/idris2/repl/repl007/run
Executable file
3
tests/idris2/repl/repl007/run
Executable file
@ -0,0 +1,3 @@
|
||||
. ../../../testutils.sh
|
||||
|
||||
idris2 < input
|
Loading…
Reference in New Issue
Block a user