3e4752f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix name decoration

Not separating the name from the index in MNs means that it's possible to generate duplicate names in code generation! Fixes #3719

commit3e4752fc9fa64785420479c85a7066a5ea00d785 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 31 Mar 2017, 14:16 (10 years ago) parent4c0acf6

8 files changed+18−18

compare with master

unifiedsplit

rts/idris_main.c+1−1 src/IRTS/CodegenC.hs+2−2 src/Idris/Core/TT.hs+2−2 test/dsl001/expected+4−4 test/dsl001/input+1−1 test/interactive010/expected+2−2 test/pkg001/expected+1−1 test/proof009/expected+5−5

rts/idris_main.c+1−1

@@ -55,7 +55,7 @@ int main(int argc, char **argv) {

5555 init_nullaries();

5656 init_signals();

5757

58− _idris__123_runMain0_125_(vm, NULL);

58+ _idris__123_runMain_95_0_125_(vm, NULL);

5959

6060#ifdef IDRIS_DEBUG

6161 if (opts.show_summary) {

src/IRTS/CodegenC.hs+2−2

@@ -841,14 +841,14 @@ genWrapper (desc, tag) = ret ++ " " ++ wrapperName tag ++ "(" ++

841841 indent 1 ++ "STOREOLD;\n" ++

842842 indent 1 ++ "BASETOP(0);\n" ++

843843 indent 1 ++ "ADDTOP(2);\n" ++

844− indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" ++

844+ indent 1 ++ "CALL(_idris__123_APPLY_95_0_125_);\n" ++

845845 indent 1 ++ "TOP(0)=REG1;\n" ++

846846 applyArgs (y:xs)

847847 applyArgs x = push 1 x ++

848848 indent 1 ++ "STOREOLD;\n" ++

849849 indent 1 ++ "BASETOP(0);\n" ++

850850 indent 1 ++ "ADDTOP(" ++ show (length x + 1) ++ ");\n" ++

851− indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n"

851+ indent 1 ++ "CALL(_idris__123_APPLY_95_0_125_);\n"

852852 renderArgs [] = "void"

853853 renderArgs [((s, _), n)] = s ++ " a" ++ (show n)

854854 renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++

src/Idris/Core/TT.hs+2−2

@@ -538,7 +538,7 @@ instance Show Name where

538538 show (UN n) = str n

539539 show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n

540540 show (MN _ u) | u == txt "underscore" = "_"

541− show (MN i s) = "{" ++ str s ++ show i ++ "}"

541+ show (MN i s) = "{" ++ str s ++ "_" ++ show i ++ "}"

542542 show (SN s) = show s

543543 show (SymRef i) = "##symbol" ++ show i ++ "##"

544544

@@ -559,7 +559,7 @@ showCG :: Name -> String

559559showCG (UN n) = T.unpack n

560560showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n

561561showCG (MN _ u) | u == txt "underscore" = "_"

562−showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

562+showCG (MN i s) = "{" ++ T.unpack s ++ "_" ++ show i ++ "}"

563563showCG (SN s) = showCG' s

564564 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

565565 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i

test/dsl001/expected+4−4

@@ -1,13 +1,13 @@

1124

2212

33testFac : Int

4−testFac = PE_interp_e04a79ff [] (PE_fromInteger_d6648df 4)

5−PE_interp_e04a79ff : Env G -> Int -> Int

6−PE_interp_e04a79ff (3arg) = \x =>

4+testFac = PE_interp_9b251b28 [] (PE_fromInteger_d6648df 4)

5+PE_interp_9b251b28 : Env G -> Int -> Int

6+PE_interp_9b251b28 (3arg) = \x =>

77 ifThenElse (PE_==_ba2f651f x

88 (PE_fromInteger_d6648df 0))

99 (Delay (PE_fromInteger_d6648df 1))

10− (Delay (PE_*_ba2f651f (PE_interp_e04a79ff (x ::

10+ (Delay (PE_*_ba2f651f (PE_interp_9b251b28 (x ::

1111 (3arg))

1212 (PE_-_ba2f651f x

1313 (PE_fromInteger_d6648df 1)))

test/dsl001/input+1−1

@@ -1,2 +1,2 @@

11:printdef testFac

2−:printdef PE_interp_e04a79ff

2+:printdef PE_interp_9b251b28

test/interactive010/expected+2−2

@@ -4,9 +4,9 @@ Prelude.Strings.(++) : String -> String -> String

44Usage is :doc <functionname>

55Usage is :wc <functionname>

66Usage is :printdef <functionname>

7−pat {ty503} : Type toplevel.u. pat {__interface504} : Prelude.Interfaces.Fractional {ty503}. Prelude.Interfaces./ {ty503} {__interface504}

7+pat {ty_503} : Type toplevel.u. pat {__interface_504} : Prelude.Interfaces.Fractional {ty_503}. Prelude.Interfaces./ {ty_503} {__interface_504}

9− : pty {ty503} : Type toplevel.u. pty {__interface504} : Prelude.Interfaces.Fractional {ty503}. {ty503} -> {ty503} -> {ty503}

9+ : pty {ty_503} : Type toplevel.u. pty {__interface_504} : Prelude.Interfaces.Fractional {ty_503}. {ty_503} -> {ty_503} -> {ty_503}

1010(input):1:1: error: expected: ":",

1111 dependent type signature,

1212 end of input

test/pkg001/expected+1−1

@@ -11,7 +11,7 @@ The options need removing are:

1111

1212

1313

14−Elaborating {__Infer0}

14+Elaborating {__Infer_0}

1515builtin

1616Elaborating =

1717builtin

test/proof009/expected+5−5

@@ -2,20 +2,20 @@ Warning: this interactive prover is deprecated and will be removed in a future r

44---------- Goal: ----------

5−{hole0} : Int -> Int -> Int

5+{hole_0} : Int -> Int -> Int

66-Main.arhs> ---------- Other goals: ----------

7−{hole0}

7+{hole_0}

88---------- Assumptions: ----------

99 x : Int

1010---------- Goal: ----------

11−{hole1} : Int -> Int

11+{hole_1} : Int -> Int

1212-Main.arhs> ---------- Other goals: ----------

13−{hole1},{hole0}

13+{hole_1},{hole_0}

1414---------- Assumptions: ----------

1515 x : Int

1616 y : Int

1717---------- Goal: ----------

18−{hole2} : Int

18+{hole_2} : Int

1919-Main.arhs> arhs: No more goals.

2020-Main.arhs> Proof completed!

2121Main.arhs = proof