git.iko.soy/Idris-dev
on master help sign in
Fix name decoration
3e4752fEdwin Brady
rts/idris_main.c+1−1
compare with master
unifiedsplit
@@ -55,7 +55,7 @@ int main(int argc, char **argv) {
55 init_nullaries();
55 init_nullaries();
56 init_signals();
56 init_signals();
57
57
58− _idris__123_runMain0_125_(vm, NULL);
58+ _idris__123_runMain_95_0_125_(vm, NULL);
59
59
60#ifdef IDRIS_DEBUG
60#ifdef IDRIS_DEBUG
61 if (opts.show_summary) {
61 if (opts.show_summary) {
src/IRTS/CodegenC.hs+2−2
@@ -841,14 +841,14 @@ genWrapper (desc, tag) = ret ++ " " ++ wrapperName tag ++ "(" ++
841 indent 1 ++ "STOREOLD;\n" ++
841 indent 1 ++ "STOREOLD;\n" ++
842 indent 1 ++ "BASETOP(0);\n" ++
842 indent 1 ++ "BASETOP(0);\n" ++
843 indent 1 ++ "ADDTOP(2);\n" ++
843 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" ++
845 indent 1 ++ "TOP(0)=REG1;\n" ++
845 indent 1 ++ "TOP(0)=REG1;\n" ++
846 applyArgs (y:xs)
846 applyArgs (y:xs)
847 applyArgs x = push 1 x ++
847 applyArgs x = push 1 x ++
848 indent 1 ++ "STOREOLD;\n" ++
848 indent 1 ++ "STOREOLD;\n" ++
849 indent 1 ++ "BASETOP(0);\n" ++
849 indent 1 ++ "BASETOP(0);\n" ++
850 indent 1 ++ "ADDTOP(" ++ show (length x + 1) ++ ");\n" ++
850 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"
852 renderArgs [] = "void"
852 renderArgs [] = "void"
853 renderArgs [((s, _), n)] = s ++ " a" ++ (show n)
853 renderArgs [((s, _), n)] = s ++ " a" ++ (show n)
854 renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++
854 renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++
src/Idris/Core/TT.hs+2−2
@@ -538,7 +538,7 @@ instance Show Name where
538 show (UN n) = str n
538 show (UN n) = str n
539 show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n
539 show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n
540 show (MN _ u) | u == txt "underscore" = "_"
540 show (MN _ u) | u == txt "underscore" = "_"
541− show (MN i s) = "{" ++ str s ++ show i ++ "}"
541+ show (MN i s) = "{" ++ str s ++ "_" ++ show i ++ "}"
542 show (SN s) = show s
542 show (SN s) = show s
543 show (SymRef i) = "##symbol" ++ show i ++ "##"
543 show (SymRef i) = "##symbol" ++ show i ++ "##"
544
544
@@ -559,7 +559,7 @@ showCG :: Name -> String
559showCG (UN n) = T.unpack n
559showCG (UN n) = T.unpack n
560showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n
560showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n
561showCG (MN _ u) | u == txt "underscore" = "_"
561showCG (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 ++ "}"
563showCG (SN s) = showCG' s
563showCG (SN s) = showCG' s
564 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i
564 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i
565 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i
565 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i
test/dsl001/expected+4−4
@@ -1,13 +1,13 @@
124
124
212
212
3testFac : Int
3testFac : Int
4−testFac = PE_interp_e04a79ff [] (PE_fromInteger_d6648df 4)
4+testFac = PE_interp_9b251b28 [] (PE_fromInteger_d6648df 4)
5−PE_interp_e04a79ff : Env G -> Int -> Int
5+PE_interp_9b251b28 : Env G -> Int -> Int
6−PE_interp_e04a79ff (3arg) = \x =>
6+PE_interp_9b251b28 (3arg) = \x =>
7 ifThenElse (PE_==_ba2f651f x
7 ifThenElse (PE_==_ba2f651f x
8 (PE_fromInteger_d6648df 0))
8 (PE_fromInteger_d6648df 0))
9 (Delay (PE_fromInteger_d6648df 1))
9 (Delay (PE_fromInteger_d6648df 1))
10− (Delay (PE_*_ba2f651f (PE_interp_e04a79ff (x ::
10+ (Delay (PE_*_ba2f651f (PE_interp_9b251b28 (x ::
11 (3arg))
11 (3arg))
12 (PE_-_ba2f651f x
12 (PE_-_ba2f651f x
13 (PE_fromInteger_d6648df 1)))
13 (PE_fromInteger_d6648df 1)))
test/dsl001/input+1−1
@@ -1,2 +1,2 @@
1:printdef testFac
1: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
4Usage is :doc <functionname>
4Usage is :doc <functionname>
5Usage is :wc <functionname>
5Usage is :wc <functionname>
6Usage is :printdef <functionname>
6Usage 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}
8
8
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}
10(input):1:1: error: expected: ":",
10(input):1:1: error: expected: ":",
11 dependent type signature,
11 dependent type signature,
12 end of input
12 end of input
test/pkg001/expected+1−1
@@ -11,7 +11,7 @@ The options need removing are:
11
11
12
12
13
13
14−Elaborating {__Infer0}
14+Elaborating {__Infer_0}
15builtin
15builtin
16Elaborating =
16Elaborating =
17builtin
17builtin
test/proof009/expected+5−5
@@ -2,20 +2,20 @@ Warning: this interactive prover is deprecated and will be removed in a future r
2
2
3
3
4---------- Goal: ----------
4---------- Goal: ----------
5−{hole0} : Int -> Int -> Int
5+{hole_0} : Int -> Int -> Int
6-Main.arhs> ---------- Other goals: ----------
6-Main.arhs> ---------- Other goals: ----------
7−{hole0}
7+{hole_0}
8---------- Assumptions: ----------
8---------- Assumptions: ----------
9 x : Int
9 x : Int
10---------- Goal: ----------
10---------- Goal: ----------
11−{hole1} : Int -> Int
11+{hole_1} : Int -> Int
12-Main.arhs> ---------- Other goals: ----------
12-Main.arhs> ---------- Other goals: ----------
13−{hole1},{hole0}
13+{hole_1},{hole_0}
14---------- Assumptions: ----------
14---------- Assumptions: ----------
15 x : Int
15 x : Int
16 y : Int
16 y : Int
17---------- Goal: ----------
17---------- Goal: ----------
18−{hole2} : Int
18+{hole_2} : Int
19-Main.arhs> arhs: No more goals.
19-Main.arhs> arhs: No more goals.
20-Main.arhs> Proof completed!
20-Main.arhs> Proof completed!
21Main.arhs = proof
21Main.arhs = proof