git.iko.soy/Idris-dev
on master help sign in
Change internal names of pattern bindings

Use convention that names beginning __ aren't displayed - we can't use these names anyway.

commit03b99805decd5dcea351d64f07e126db0137da99 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 29 Nov 2015, 21:23 (11 years ago) parent180bac5
2 files changed+4−4
compare with master
unifiedsplit
libs/base/System.idr+1−1 src/Idris/DSL.hs+3−3
libs/base/System.idr+1−1
@@ -56,7 +56,7 @@ getEnvironment = getAllPairs 0 []
5656exit : Int -> IO ()
5757exit code = foreign FFI_C "exit" (Int -> IO ()) code
5858
59−||| Get the Unix time
59+||| Get the numbers of sections since 1st January 1970, 00:00 UTC
6060time : IO Integer
6161time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
6262 return t
src/Idris/DSL.hs+3−3
@@ -98,8 +98,8 @@ expandSugar dsl (PDoBlock ds)
9898 block b (DoBind fc n nfc tm : rest)
9999 = PApp fc b [pexp tm, pexp (PLam fc n nfc Placeholder (block b rest))]
100100 block b (DoBindP fc p tm alts : rest)
101− = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "bpat") NoFC Placeholder
102− (PCase fc (PRef fc [] (sMN 0 "bpat"))
101+ = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "__bpat") NoFC Placeholder
102+ (PCase fc (PRef fc [] (sMN 0 "__bpat"))
103103 ((p, block b rest) : alts)))]
104104 block b (DoLet fc n nfc ty tm : rest)
105105 = PLet fc n nfc ty tm (block b rest)
@@ -108,7 +108,7 @@ expandSugar dsl (PDoBlock ds)
108108 block b (DoExp fc tm : rest)
109109 = PApp fc b
110110 [pexp tm,
111− pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]
111+ pexp (PLam fc (sMN 0 "__bindx") NoFC (mkTy tm) (block b rest))]
112112 where mkTy (PCase _ _ _) = PRef fc [] unitTy
113113 mkTy (PMetavar _ _) = PRef fc [] unitTy
114114 mkTy _ = Placeholder