46e894d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use Data.Text for variable names

An experiment: it appears to reduce memory usage and speed things up slightly, but in its current form breaks type providers and :x. I am stuck on working out what's wrong, so if anyone can see what the problem is, please do let me know and/or fix it!

commit46e894d386d57e723ee63cb50bb2e41e59ad4d97 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Jan 2014, 01:53 (13 years ago) parent66ec833

41 files changed+675−568

compare with master

unifiedsplit

src/IRTS/CodegenC.hs+1−1 src/IRTS/CodegenJava.hs+5−5 src/IRTS/CodegenJavaScript.hs+12−10 src/IRTS/Compiler.hs+34−31 src/IRTS/Defunctionalise.hs+14−14 src/IRTS/Java/Mangling.hs+3−3 src/IRTS/Lang.hs+1−1 src/IRTS/Simplified.hs+1−1 src/Idris/AbsSyntax.hs+34−31 src/Idris/AbsSyntaxTree.hs+21−19 src/Idris/CaseSplit.hs+13−12 src/Idris/Completion.hs+3−3 src/Idris/Core/CaseTree.hs+5−5 src/Idris/Core/Elaborate.hs+9−9 src/Idris/Core/Evaluate.hs+14−14 src/Idris/Core/Execute.hs+57−33 src/Idris/Core/ProofState.hs+7−7 src/Idris/Core/TT.hs+60−29 src/Idris/Core/Typecheck.hs+1−1 src/Idris/Core/Unify.hs+1−1 src/Idris/Coverage.hs+12−9 src/Idris/DSL.hs+4−4 src/Idris/DataOpts.hs+26−15 src/Idris/Delaborate.hs+9−9 src/Idris/Docs.hs+1−1 src/Idris/ElabDecls.hs+83−75 src/Idris/ElabTerm.hs+103−99 src/Idris/IBC.hs+8−1 src/Idris/ParseData.hs+1−1 src/Idris/ParseExpr.hs+26−26 src/Idris/ParseHelpers.hs+2−2 src/Idris/ParseOps.hs+5−5 src/Idris/Parser.hs+9−9 src/Idris/PartialEval.hs+2−2 src/Idris/Primitives.hs+50−50 src/Idris/Prover.hs+2−1 src/Idris/Providers.hs+14−7 src/Idris/REPL.hs+15−15 src/Idris/Transforms.hs+3−3 src/Pkg/PParser.hs+1−1 src/Pkg/Package.hs+3−3

src/IRTS/CodegenC.hs+1−1

@@ -444,7 +444,7 @@ doOp v LStdIn [] = v ++ "MKPTR(vm, stdin)"

444444doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)"

445445doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

446446

447−doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

447+doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

448448doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

449449doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

450450doOp v LNullPtr [] = v ++ "MKPTR(vm, NULL)"

src/IRTS/CodegenJava.hs+5−5

@@ -369,13 +369,13 @@ addMainMethod decls

369369 | otherwise = decls

370370 where

371371 findMain ((MemberDecl (MemberClassDecl (ClassDecl _ name _ _ _ (ClassBody body)))):_)

372− | name == mangle' (UN "Main") = findMainMethod body

372+ | name == mangle' (sUN "Main") = findMainMethod body

373373 findMain (_:decls) = findMain decls

374374 findMain [] = False

375375

376− innerMainMethod = (either error id $ mangle (UN "main"))

376+ innerMainMethod = (either error id $ mangle (sUN "main"))

377377 findMainMethod ((MemberDecl (MethodDecl _ _ _ name [] _ _)):_)

378− | name == mangle' (UN "main") = True

378+ | name == mangle' (sUN "main") = True

379379 findMainMethod (_:decls) = findMainMethod decls

380380 findMainMethod [] = False

381381

@@ -390,7 +390,7 @@ mkMainMethod =

390390 $ call "idris_initArgs" [ (threadType ~> "currentThread") []

391391 , jConst "args"

392392 ]

393− , BlockStmt . ExpStmt $ call (mangle' (MN 0 "runMain")) []

393+ , BlockStmt . ExpStmt $ call (mangle' (sMN 0 "runMain")) []

394394 ]

395395

396396-----------------------------------------------------------------------

@@ -749,6 +749,6 @@ mkPrimitiveFunction op args =

749749

750750mkThread :: LVar -> CodeGeneration Exp

751751mkThread arg =

752− (\ closure -> (closure ~> "fork") []) <$> mkMethodCallClosure (MN 0 "EVAL") [arg]

752+ (\ closure -> (closure ~> "fork") []) <$> mkMethodCallClosure (sMN 0 "EVAL") [arg]

753753

754754

src/IRTS/CodegenJavaScript.hs+12−10

@@ -606,7 +606,7 @@ codegenJavaScript target definitions filename outputType = do

606606 mainFun = jsTailcall $ jsCall runMain []

607607

608608 runMain :: String

609− runMain = idrNamespace ++ translateName (MN 0 "runMain")

609+ runMain = idrNamespace ++ translateName (sMN 0 "runMain")

610610

611611 invokeLoop :: String

612612 invokeLoop = compileJS $ jsCall "main" []

@@ -671,15 +671,15 @@ translateIdentifier =

671671

672672translateNamespace :: Name -> String

673673translateNamespace (UN _) = idrNamespace

674−translateNamespace (NS _ ns) = idrNamespace ++ concatMap translateIdentifier ns

674+translateNamespace (NS _ ns) = idrNamespace ++ concatMap (translateIdentifier . str) ns

675675translateNamespace (MN _ _) = idrNamespace

676676translateNamespace (SN name) = idrNamespace ++ translateSpecialName name

677677translateNamespace NErased = idrNamespace

678678

679679translateName :: Name -> String

680−translateName (UN name) = 'u' : translateIdentifier name

680+translateName (UN name) = 'u' : translateIdentifier (str name)

681681translateName (NS name _) = 'n' : translateName name

682−translateName (MN i name) = 'm' : translateIdentifier name ++ show i

682+translateName (MN i name) = 'm' : translateIdentifier (str name) ++ show i

683683translateName (SN name) = 's' : translateSpecialName name

684684translateName NErased = "e"

685685

@@ -688,9 +688,9 @@ translateSpecialName name

688688 | WhereN i m n <- name =

689689 'w' : translateName m ++ translateName n ++ show i

690690 | InstanceN n s <- name =

691− 'i' : translateName n ++ concatMap translateIdentifier s

691+ 'i' : translateName n ++ concatMap (translateIdentifier . str) s

692692 | ParentN n s <- name =

693− 'p' : translateName n ++ translateIdentifier s

693+ 'p' : translateName n ++ translateIdentifier (str s)

694694 | MethodN n <- name =

695695 'm' : translateName n

696696 | CaseN n <- name =

@@ -714,9 +714,10 @@ translateConstant c =

714714

715715translateDeclaration :: (String, SDecl) -> JS

716716translateDeclaration (path, SFun name params stackSize body)

717− | (MN _ "APPLY") <- name

717+ | (MN _ ap) <- name

718718 , (SLet var val next) <- body

719− , (SChkCase cvar cases) <- next =

719+ , (SChkCase cvar cases) <- next

720+ , ap == txt "APPLY" =

720721 let lvar = translateVariableName var

721722 lookup = "[" ++ lvar ++ ".tag](fn0,arg0," ++ lvar ++ ")" in

722723 JSSeq [ lookupTable [(var, "chk")] var cases

@@ -735,8 +736,9 @@ translateDeclaration (path, SFun name params stackSize body)

735736 )

736737 ]

737738

738− | (MN _ "EVAL") <- name

739− , (SChkCase var cases) <- body =

739+ | (MN _ ev) <- name

740+ , (SChkCase var cases) <- body

741+ , ev == txt "EVAL" =

740742 JSSeq [ lookupTable [] var cases

741743 , jsDecl $ JSFunction ["arg0"] (JSReturn $

742744 JSTernary (

src/IRTS/Compiler.hs+34−31

@@ -40,7 +40,7 @@ compile codegen f tm

4040 = do checkMVs

4141 let tmnames = namesUsed (STerm tm)

4242 usedIn <- mapM (allNames []) tmnames

43− let used = [UN "prim__subBigInt", UN "prim__addBigInt"] : usedIn

43+ let used = [sUN "prim__subBigInt", sUN "prim__addBigInt"] : usedIn

4444 defsIn <- mkDecls tm (concat used)

4545 findUnusedArgs (concat used)

4646 maindef <- irMain tm

@@ -49,7 +49,7 @@ compile codegen f tm

4949 flags <- getFlags codegen

5050 hdrs <- getHdrs codegen

5151 impdirs <- allImportDirs

52− let defs = defsIn ++ [(MN 0 "runMain", maindef)]

52+ let defs = defsIn ++ [(sMN 0 "runMain", maindef)]

5353 -- iputStrLn $ showSep "\n" (map show defs)

5454 let (nexttag, tagged) = addTags 65536 (liftAll defs)

5555 let ctxtIn = addAlist tagged emptyContext

@@ -108,7 +108,7 @@ compile codegen f tm

108108

109109irMain :: TT Name -> Idris LDecl

110110irMain tm = do i <- ir tm

111− return $ LFun [] (MN 0 "runMain") [] (LForce i)

111+ return $ LFun [] (sMN 0 "runMain") [] (LForce i)

112112

113113mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

114114mkDecls t used

@@ -137,7 +137,7 @@ build (n, d)

137137 = do i <- getIState

138138 case lookup n (idris_scprims i) of

139139 Just (ar, op) ->

140− let args = map (\x -> MN x "op") [0..] in

140+ let args = map (\x -> sMN x "op") [0..] in

141141 return (n, (LFun [] n (take ar args)

142142 (LOp op (map (LV . Glob) (take ar args)))))

143143 _ -> do def <- mkLDecl n d

@@ -168,40 +168,38 @@ mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)

168168instance ToIR (TT Name) where

169169 ir tm = ir' [] tm where

170170 ir' env tm@(App f a)

171− | (P _ (UN "mkForeignPrim") _, args) <- unApply tm

171+ | (P _ (UN m) _, args) <- unApply tm,

172+ m == txt "mkForeignPrim"

172173 = doForeign env args

173− | (P _ (UN "unsafePerformPrimIO") _, [_, arg]) <- unApply tm

174+ | (P _ (UN u) _, [_, arg]) <- unApply tm,

175+ u == txt "unsafePerformPrimIO"

174176 = ir' env arg

175177 -- TMP HACK - until we get inlining.

176− | (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm

178+ | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,

179+ r == txt "replace"

177180 = ir' env arg

178− | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

181+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

182+ l == txt "lazy"

179183 = do arg' <- ir' env arg

180184 return $ LLazyExp arg'

181− | (P _ (UN "assert_smaller") _, [_, _, _, arg]) <- unApply tm

185+ | (P _ (UN a) _, [_, _, _, arg]) <- unApply tm,

186+ a == txt "assert_smaller"

182187 = ir' env arg

183− | (P _ (UN "par") _, [_, arg]) <- unApply tm

188+ | (P _ (UN p) _, [_, arg]) <- unApply tm,

189+ p == txt "par"

184190 = do arg' <- ir' env arg

185191 return $ LOp LPar [LLazyExp arg']

186− | (P _ (UN "prim_fork") _, [arg]) <- unApply tm

192+ | (P _ (UN pf) _, [arg]) <- unApply tm,

193+ pf == txt "prim_fork"

187194 = do arg' <- ir' env arg

188195 return $ LOp LFork [LLazyExp arg']

189−-- | (P _ (UN "prim__IO") _, [v]) <- unApply tm

190−-- = do v' <- ir' env v

191−-- return v'

192−-- | (P _ (UN "prim_io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm

193−-- = do v' <- ir' env v

194−-- sc' <- ir' (n:env) sc

195−-- return (LLet n (LForce v') sc')

196−-- | (P _ (UN "prim_io_bind") _, [_,_,v,k]) <- unApply tm

197−-- = do v' <- ir' env v

198−-- k' <- ir' env k

199−-- return (LApp False k' [LForce v'])

200− | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm

196+ | (P _ (UN m) _, [_,size,t]) <- unApply tm,

197+ m == txt "malloc"

201198 = do size' <- ir' env size

202199 t' <- ir' env t

203200 return t' -- TODO $ malloc_ size' t'

204− | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm

201+ | (P _ (UN tm) _, [_,t]) <- unApply tm,

202+ tm == txt "trace_malloc"

205203 = do t' <- ir' env t

206204 return t' -- TODO

207205-- | (P _ (NS (UN "S") ["Nat", "Prelude"]) _, [k]) <- unApply tm

@@ -272,7 +270,7 @@ instance ToIR (TT Name) where

272270 (args ++ map (\n -> P Bound n undefined) extra)

273271 return $ LLam extra sc'

274272

275− satArgs n = map (\i -> MN i "sat") [1..n]

273+ satArgs n = map (\i -> sMN i "sat") [1..n]

276274

277275 buildApp env e [] = return e

278276 buildApp env e xs = do xs' <- mapM (ir' env) xs

@@ -300,10 +298,15 @@ getFTypes tm = case unApply tm of

300298 fmap (mkIty' ty :) (getFTypes xs)

301299 _ -> Nothing

302300

303−mkIty' (P _ (UN ty) _) = mkIty ty

304−mkIty' (App (P _ (UN "FIntT") _) (P _ (UN intTy) _)) = mkIntIty intTy

305−mkIty' (App (App (P _ (UN "FFunction") _) _) (App (P _ (UN "FAny") _) (App (P _ (UN "IO") _) _))) = FFunctionIO

306−mkIty' (App (App (P _ (UN "FFunction") _) _) _) = FFunction

301+mkIty' (P _ (UN ty) _) = mkIty (str ty)

302+mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

303+ | fi == txt "FIntT" = mkIntIty (str intTy)

304+mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

305+ | ff == txt "FFunction" && fa == txt "FAny" &&

306+ io == txt "IO"

307+ = FFunctionIO

308+mkIty' (App (App (P _ (UN ff) _) _) _)

309+ | ff == txt "FFunction" = FFunction

307310mkIty' _ = FAny

308311

309312-- would be better if these FInt types were evaluated at compile time

@@ -337,8 +340,8 @@ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

337340mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

338341mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

339342

340−zname = NS (UN "Z") ["Nat","Prelude"]

341−sname = NS (UN "S") ["Nat","Prelude"]

343+zname = sNS (sUN "Z") ["Nat","Prelude"]

344+sname = sNS (sUN "S") ["Nat","Prelude"]

342345

343346instance ToIR ([Name], SC) where

344347 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

src/IRTS/Defunctionalise.hs+14−14

@@ -143,7 +143,7 @@ addApps defs (n, LFun _ _ args e)

143143 = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)

144144

145145 chainAPPLY f [] = f

146− chainAPPLY f (a : as) = chainAPPLY (DApp False (MN 0 "APPLY") [f, a]) as

146+ chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as

147147

148148 -- if anything in the DExp is projected from, we'll need to evaluate it,

149149 -- but we only want to do it once, rather than every time we project.

@@ -171,7 +171,7 @@ addApps defs (n, LFun _ _ args e)

171171 needsEval x (DProj (DV (Glob x')) _) = x == x'

172172 needsEval x _ = False

173173

174−eEVAL x = DApp False (MN 0 "EVAL") [x]

174+eEVAL x = DApp False (sMN 0 "EVAL") [x]

175175

176176data EvalApply a = EvalCase (Name -> a)

177177 | ApplyCase a

@@ -198,26 +198,26 @@ mkApplyCase fname n ar

198198 (nm, n, ApplyCase (DConCase (-1) nm (take n (genArgs 0))

199199 (DApp False (mkUnderCon fname (ar - (n + 1)))

200200 (map (DV . Glob) (take n (genArgs 0) ++

201− [MN 0 "arg"])))))

201+ [sMN 0 "arg"])))))

202202 : mkApplyCase fname (n + 1) ar

203203

204204mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

205−mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"]

206− (mkBigCase (MN 0 "EVAL") 256 (DV (Glob (MN 0 "arg")))

205+mkEval xs = (sMN 0 "EVAL", DFun (sMN 0 "EVAL") [sMN 0 "arg"]

206+ (mkBigCase (sMN 0 "EVAL") 256 (DV (Glob (sMN 0 "arg")))

207207 (mapMaybe evalCase xs ++

208− [DDefaultCase (DV (Glob (MN 0 "arg")))])))

208+ [DDefaultCase (DV (Glob (sMN 0 "arg")))])))

209209 where

210− evalCase (n, t, EvalCase x) = Just (x (MN 0 "arg"))

210+ evalCase (n, t, EvalCase x) = Just (x (sMN 0 "arg"))

211211 evalCase _ = Nothing

212212

213213mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)

214−mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]

214+mkApply xs = (sMN 0 "APPLY", DFun (sMN 0 "APPLY") [sMN 0 "fn", sMN 0 "arg"]

215215 (case mapMaybe applyCase xs of

216216 [] -> DNothing

217217 cases ->

218− mkBigCase (MN 0 "APPLY") 256

219− (DApp False (MN 0 "EVAL")

220− [DV (Glob (MN 0 "fn"))])

218+ mkBigCase (sMN 0 "APPLY") 256

219+ (DApp False (sMN 0 "EVAL")

220+ [DV (Glob (sMN 0 "fn"))])

221221 (cases ++

222222 [DDefaultCase DNothing])))

223223 where

@@ -231,11 +231,11 @@ declare t xs = dec' t xs [] where

231231 dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, DConstructor n t ar) : acc)

232232

233233

234−genArgs i = MN i "P_c" : genArgs (i + 1)

234+genArgs i = sMN i "P_c" : genArgs (i + 1)

235235

236−mkFnCon n = MN 0 ("P_" ++ show n)

236+mkFnCon n = sMN 0 ("P_" ++ show n)

237237mkUnderCon n 0 = n

238−mkUnderCon n missing = MN missing ("U_" ++ show n)

238+mkUnderCon n missing = sMN missing ("U_" ++ show n)

239239

240240instance Show DExp where

241241 show e = show' [] e where

src/IRTS/Java/Mangling.hs+3−3

@@ -26,7 +26,7 @@ prefixCallNamespaces name (SFun fname args i e) =

2626 where

2727 prefixCallNamespacesExp :: Ident -> SExp -> SExp

2828 prefixCallNamespacesExp (Ident name) (SApp tail (NS n ns) args) =

29− SApp tail (NS n (name:ns)) args

29+ SApp tail (NS n (txt name:ns)) args

3030 prefixCallNamespacesExp name (SLet var e1 e2) =

3131 SLet var (prefixCallNamespacesExp name e1) (prefixCallNamespacesExp name e2)

3232 prefixCallNamespacesExp name (SUpdate var e) =

@@ -63,7 +63,7 @@ mangleWithPrefix prefix (UN name) =

6363 . parser ident

6464 . (prefix ++)

6565 . cleanNonLetter

66− $ cleanWs False name

66+ $ cleanWs False (str name)

6767 where

6868 cleanNonLetter (x:xs)

6969 | x == '#' = "_Hash" ++ cleanNonLetter xs

@@ -96,7 +96,7 @@ mangleWithPrefix prefix (UN name) =

9696 | capitalize = (toUpper x) : (cleanWs False xs)

9797 | otherwise = x : (cleanWs False xs)

9898 cleanWs _ [] = []

99−mangleWithPrefix prefix s@(SN _) = mangleWithPrefix prefix (UN (showCG s))

99+mangleWithPrefix prefix s@(SN _) = mangleWithPrefix prefix (sUN (showCG s))

100100

101101mangle :: (Applicative m, MonadError String m) => Name -> m Ident

102102mangle = mangleWithPrefix "__IDRCG__"

src/IRTS/Lang.hs+1−1

@@ -102,7 +102,7 @@ data LiftState = LS Name Int [(Name, LDecl)]

102102

103103lname (NS n x) i = NS (lname n i) x

104104lname (UN n) i = MN i n

105−lname x i = MN i (show x)

105+lname x i = sMN i (show x)

106106

107107liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]

108108liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs

src/IRTS/Simplified.hs+1−1

@@ -94,7 +94,7 @@ sVar (DV (Glob x))

9494sVar (DV x) = return (x, Nothing)

9595sVar e = do e' <- simplify False e

9696 i <- hvar

97− return (Glob (MN i "R"), Just e')

97+ return (Glob (sMN i "R"), Just e')

9898

9999mkapp f args = mkapp' f args [] where

100100 mkapp' f [] args = return $ f (reverse args)

src/Idris/AbsSyntax.hs+34−31

@@ -180,7 +180,7 @@ addNameHint ty n

180180 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }

181181

182182getNameHints :: IState -> Name -> [Name]

183−getNameHints i (UN "->") = [UN "f",UN "g"]

183+getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]

184184getNameHints i n =

185185 case lookupCtxt n (idris_namehints i) of

186186 [ns] -> ns

@@ -200,7 +200,7 @@ addInstance int n i

200200 [CI a b c d e ins] ->

201201 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)

202202 putIState $ ist { idris_classes = cs }

203− _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [] [i]) (idris_classes ist)

203+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)

204204 putIState $ ist { idris_classes = cs }

205205 where addI i ins | int = i : ins

206206 | chaser n = ins ++ [i]

@@ -209,7 +209,8 @@ addInstance int n i

209209 insI i (n : ns) | chaser n = i : n : ns

210210 | otherwise = n : insI i ns

211211

212− chaser (UN ('@':'@':_)) = True

212+ chaser (UN nm)

213+ | ('@':'@':_) <- str nm = True

213214 chaser (NS n _) = chaser n

214215 chaser _ = False

215216

@@ -689,16 +690,16 @@ setTypeCase t = do i <- getIState

689690

690691bi = fileFC "builtin"

691692

692−inferTy = MN 0 "__Infer"

693−inferCon = MN 0 "__infer"

693+inferTy = sMN 0 "__Infer"

694+inferCon = sMN 0 "__infer"

694695inferDecl = PDatadecl inferTy

695696 PType

696− [("", inferCon, PPi impl (MN 0 "iType") PType (

697− PPi expl (MN 0 "ival") (PRef bi (MN 0 "iType"))

697+ [("", inferCon, PPi impl (sMN 0 "iType") PType (

698+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

698699 (PRef bi inferTy)), bi)]

699700inferOpts = []

700701

701−infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "iType") Placeholder True, pexp t]

702+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

702703infP = P (TCon 6 0) inferTy (TType (UVal 0))

703704

704705getInferTerm, getInferType :: Term -> Term

@@ -715,18 +716,18 @@ primNames = [unitTy, unitCon,

715716 falseTy, pairTy, pairCon,

716717 eqTy, eqCon, inferTy, inferCon]

717718

718−unitTy = MN 0 "__Unit"

719−unitCon = MN 0 "__II"

719+unitTy = sMN 0 "__Unit"

720+unitCon = sMN 0 "__II"

720721unitDecl = PDatadecl unitTy PType

721722 [("", unitCon, PRef bi unitTy, bi)]

722723unitOpts = [DefaultEliminator]

723724

724−falseTy = MN 0 "__False"

725+falseTy = sMN 0 "__False"

725726falseDecl = PDatadecl falseTy PType []

726727falseOpts = []

727728

728−pairTy = MN 0 "__Pair"

729−pairCon = MN 0 "__MkPair"

729+pairTy = sMN 0 "__Pair"

730+pairCon = sMN 0 "__MkPair"

730731pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

731732 [("", pairCon, PPi impl (n "A") PType (

732733 PPi impl (n "B") PType (

@@ -734,11 +735,11 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

734735 PPi expl (n "b") (PRef bi (n "B"))

735736 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

736737 pexp (PRef bi (n "B"))])))), bi)]

737− where n a = MN 0 a

738+ where n a = sMN 0 a

738739pairOpts = []

739740

740−eqTy = UN "="

741−eqCon = UN "refl"

741+eqTy = sUN "="

742+eqCon = sUN "refl"

742743eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

743744 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

744745 PType)

@@ -748,19 +749,19 @@ eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

748749 pimp (n "B") Placeholder False,

749750 pexp (PRef bi (n "x")),

750751 pexp (PRef bi (n "x"))])), bi)]

751− where n a = MN 0 a

752+ where n a = sMN 0 a

752753eqOpts = []

753754

754−elimName = UN "__Elim"

755−elimMethElimTy = UN "__elimTy"

756−elimMethElim = UN "elim"

757−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]

755+elimName = sUN "__Elim"

756+elimMethElimTy = sUN "__elimTy"

757+elimMethElim = sUN "elim"

758+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

758759 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

759760 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

760761

761762-- Defined in builtins.idr

762−sigmaTy = UN "Exists"

763−existsCon = UN "Ex_intro"

763+sigmaTy = sUN "Exists"

764+existsCon = sUN "Ex_intro"

764765

765766piBind :: [(Name, PTerm)] -> PTerm -> PTerm

766767piBind = piBindp expl

@@ -898,7 +899,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

898899 updateps yn nm [] = []

899900 updateps yn nm (((a, t), i):as)

900901 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

901− | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as

902+ | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as

902903

903904 removeBound lhs ns = ns \\ nub (bnames lhs)

904905

@@ -1037,7 +1038,7 @@ addUsingConstraints syn fc t

10371038 -- if all of args in ns, then add it

10381039 doAdd (UConstraint c args : cs) ns t

10391040 | all (\n -> elem n ns) args

1040− = PPi (Constraint False Dynamic "") (MN 0 "cu")

1041+ = PPi (Constraint False Dynamic "") (sMN 0 "cu")

10411042 (mkConst c args) (doAdd cs ns t)

10421043 | otherwise = doAdd cs ns t

10431044

@@ -1461,12 +1462,14 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

14611462 fullApp x = x

14621463

14631464 match' x y = match (fullApp x) (fullApp y)

1464− match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'

1465− | PConstant (I _) <- getTm x = match (getTm x) x'

1466− match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])

1467− | PConstant (I _) <- getTm x = match (getTm x) x'

1468− match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'

1469− match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')

1465+ match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'

1466+ | fi == txt "fromInteger" && b == txt "builtins",

1467+ PConstant (I _) <- getTm x = match (getTm x) x'

1468+ match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])

1469+ | fi == txt "fromInteger" && b == txt "builtins",

1470+ PConstant (I _) <- getTm x = match (getTm x) x'

1471+ match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'

1472+ match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')

14701473 match (PApp _ f args) (PApp _ f' args')

14711474 | length args == length args'

14721475 = do mf <- match' f f'

src/Idris/AbsSyntaxTree.hs+21−19

@@ -156,10 +156,10 @@ deriving instance Binary CGInfo

156156deriving instance NFData CGInfo

157157!-}

158158

159−primDefs = [UN "unsafePerformPrimIO",

160− UN "mkLazyForeignPrim",

161− UN "mkForeignPrim",

162− UN "FalseElim"]

159+primDefs = [sUN "unsafePerformPrimIO",

160+ sUN "mkLazyForeignPrim",

161+ sUN "mkForeignPrim",

162+ sUN "FalseElim"]

163163

164164-- information that needs writing for the current module's .ibc file

165165data IBCWrite = IBCFix FixDecl

@@ -844,10 +844,10 @@ deriving instance Binary SSymbol

844844deriving instance NFData SSymbol

845845!-}

846846

847−initDSL = DSL (PRef f (UN ">>="))

848− (PRef f (UN "return"))

849− (PRef f (UN "<$>"))

850− (PRef f (UN "pure"))

847+initDSL = DSL (PRef f (sUN ">>="))

848+ (PRef f (sUN "return"))

849+ (PRef f (sUN "<$>"))

850+ (PRef f (sUN "pure"))

851851 Nothing

852852 Nothing

853853 Nothing

@@ -883,7 +883,7 @@ expandNS :: SyntaxInfo -> Name -> Name

883883expandNS syn n@(NS _ _) = n

884884expandNS syn n = case syn_namespace syn of

885885 [] -> n

886− xs -> NS n xs

886+ xs -> sNS n xs

887887

888888

889889--- Pretty printing declarations and terms

@@ -980,8 +980,8 @@ prettyImp impl = prettySe 10

980980 prettyBasic n

981981 where

982982 prettyBasic n@(UN _) = pretty n

983− prettyBasic (MN _ s) = text s

984− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n

983+ prettyBasic (MN _ s) = text (str s)

984+ prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n

985985 prettyBasic (SN sn) = text (show sn)

986986 prettySe p (PLam n ty sc) =

987987 bracket p 2 $

@@ -1052,8 +1052,9 @@ prettyImp impl = prettySe 10

10521052 | not impl = pretty f

10531053 prettySe p (PAppBind _ (PRef _ f) [])

10541054 | not impl = text "!" <+> pretty f

1055− prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)

1056− | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =

1055+ prettySe p (PApp _ (PRef _ op@(UN nm)) args)

1056+ | not (tnull nm) &&

1057+ length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

10571058 let [l, r] = getExps args in

10581059 bracket p 1 $

10591060 if size r > breakingSize then

@@ -1166,8 +1167,8 @@ showName ist bnd impl colour n = case ist of

11661167 Nothing -> showbasic n

11671168 where name = if impl then show n else showbasic n

11681169 showbasic n@(UN _) = showCG n

1169− showbasic (MN _ s) = s

1170− showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

1170+ showbasic (MN _ s) = str s

1171+ showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

11711172 showbasic (SN s) = show s

11721173 fst3 (x, _, _) = x

11731174 colourise n t = let ctxt' = fmap tt_ctxt ist in

@@ -1241,8 +1242,9 @@ showImp ist impl colour tm = se 10 [] tm where

12411242 | not impl = se p bnd hd

12421243 se p bnd (PAppBind _ hd@(PRef _ f) [])

12431244 | not impl = "!" ++ se p bnd hd

1244− se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)

1245− | length (getExps args) == 2 && not impl && not (isAlpha f)

1245+ se p bnd (PApp _ op@(PRef _ (UN nm)) args)

1246+ | not (tnull nm) &&

1247+ length (getExps args) == 2 && not impl && not (isAlpha (thead nm))

12461248 = let [l, r] = getExps args in

12471249 bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r

12481250 se p bnd (PApp _ f as)

@@ -1290,9 +1292,9 @@ showImp ist impl colour tm = se 10 [] tm where

12901292-- se p bnd x = "Not implemented"

12911293

12921294 slist' p bnd (PApp _ (PRef _ nil) _)

1293− | not impl && nsroot nil == UN "Nil" = Just []

1295+ | not impl && nsroot nil == sUN "Nil" = Just []

12941296 slist' p bnd (PApp _ (PRef _ cons) args)

1295− | nsroot cons == UN "::",

1297+ | nsroot cons == sUN "::",

12961298 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

12971299 all isImp imps,

12981300 Just tl' <- slist' p bnd tl

src/Idris/CaseSplit.hs+13−12

@@ -91,7 +91,8 @@ inventName ist ty n =

9191 Nothing -> []

9292 Just t -> getNameHints ist t

9393 let nsupp = case n of

94− MN i ('_':_) -> mkSupply (supp ++ varlist)

94+ MN i n | not (tnull n) && thead n == '_'

95+ -> mkSupply (supp ++ varlist)

9596 MN i n -> mkSupply (UN n : supp ++ varlist)

9697 x -> mkSupply (x : supp)

9798 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++

@@ -106,7 +107,7 @@ inventName ist ty n =

106107mkSupply ns = mkSupply' ns (map nextName ns)

107108 where mkSupply' xs ns' = xs ++ mkSupply ns'

108109

109−varlist = map (UN . (:[])) "xyzwstuv" -- EB's personal preference :)

110+varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

110111

111112stripNS tm = mapPT dens tm where

112113 dens (PRef fc n) = PRef fc (nsroot n)

@@ -164,7 +165,7 @@ argTys ist (PRef fc n)

164165 = case lookupTy n (tt_ctxt ist) of

165166 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing

166167 _ -> repeat Nothing

167− where tyName (Bind _ (Pi _) _) = Just (UN "->")

168+ where tyName (Bind _ (Pi _) _) = Just (sUN "->")

168169 tyName t | (P _ n _, _) <- unApply t = Just n

169170 | otherwise = Nothing

170171argTys _ _ = repeat Nothing

@@ -264,8 +265,8 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

264265

265266 -- TMP HACK: If there are Nats, we don't want to show as numerals since

266267 -- this isn't supported in a pattern, so special case here

267− nshow (PRef _ (UN "Z")) = "Z"

268− nshow (PApp _ (PRef _ (UN "S")) [x]) =

268+ nshow (PRef _ (UN z)) | z == txt "Z" = "Z"

269+ nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =

269270 "S " ++ addBrackets (nshow (getTm x))

270271 nshow t = show t

271272

@@ -296,7 +297,7 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

296297getUniq nm i

297298 = do ist <- getIState

298299 let n = nameRoot [] nm ++ "_" ++ show i

299− case lookupTy (UN n) (tt_ctxt ist) of

300+ case lookupTy (sUN n) (tt_ctxt ist) of

300301 [] -> return (n, i+1)

301302 _ -> getUniq nm (i+1)

302303

@@ -324,14 +325,14 @@ getClause l fn fp = do ty <- getInternalApp fp l

324325 mkApp i _ _ = ""

325326

326327 getNameFrom i used (PPi _ _ _ _)

327− = uniqueNameFrom (mkSupply [UN "f", UN "g"]) used

328+ = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used

328329 getNameFrom i used (PApp fc f as) = getNameFrom i used f

329− getNameFrom i used (PEq _ _ _) = uniqueNameFrom [UN "prf"] used

330+ getNameFrom i used (PEq _ _ _) = uniqueNameFrom [sUN "prf"] used

330331 getNameFrom i used (PRef fc f)

331332 = case getNameHints i f of

332− [] -> uniqueName (UN "x") used

333+ [] -> uniqueName (sUN "x") used

333334 ns -> uniqueNameFrom (mkSupply ns) used

334− getNameFrom i used _ = uniqueName (UN "x") used

335+ getNameFrom i used _ = uniqueName (sUN "x") used

335336

336337getProofClause :: Int -- ^ line number that the type is declared

337338 -> Name -- ^ Function name

@@ -363,11 +364,11 @@ mkWith str n = let str' = replaceRHS str "with (_)"

363364nameMissing :: [PTerm] -> Idris [PTerm]

364365nameMissing ps = do ist <- get

365366 newPats <- mapM nm ps

366− let newPats' = mergeAllPats ist (UN "_") (base (head ps))

367+ let newPats' = mergeAllPats ist (sUN "_") (base (head ps))

367368 newPats

368369 return (map fst newPats')

369370 where

370− base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (UN "_")))) args)

371+ base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (sUN "_")))) args)

371372 base t = t

372373

373374 nm ptm = do mptm <- elabNewPat ptm

src/Idris/Completion.hs+3−3

@@ -54,9 +54,9 @@ tactics = map fst tacticArgs

5454-- | Convert a name into a string usable for completion. Filters out names

5555-- that users probably don't want to see.

5656nameString :: Name -> Maybe String

57−nameString (UN ('@':_)) = Nothing

58−nameString (UN ('#':_)) = Nothing

59−nameString (UN n) = Just n

57+nameString (UN nm)

58+ | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing

59+nameString (UN n) = Just (str n)

6060nameString (NS n _) = nameString n

6161nameString _ = Nothing

6262

src/Idris/Core/CaseTree.hs+5−5

@@ -216,7 +216,7 @@ simpleCase tc cover reflect phase fc argtys cs

216216 then return t

217217 else Error (At fc (Msg "Typecase is not allowed"))

218218 Error err -> Error (At fc err)

219− where args = map (\i -> MN i "e") [0..]

219+ where args = map (\i -> sMN i "e") [0..]

220220 defaultCase True = STerm Erased

221221 defaultCase False = UnmatchedCase "Error"

222222 fstT (x, _, _) = x

@@ -300,8 +300,8 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

300300 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

301301 return $ PCon n t args'

302302 -- n + 1

303− toPat' (P _ (UN "prim__addBigInt") _)

304− [p, Constant (BI 1)]

303+ toPat' (P _ (UN pabi) _)

304+ [p, Constant (BI 1)] | pabi == txt "prim__addBigInt"

305305 = do p' <- toPat' p []

306306 return $ PSuc p'

307307 -- Typecase

@@ -333,7 +333,7 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

333333 toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc

334334 = do t' <- toPat' t []

335335 sc' <- toPat' sc []

336− return $ PReflected (UN "->") (t':sc':[])

336+ return $ PReflected (sUN "->") (t':sc':[])

337337 toPat' (P _ n _) args | reflect

338338 = do args' <- mapM (\x -> toPat' x []) args

339339 return $ PReflected n args'

@@ -490,7 +490,7 @@ argsToAlt rs@((r, m) : rest)

490490 uniq i n = n

491491

492492getVar :: String -> State CS Name

493−getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (MN v b)

493+getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)

494494

495495groupCons :: [Clause] -> State CS [Group]

496496groupCons cs = gc [] cs

src/Idris/Core/Elaborate.hs+9−9

@@ -445,7 +445,7 @@ prepare_apply fn imps =

445445

446446 mkMN n@(MN i _) = n

447447 mkMN n@(UN x) = MN 99999 x

448− mkMN n@(SN s) = MN 99999 (show s)

448+ mkMN n@(SN s) = sMN 99999 (show s)

449449 mkMN (NS n xs) = NS (mkMN n) xs

450450

451451 rebind hs (Bind n t sc)

@@ -564,9 +564,9 @@ checkPiGoal n

564564 = do g <- goal

565565 case g of

566566 Bind _ (Pi _) _ -> return ()

567− _ -> do a <- getNameFrom (MN 0 "pargTy")

568− b <- getNameFrom (MN 0 "pretTy")

569− f <- getNameFrom (MN 0 "pf")

567+ _ -> do a <- getNameFrom (sMN 0 "pargTy")

568+ b <- getNameFrom (sMN 0 "pretTy")

569+ f <- getNameFrom (sMN 0 "pf")

570570 claim a RType

571571 claim b RType

572572 claim f (RBind n (Pi (Var a)) (Var b))

@@ -578,13 +578,13 @@ checkPiGoal n

578578

579579simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

580580simple_app fun arg appstr =

581− do a <- getNameFrom (MN 0 "argTy")

582− b <- getNameFrom (MN 0 "retTy")

583− f <- getNameFrom (MN 0 "f")

584− s <- getNameFrom (MN 0 "s")

581+ do a <- getNameFrom (sMN 0 "argTy")

582+ b <- getNameFrom (sMN 0 "retTy")

583+ f <- getNameFrom (sMN 0 "f")

584+ s <- getNameFrom (sMN 0 "s")

585585 claim a RType

586586 claim b RType

587− claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

587+ claim f (RBind (sMN 0 "aX") (Pi (Var a)) (Var b))

588588 tm <- get_term

589589 start_unify s

590590 claim s (Var a)

src/Idris/Core/Evaluate.hs+14−14

@@ -99,11 +99,11 @@ specialise ctxt env limits t

9999

100100simplify :: Context -> Env -> TT Name -> TT Name

101101simplify ctxt env t

102− = evalState (do val <- eval False ctxt [(UN "lazy", 0),

103− (UN "assert_smaller", 0),

104− (UN "par", 0),

105− (UN "prim__syntactic_eq", 0),

106− (UN "fork", 0)]

102+ = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

103+ (sUN "assert_smaller", 0),

104+ (sUN "par", 0),

105+ (sUN "prim__syntactic_eq", 0),

106+ (sUN "fork", 0)]

107107 (map finalEntry env) (finalise t)

108108 [Simplify]

109109 quote 0 val) initEval

@@ -111,11 +111,11 @@ simplify ctxt env t

111111-- | Simplify for run-time (i.e. basic inlining)

112112rt_simplify :: Context -> Env -> TT Name -> TT Name

113113rt_simplify ctxt env t

114− = evalState (do val <- eval False ctxt [(UN "lazy", 0),

115− (UN "assert_smaller", 0),

116− (UN "par", 0),

117− (UN "prim__syntactic_eq", 0),

118− (UN "prim_fork", 0)]

114+ = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

115+ (sUN "assert_smaller", 0),

116+ (sUN "par", 0),

117+ (sUN "prim__syntactic_eq", 0),

118+ (sUN "prim_fork", 0)]

119119 (map finalEntry env) (finalise t)

120120 [RunTT]

121121 quote 0 val) initEval

@@ -190,7 +190,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

190190 = not (inl || dict) || elem n stk

191191 | Simplify `elem` opts

192192 = (not (inl || dict) || elem n stk)

193− || (n == UN "prim__syntactic_eq")

193+ || (n == sUN "prim__syntactic_eq")

194194 | otherwise = False

195195

196196 getCases cd | simpl = cases_totcheck cd

@@ -412,7 +412,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

412412 chooseAlt env _ (VP _ n _, args) alts amap

413413 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)

414414 chooseAlt env _ (VBind _ _ (Pi s) t, []) alts amap

415− | Just (ns, sc) <- findFn (UN "->") alts

415+ | Just (ns, sc) <- findFn (sUN "->") alts

416416 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern

417417 return $ Just (updateAmap (zip ns [s, t']) amap, sc)

418418 chooseAlt _ _ _ alts amap

@@ -492,7 +492,7 @@ instance Quote Value where

492492 = do sc' <- quote i sc

493493 t' <- quote i t

494494 v' <- quote i v

495− let sc'' = pToV (MN vd "vlet") (addBinder sc')

495+ let sc'' = pToV (sMN vd "vlet") (addBinder sc')

496496 return (Bind n (Let t' v') sc'')

497497 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

498498 quote i (VType u) = return $ TType u

@@ -891,7 +891,7 @@ lookupDefAcc :: Name -> Bool -> Context ->

891891lookupDefAcc n mkpublic ctxt

892892 = map mkp $ lookupCtxt n (definitions ctxt)

893893 -- io_bind a special case for REPL prettiness

894− where mkp (d, a, _, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))

894+ where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

895895 then (d, Public) else (d, a)

896896

897897lookupTotal :: Name -> Context -> [Totality]

src/Idris/Core/Execute.hs+57−33

@@ -96,7 +96,7 @@ toTT (EApp e1 e2) = do e1' <- toTT e1

9696toTT (EType u) = return $ TType u

9797toTT EErased = return Erased

9898toTT (EConstant c) = return (Constant c)

99−toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT

99+toTT (EThunk i) = return (P (DCon 0 0) (sMN i "THUNK") Erased) --(force i) >>= toTT

100100toTT (EHandle _) = return Erased

101101

102102unApplyV :: ExecVal -> (ExecVal, [ExecVal])

@@ -173,7 +173,7 @@ execute tm = do est <- initState

173173 Right tm' -> return tm'

174174

175175ioWrap :: ExecVal -> ExecVal

176−ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]

176+ioWrap tm = mkEApp (EP (DCon 0 2) (sUN "prim__IO") EErased) [EErased, tm]

177177

178178ioUnit :: ExecVal

179179ioUnit = ioWrap (EP Ref unitCon EErased)

@@ -219,8 +219,9 @@ execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

219219execApp env ctxt (f, args) = do newF <- doExec env ctxt f

220220 laziness <- (++ repeat False) <$> (getLaziness newF)

221221 newArgs <- mapM argExec (zip args laziness)

222− execApp' env ctxt newF newArgs

223− where getLaziness (EP _ (UN "lazy") _) = return [False, True]

222+ res <- execApp' env ctxt newF newArgs

223+ return res

224+ where getLaziness (EP _ l _) | l == sUN "lazy" = return [False, True]

224225 getLaziness (EP _ n _) = do est <- getExecState

225226 let argInfo = exec_implicits est

226227 case lookupCtxtName n argInfo of

@@ -235,28 +236,36 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f

235236

236237execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

237238execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

238−execApp' env ctxt (EP _ (UN "unsafePerformPrimIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =

239− execApp' env ctxt v rest

240−

241−execApp' env ctxt (EP _ (UN "prim_io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

239+execApp' env ctxt (EP _ fp _) (ty:action:rest)

240+ | fp == upio,

241+ (prim__IO, [_, v]) <- unApplyV action

242+ = execApp' env ctxt v rest

243+

244+execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)

245+ | fp == piobind,

246+ (prim__IO, [_, v']) <- unApplyV v =

242247 do v'' <- tryForce v'

243248 res <- execApp' env ctxt k [v''] >>= tryForce

244249 execApp' env ctxt res rest

245−execApp' env ctxt con@(EP _ (UN "prim_io_return") _) args@(tp:v:rest) =

250+execApp' env ctxt con@(EP _ fp _) args@(tp:v:rest)

251+ | fp == pioret =

246252 do v' <- tryForce v

247253 execApp' env ctxt (mkEApp con [tp, v']) rest

248254

249255-- Special cases arising from not having access to the C RTS in the interpreter

250−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str arg):_:rest)

251− | Just (FFun "putStr" _ _) <- foreignFromTT fn

256+execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

257+ | fp == mkfprim,

258+ Just (FFun "putStr" _ _) <- foreignFromTT fn

252259 = do execIO (putStr arg)

253260 execApp' env ctxt ioUnit rest

254−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:_:EHandle h:_:rest)

255− | Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

261+execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

262+ | fp == mkfprim,

263+ Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

256264 = do contents <- execIO $ hGetLine h

257265 execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest

258−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

259− | Just (FFun "fileOpen" _ _) <- foreignFromTT fn

266+execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

267+ | fp == mkfprim,

268+ Just (FFun "fileOpen" _ _) <- foreignFromTT fn

260269 = do m <- case mode of

261270 "r" -> return ReadMode

262271 "w" -> return WriteMode

@@ -268,34 +277,38 @@ execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str f):EConstan

268277 h <- execIO $ openFile f m

269278 execApp' env ctxt (ioWrap (EHandle h)) (tail rest)

270279

271−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)

272− | Just (FFun "fileEOF" _ _) <- foreignFromTT fn

280+execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

281+ | fp == mkfprim,

282+ Just (FFun "fileEOF" _ _) <- foreignFromTT fn

273283 = do eofp <- execIO $ hIsEOF h

274284 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

275285 execApp' env ctxt res (tail rest)

276286

277−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)

278− | Just (FFun "fileClose" _ _) <- foreignFromTT fn

287+execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

288+ | fp == mkfprim,

289+ Just (FFun "fileClose" _ _) <- foreignFromTT fn

279290 = do execIO $ hClose h

280291 execApp' env ctxt ioUnit (tail rest)

281292

282−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EPtr p):rest)

283− | Just (FFun "isNull" _ _) <- foreignFromTT fn

293+execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

294+ | fp == mkfprim,

295+ Just (FFun "isNull" _ _) <- foreignFromTT fn

284296 = let res = ioWrap . EConstant . I $

285297 if p == nullPtr then 1 else 0

286298 in execApp' env ctxt res (tail rest)

287299

288300-- A foreign-returned char* has to be tested for NULL sometimes

289−execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str s):rest)

290− | Just (FFun "isNull" _ _) <- foreignFromTT fn

301+execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

302+ | fp == mkfprim,

303+ Just (FFun "isNull" _ _) <- foreignFromTT fn

291304 = let res = ioWrap . EConstant . I $ 0

292305 in execApp' env ctxt res (tail rest)

293306

294307-- Throw away the 'World' argument to the foreign function

295308

296−execApp' env ctxt f@(EP _ (UN "mkForeignPrim") _) args@(ty:fn:xs)

297− | Just (FFun f argTs retT) <- foreignFromTT fn

298− , length xs >= length argTs =

309+execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs)

310+ | Just (FFun f argTs retT) <- foreignFromTT fn,

311+ fp == mkfprim && length xs >= length argTs =

299312 do let (args', xs') = (take (length argTs) xs, -- foreign args

300313 drop (length argTs + 1) xs) -- rest

301314 res <- stepForeign (ty:fn:args')

@@ -343,13 +356,23 @@ execApp' env ctxt (EThunk i) args = do f <- force i

343356execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

344357execApp' env ctxt f args = return (mkEApp f args)

345358

359+prs = sUN "prim__readString"

360+pbm = sUN "prim__believe_me"

361+pstd = sUN "prim__stdin"

362+mkfprim = sUN "mkForeignPrim"

363+pioret = sUN "prim_io_return"

364+piobind = sUN "prim_io_bind"

365+upio = sUN "unsafePerformPrimIO"

366+

346367-- | Look up primitive operations in the global table and transform them into ExecVal functions

347368getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

348−getOp (UN "prim__believe_me") [_, _, x] = Just (return x)

349−getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =

369+getOp fn [_, _, x] | fn == pbm = Just (return x)

370+getOp fn [EP _ fn' _]

371+ | fn == prs && fn' == pstd =

350372 Just $ do line <- execIO getLine

351373 return (EConstant (Str line))

352−getOp (UN "prim__readString") [EHandle h] =

374+getOp fn [EHandle h]

375+ | fn == prs =

353376 Just $ do contents <- execIO $ hGetLine h

354377 return (EConstant (Str (contents ++ "\n")))

355378getOp n args = getPrim n primitives >>= flip applyPrim args

@@ -478,11 +501,12 @@ foreignFromTT t = case (unApplyV t) of

478501 argFTy <- sequence $ map getFTy argTy

479502 retFTy <- getFTy ret

480503 return $ FFun name argFTy retFTy

481− _ -> trace "failed to construct ffun" Nothing

504+ _ -> trace ("failed to construct ffun") Nothing

482505

483506getFTy :: ExecVal -> Maybe FType

484−getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =

485− case intTy of

507+getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))

508+ | fi == txt "FIntT" =

509+ case str intTy of

486510 "ITNative" -> Just (FArith (ATInt ITNative))

487511 "ITChar" -> Just (FArith (ATInt ITChar))

488512 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))

@@ -491,7 +515,7 @@ getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =

491515 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))

492516 _ -> Nothing

493517getFTy (EP _ (UN t) _) =

494− case t of

518+ case str t of

495519 "FFloat" -> Just (FArith ATFloat)

496520 "FString" -> Just FString

497521 "FPtr" -> Just FPtr

src/Idris/Core/ProofState.hs+7−7

@@ -159,7 +159,7 @@ hole (Hole _) = True

159159hole (Guess _ _) = True

160160hole _ = False

161161

162−holeName i = MN i "hole"

162+holeName i = sMN i "hole"

163163

164164qshow :: Fails -> String

165165qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

@@ -209,7 +209,7 @@ getName :: Monad m => String -> StateT TState m Name

209209getName tag = do ps <- get

210210 let n = nextname ps

211211 put (ps { nextname = n+1 })

212− return $ MN n tag

212+ return $ sMN n tag

213213

214214action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()

215215action a = do ps <- get

@@ -568,16 +568,16 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

568568 do (tmv, tmt) <- lift $ check ctxt env tm

569569 let tmt' = normalise ctxt env tmt

570570 case unApply tmt' of

571− (P _ (UN "=") _, [lt,rt,l,r]) ->

571+ (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->

572572 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

573573 let newt = mkP l r l t

574574 let sc = forget $ (Bind x (Hole newt)

575− (mkApp (P Ref (UN "replace") (TType (UVal 0)))

575+ (mkApp (P Ref (sUN "replace") (TType (UVal 0)))

576576 [lt, l, r, p, tmv, xp]))

577577 (scv, sct) <- lift $ check ctxt env sc

578578 return scv

579579 _ -> lift $ tfail (NotEquality tmv tmt')

580− where rname = MN 0 "replaced"

580+ where rname = sMN 0 "replaced"

581581rewrite _ _ _ _ = fail "Can't rewrite here"

582582

583583-- To make the P for rewrite, replace syntactic occurrences of l in ty with

@@ -633,7 +633,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

633633 [] -> fail $ "Induction needs an eliminator for " ++ show tnm

634634 xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show tnm

635635 _ -> fail "Unkown type for induction"

636− where scname = MN 0 "scarg"

636+ where scname = sMN 0 "scarg"

637637 makeConsArg (nm, ty) = P Bound nm ty

638638 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

639639 bindConsArgs [] v = v

@@ -642,7 +642,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

642642 splitTyArgs param_pos tyargs =

643643 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs

644644 in (map snd params, map snd indicies)

645− makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (MN 0 "idx") nms):nms) []

645+ makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []

646646 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

647647 let var = P Bound idnm idxt

648648 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

src/Idris/Core/TT.hs+60−29

@@ -25,6 +25,7 @@ import Control.Monad.Trans.Error (Error(..))

2525import Debug.Trace

2626import qualified Data.Map.Strict as Map

2727import Data.Char

28+import qualified Data.Text as T

2829import Data.List

2930import Data.Vector.Unboxed (Vector)

3031import qualified Data.Vector.Unboxed as V

@@ -240,22 +241,44 @@ traceWhen False _ a = a

240241

241242-- | Names are hierarchies of strings, describing scope (so no danger of

242243-- duplicate names, but need to be careful on lookup).

243−data Name = UN String -- ^ User-provided name

244− | NS Name [String] -- ^ Root, namespaces

245− | MN Int String -- ^ Machine chosen names

244+data Name = UN T.Text -- ^ User-provided name

245+ | NS Name [T.Text] -- ^ Root, namespaces

246+ | MN Int T.Text -- ^ Machine chosen names

246247 | NErased -- ^ Name of somethng which is never used in scope

247248 | SN SpecialName -- ^ Decorated function names

248249 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

249250 deriving (Eq, Ord)

250251

252+txt :: String -> T.Text

253+txt = T.pack

254+

255+str :: T.Text -> String

256+str = T.unpack

257+

258+tnull :: T.Text -> Bool

259+tnull = T.null

260+

261+thead :: T.Text -> Char

262+thead = T.head

263+

264+-- Smart constructors for names, using old String style

265+sUN :: String -> Name

266+sUN s = UN (txt s)

267+

268+sNS :: Name -> [String] -> Name

269+sNS n ss = NS n (map txt ss)

270+

271+sMN :: Int -> String -> Name

272+sMN i s = MN i (txt s)

273+

251274{-!

252275deriving instance Binary Name

253276deriving instance NFData Name

254277!-}

255278

256279data SpecialName = WhereN Int Name Name

257− | InstanceN Name [String]

258− | ParentN Name String

280+ | InstanceN Name [T.Text]

281+ | ParentN Name T.Text

259282 | MethodN Name

260283 | CaseN Name

261284 | ElimN Name

@@ -265,6 +288,12 @@ deriving instance Binary SpecialName

265288deriving instance NFData SpecialName

266289!-}

267290

291+sInstanceN :: Name -> [String] -> SpecialName

292+sInstanceN n ss = InstanceN n (map T.pack ss)

293+

294+sParentN :: Name -> String -> SpecialName

295+sParentN n s = ParentN n (T.pack s)

296+

268297instance Sized Name where

269298 size (UN n) = 1

270299 size (NS n els) = 1 + length els

@@ -272,36 +301,36 @@ instance Sized Name where

272301 size _ = 1

273302

274303instance Pretty Name where

275− pretty (UN n) = text n

304+ pretty (UN n) = text (T.unpack n)

276305 pretty (NS n s) = pretty n

277− pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace

306+ pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

278307 pretty (SN s) = text (show s)

279308

280309instance Show Name where

281− show (UN n) = n

282− show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

283− show (MN _ "underscore") = "_"

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

310+ show (UN n) = str n

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

312+ show (MN _ u) | u == txt "underscore" = "_"

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

285314 show (SN s) = show s

286315 show NErased = "_"

287316

288317instance Show SpecialName where

289318 show (WhereN i p c) = show p ++ ", " ++ show c

290− show (InstanceN cl inst) = showSep ", " inst ++ " instance of " ++ show cl

319+ show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl

291320 show (MethodN m) = "method " ++ show m

292− show (ParentN p c) = show p ++ "#" ++ c

321+ show (ParentN p c) = show p ++ "#" ++ T.unpack c

293322 show (CaseN n) = "case block in " ++ show n

294323 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

295324

296325-- Show a name in a way decorated for code generation, not human reading

297326showCG :: Name -> String

298−showCG (UN n) = n

299−showCG (NS n s) = showSep "." (reverse s) ++ "." ++ showCG n

300−showCG (MN _ "underscore") = "_"

301−showCG (MN i s) = "{" ++ s ++ show i ++ "}"

327+showCG (UN n) = T.unpack n

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

329+showCG (MN _ u) | u == txt "underscore" = "_"

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

302331showCG (SN s) = showCG' s

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

304− showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" inst

333+ showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

305334 showCG' (MethodN m) = '!':showCG m

306335 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

307336 showCG' (CaseN c) = showCG c ++ "_case"

@@ -317,7 +346,8 @@ emptyContext = Map.empty

317346mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b

318347mapCtxt = fmap . fmap

319348

320−tcname (UN ('@':_)) = True

349+tcname (UN xs) | T.null xs = False

350+ | otherwise = T.head xs == '@'

321351tcname (NS n _) = tcname n

322352tcname (SN (InstanceN _ _)) = True

323353tcname (SN (MethodN _)) = True

@@ -325,7 +355,8 @@ tcname (SN (ParentN _ _)) = True

325355tcname _ = False

326356

327357implicitable (NS n _) = implicitable n

328−implicitable (UN (x:xs)) = isLower x

358+implicitable (UN xs) | T.null xs = False

359+ | otherwise = isLower (T.head xs)

329360implicitable (MN _ _) = True

330361implicitable _ = False

331362

@@ -626,10 +657,10 @@ instance TermSize (TT Name) where

626657 | otherwise = 1

627658 termsize n (V _) = 1

628659 termsize n (Bind n' (Let t v) sc)

629− = let rn = if n == n' then MN 0 "noname" else n in

660+ = let rn = if n == n' then sMN 0 "noname" else n in

630661 termsize rn v + termsize rn sc

631662 termsize n (Bind n' b sc)

632− = let rn = if n == n' then MN 0 "noname" else n in

663+ = let rn = if n == n' then sMN 0 "noname" else n in

633664 termsize rn sc

634665 termsize n (App f a) = termsize n f + termsize n a

635666 termsize n (Proj t i) = termsize n t

@@ -889,13 +920,13 @@ uniqueBinders ns t = t

889920

890921nextName (NS x s) = NS (nextName x) s

891922nextName (MN i n) = MN (i+1) n

892−nextName (UN x) = let (num', nm') = span isDigit (reverse x)

893− nm = reverse nm'

894− num = readN (reverse num') in

895− UN (nm ++ show (num+1))

923+nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)

924+ nm = T.reverse nm'

925+ num = readN (T.reverse num') in

926+ UN (nm `T.append` txt (show (num+1)))

896927 where

897− readN "" = 0

898− readN x = read x

928+ readN x | not (T.null x) = read (T.unpack x)

929+ readN x = 0

899930nextName (SN x) = SN (nextName' x)

900931 where

901932 nextName' (WhereN i f x) = WhereN i f (nextName x)

@@ -1040,7 +1071,7 @@ pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

10401071 pureBinder (Let t v) = pureTerm t && pureTerm v

10411072 pureBinder t = pureTerm (binderTy t)

10421073

1043− notClassName (MN _ "class") = False

1074+ notClassName (MN _ c) | c == txt "class" = False

10441075 notClassName _ = True

10451076

10461077pureTerm _ = True

src/Idris/Core/Typecheck.hs+1−1

@@ -88,7 +88,7 @@ check' holes ctxt env top = chk env top where

8888 -- make sure bound names in function types are locally unique, machine

8989 -- generated names, we'll be fine.

9090 -- NOTE: now replaced with 'uniqueBinders' above

91− where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)

91+ where renameBinders i (Bind x (Pi s) t) = Bind (sMN i "binder") (Pi s)

9292 (renameBinders (i+1) t)

9393 renameBinders i sc = sc

9494 chk env RType

src/Idris/Core/Unify.hs+1−1

@@ -277,7 +277,7 @@ unify ctxt env topx topy dont holes =

277277

278278 un' fn bnames (App f x) (Bind n (Pi t) y)

279279 | noOccurrence n y && x == y

280− = un' False bnames f (Bind (MN 0 "uv") (Lam (TType (UVar 0)))

280+ = un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

281281 (Bind n (Pi t) (V 1)))

282282

283283 un' fn bnames (Bind x bx sx) (Bind y by sy)

src/Idris/Coverage.hs+12−9

@@ -31,7 +31,7 @@ mkPatTm t = do i <- getIState

3131 return $ mkApp t' args'

3232 toTT _ = do v <- get

3333 put (v + 1)

34− return (P Bound (MN v "imp") Erased)

34+ return (P Bound (sMN v "imp") Erased)

3535

3636-- Given a list of LHSs, generate a extra clauses which cover the remaining

3737-- cases. The ones which haven't been provided are marked 'absurd' so that the

@@ -166,13 +166,13 @@ genAll i args

166166 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

167167 otherPats o@(PPair fc l r)

168168 = ops fc pairCon

169− ([pimp (UN "A") Placeholder True,

170− pimp (UN "B") Placeholder True] ++

169+ ([pimp (sUN "A") Placeholder True,

170+ pimp (sUN "B") Placeholder True] ++

171171 [pexp l, pexp r]) o

172172 otherPats o@(PDPair fc t _ v)

173− = ops fc (UN "Ex_intro")

174− ([pimp (UN "a") Placeholder True,

175− pimp (UN "P") Placeholder True] ++

173+ = ops fc (sUN "Ex_intro")

174+ ([pimp (sUN "a") Placeholder True,

175+ pimp (sUN "P") Placeholder True] ++

176176 [pexp t,pexp v]) o

177177 otherPats o@(PConstant c) = return o

178178 otherPats arg = return Placeholder

@@ -191,7 +191,8 @@ genAll i args

191191 getExpTm t = getTm t

192192

193193 -- put it back to its original form

194− resugar (PApp _ (PRef fc (UN "Ex_intro")) [_,_,t,v])

194+ resugar (PApp _ (PRef fc (UN ei)) [_,_,t,v])

195+ | ei == txt "Ex_intro"

195196 = PDPair fc (getTm t) Placeholder (getTm v)

196197 resugar (PApp _ (PRef fc n) [_,_,l,r])

197198 | n == pairCon

@@ -258,7 +259,8 @@ calcProd i fc topn pats

258259

259260 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

260261 prod n done ok ap@(App _ _)

261− | (P _ (UN "lazy") _, [_, arg]) <- unApply ap = prod n done ok arg

262+ | (P _ (UN l) _, [_, arg]) <- unApply ap,

263+ l == txt "lazy" = prod n done ok arg

262264 | (P nt f _, args) <- unApply ap

263265 = do recOK <- checkProdRec (n:done) f

264266 let ctxt = tt_ctxt i

@@ -405,7 +407,8 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

405407 findCalls (dePat rhs) (patvars lhs) pargs

406408

407409 findCalls ap@(App f a) pvs pargs

408− | (P _ (UN "lazy") _, [_, arg]) <- unApply ap

410+ | (P _ (UN l) _, [_, arg]) <- unApply ap,

411+ l == txt "lazy"

409412 = findCalls arg pvs pargs

410413 | (P _ n _, args) <- unApply ap

411414 = mkChange n args pargs ++

src/Idris/DSL.hs+4−4

@@ -57,8 +57,8 @@ expandDo dsl (PDoBlock ds)

5757 block b (DoBind fc n tm : rest)

5858 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

5959 block b (DoBindP fc p tm : rest)

60− = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder

61− (PCase fc (PRef fc (MN 0 "bpat"))

60+ = PApp fc b [pexp tm, pexp (PLam (sMN 0 "bpat") Placeholder

61+ (PCase fc (PRef fc (sMN 0 "bpat"))

6262 [(p, block b rest)]))]

6363 block b (DoLet fc n ty tm : rest)

6464 = PLet n ty tm (block b rest)

@@ -67,7 +67,7 @@ expandDo dsl (PDoBlock ds)

6767 block b (DoExp fc tm : rest)

6868 = PApp fc b

6969 [pexp tm,

70− pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

70+ pexp (PLam (sMN 0 "bindx") Placeholder (block b rest))]

7171 block b _ = PElabError (Msg "Invalid statement in do block")

7272

7373expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

@@ -131,7 +131,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

131131 db' (PAppBind fc t args)

132132 = do args' <- dbs args

133133 (bs, n) <- get

134− let nm = MN n ("bindApp" ++ show n)

134+ let nm = sMN n ("bindApp" ++ show n)

135135 put ((nm, fc, PApp fc t args') : bs, n+1)

136136 return (PRef fc nm)

137137 db' (PApp fc t args)

src/Idris/DataOpts.hs+26−15

@@ -37,7 +37,7 @@ getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t

3737

3838 -- Label all occurrences of the variable bound in Pi in the rest of

3939 -- the term with the number i so that we can recognize them anytime later.

40− label i = instantiate $ P Bound (MN i "ctor_arg") Erased

40+ label i = instantiate $ P Bound (sMN i "ctor_arg") Erased

4141

4242 addCollapsibleArgs :: Int -> Type -> ForceMap -> ForceMap

4343 addCollapsibleArgs i (Bind vn (Pi ty) rest) alreadyForceable

@@ -73,7 +73,8 @@ getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t

7373 guardedArgs t = bareArg t

7474

7575 bareArg :: Term -> ForceMap

76− bareArg (P _ (MN i "ctor_arg") _) = M.singleton i Unconditional

76+ bareArg (P _ (MN i ctor_arg) _)

77+ | ctor_arg == txt "ctor_arg" = M.singleton i Unconditional

7778 bareArg _ = M.empty

7879

7980 unionMap :: (a -> ForceMap) -> [a] -> ForceMap

@@ -227,17 +228,24 @@ applyDataOpt oi n args

227228

228229-- Run-time: do everything

229230

231+prel = [txt "Nat", txt "Prelude"]

232+

230233instance Optimisable (TT Name) where

231− applyOpts (P _ (NS (UN "plus") ["Nat","Prelude"]) _)

232− = return (P Ref (UN "prim__addBigInt") Erased)

233− applyOpts (P _ (NS (UN "mult") ["Nat","Prelude"]) _)

234− = return (P Ref (UN "prim__mulBigInt") Erased)

235− applyOpts (App (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _) x)

234+ applyOpts (P _ (NS (UN fn) mod) _)

235+ | fn == txt "plus" && mod == prel

236+ = return (P Ref (sUN "prim__addBigInt") Erased)

237+ applyOpts (P _ (NS (UN fn) mod) _)

238+ | fn == txt "mult" && mod == prel

239+ = return (P Ref (sUN "prim__mulBigInt") Erased)

240+ applyOpts (App (P _ (NS (UN fn) mod) _) x)

241+ | fn == txt "fromIntegerNat" && mod == prel

236242 = applyOpts x

237− applyOpts (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _)

238− = return (App (P Ref (NS (UN "id") ["Basics","Prelude"]) Erased) Erased)

239− applyOpts (P _ (NS (UN "toIntegerNat") ["Nat","Prelude"]) _)

240− = return (App (P Ref (NS (UN "id") ["Basics","Prelude"]) Erased) Erased)

243+ applyOpts (P _ (NS (UN fn) mod) _)

244+ | fn == txt "fromIntegerNat" && mod == prel

245+ = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

246+ applyOpts (P _ (NS (UN fn) mod) _)

247+ | fn == txt "toIntegerNat" && mod == prel

248+ = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

241249 applyOpts c@(P (DCon t arity) n _)

242250 = do i <- getIState

243251 case lookupCtxt n (idris_optimisation i) of

@@ -288,16 +296,19 @@ applyDataOptRT oi n tag arity args

288296 (collapsible oi) (M.fromList $ forceable oi) in

289297 bind extra tm

290298 where

291− satArgs n = map (\i -> MN i "sat") [1..n]

299+ satArgs n = map (\i -> sMN i "sat") [1..n]

292300

293301 bind [] tm = tm

294302 bind (n:ns) tm = Bind n (Lam Erased) (pToV n (bind ns tm))

295303

296304 -- Nat special cases

297305 -- TODO: Would be nice if this was configurable in idris source!

298− doOpts (NS (UN "Z") ["Nat", "Prelude"]) [] _ _ = Constant (BI 0)

299− doOpts (NS (UN "S") ["Nat", "Prelude"]) [k] _ _

300− = App (App (P Ref (UN "prim__addBigInt") Erased) k) (Constant (BI 1))

306+ doOpts (NS (UN z) [nat, prelude]) [] _ _

307+ | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"

308+ = Constant (BI 0)

309+ doOpts (NS (UN s) [nat, prelude]) [k] _ _

310+ | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

311+ = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

301312

302313 doOpts n args True _ = Erased

303314 doOpts n args _ forceMap

src/Idris/Delaborate.hs+9−9

@@ -42,7 +42,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

4242

4343 de env _ (App f a) = deFn env f [a]

4444 de env _ (V i) | i < length env = PRef un (snd (env!!i))

45− | otherwise = PRef un (UN ("v" ++ show i ++ ""))

45+ | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

4646 de env _ (P _ n _) | n == unitTy = PTrue un

4747 | n == unitCon = PTrue un

4848 | n == falseTy = PFalse un

@@ -63,8 +63,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

6363 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

6464 de env _ (Bind n (Let ty val) sc)

6565 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

66− de env _ (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) [] sc

67− de env _ (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) [] sc

66+ de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

67+ de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

6868 de env _ (Bind n _ sc) = de ((n,n):env) [] sc

6969 de env _ (Constant i) = PConstant i

7070 de env _ Erased = Placeholder

@@ -82,16 +82,16 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

8282 deFn env (P _ n _) [l,r]

8383 | n == pairTy = PPair un (de env [] l) (de env [] r)

8484 | n == eqCon = PRefl un (de env [] r)

85− | n == UN "lazy" = de env [] r

85+ | n == sUN "lazy" = de env [] r

8686 deFn env (P _ n _) [ty, Bind x (Lam _) r]

87− | n == UN "Exists"

87+ | n == sUN "Exists"

8888 = PDPair un (PRef un x) (de env [] ty)

8989 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

9090 deFn env (P _ n _) [_,_,l,r]

9191 | n == pairCon = PPair un (de env [] l) (de env [] r)

9292 | n == eqTy = PEq un (de env [] l) (de env [] r)

93− | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder

94− (de env [] r)

93+ | n == sUN "Ex_intro" = PDPair un (de env [] l) Placeholder

94+ (de env [] r)

9595 deFn env (P _ n _) args | not mvs

9696 = case lookup n (idris_metavars ist) of

9797 Just (Just _, mi, _) ->

@@ -220,8 +220,8 @@ showqual i n = showName (Just i) [] False False (dens n)

220220 dens n = n

221221

222222showbasic n@(UN _) = show n

223−showbasic (MN _ s) = s

224−showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

223+showbasic (MN _ s) = str s

224+showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

225225showbasic (SN s) = show s

226226

227227

src/Idris/Docs.hs+1−1

@@ -107,7 +107,7 @@ docFun n

107107

108108 return (Doc n docstr args (delab i ty) f)

109109 where funName :: Name -> String

110− funName (UN n) = n

110+ funName (UN n) = str n

111111 funName (NS n _) = funName n

112112

113113

src/Idris/ElabDecls.hs+83−75

@@ -34,6 +34,7 @@ import Data.Maybe

3434import Debug.Trace

3535

3636import qualified Data.Map as Map

37+import qualified Data.Text as T

3738import Data.Char(isLetter, toLower)

3839import Data.List.Split (splitOn)

3940

@@ -139,14 +140,20 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

139140 | otherwise = mergeTy sc sc'

140141 mergeTy _ sc = sc

141142

142− tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))

143− (App (P _ (NS (UN "Maybe") ns2) _)

144− (App (P _ (NS (UN "List") ns3) _)

145− (P _ (NS (UN "ErrorReportPart") ns4) _))))

146− | ns1 == ["Errors","Reflection","Language"]

147− , ns2 == ["Maybe", "Prelude"]

148− , ns3 == ["List", "Prelude"]

149− , ns4 == ["Errors","Reflection","Language"] = True

143+ err = txt "Err"

144+ maybe = txt "Maybe"

145+ lst = txt "List"

146+ errrep = txt "ErrorReportPart"

147+

148+ tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))

149+ (App (P _ (NS (UN m) ns2) _)

150+ (App (P _ (NS (UN l) ns3) _)

151+ (P _ (NS (UN r) ns4) _))))

152+ | e == err && m == maybe && l == lst && r == errrep

153+ , ns1 == map txt ["Errors","Reflection","Language"]

154+ , ns2 == map txt ["Maybe", "Prelude"]

155+ , ns3 == map txt ["List", "Prelude"]

156+ , ns4 == map txt ["Errors","Reflection","Language"] = True

150157 tyIsHandler _ = False

151158

152159

@@ -337,7 +344,7 @@ elabEliminator paramPos n ty cons info = do

337344

338345 applyNS :: Name -> [String] -> Name

339346 applyNS n [] = n

340− applyNS n ns = NS n ns

347+ applyNS n ns = sNS n ns

341348

342349 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

343350 splitPi = splitPi' []

@@ -376,11 +383,11 @@ elabEliminator paramPos n ty cons info = do

376383

377384 simpleName :: Name -> String

378385 simpleName (NS n _) = simpleName n

379− simpleName (MN i n) = n ++ show i

386+ simpleName (MN i n) = str n ++ show i

380387 simpleName n = show n

381388

382389 nameSpaces :: Name -> [String]

383− nameSpaces (NS _ ns) = ns

390+ nameSpaces (NS _ ns) = map str ns

384391 nameSpaces _ = []

385392

386393 freshName :: String -> EliminatorState Name

@@ -389,16 +396,16 @@ elabEliminator paramPos n ty cons info = do

389396 let i = fromMaybe 0 (Map.lookup key nameMap)

390397 let name = key ++ show i

391398 put $ Map.insert key (i+1) nameMap

392− return (UN name)

399+ return (sUN name)

393400

394401 scrutineeName :: Name

395− scrutineeName = UN "scrutinee"

402+ scrutineeName = sUN "scrutinee"

396403

397404 scrutineeArgName :: Name

398− scrutineeArgName = UN "scrutineeArg"

405+ scrutineeArgName = sUN "scrutineeArg"

399406

400407 motiveName :: Name

401− motiveName = UN "prop"

408+ motiveName = sUN "prop"

402409

403410 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

404411 mkMotive n paramPos params indicies =

@@ -488,7 +495,7 @@ elabEliminator paramPos n ty cons info = do

488495 let (_, consIdxs) = splitArgPms resTy

489496 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

490497 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

491− applyRecMotive (n,_,ty) = (UN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

498+ applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

492499 where (_, idxs) = splitArgPms ty

493500

494501 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

@@ -539,7 +546,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

539546 (zip

540547 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

541548 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

542− addNameHint eqTy (UN "prf")

549+ addNameHint eqTy (sUN "prf")

543550 elabDecl EAll toplevel elimDecl

544551 mapM_ elabPrim primitives

545552 -- Special case prim__believe_me because it doesn't work on just constants

@@ -562,11 +569,11 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

562569

563570 p_believeMe [_,_,x] = Just x

564571 p_believeMe _ = Nothing

565− believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))

566− (Bind (UN "b") (Pi (TType (UVar (-2))))

567− (Bind (UN "x") (Pi (V 1)) (V 1)))

572+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))

573+ (Bind (sUN "b") (Pi (TType (UVar (-2))))

574+ (Bind (sUN "x") (Pi (V 1)) (V 1)))

568575 elabBelieveMe

569− = do let prim__believe_me = (UN "prim__believe_me")

576+ = do let prim__believe_me = sUN "prim__believe_me"

570577 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

571578 setTotality prim__believe_me (Partial NotCovering)

572579 i <- getIState

@@ -580,19 +587,19 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

580587 | otherwise = Just (VApp vnNothing VErased)

581588 p_synEq args = Nothing

582589

583− nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased

584− vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased

585− vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased

590+ nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased

591+ vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

592+ vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

586593 vnRefl = VP (DCon 0 2) eqCon VErased

587594

588− synEqTy = Bind (UN "a") (Pi (TType (UVar (-3))))

589− (Bind (UN "b") (Pi (TType (UVar (-3))))

590− (Bind (UN "x") (Pi (V 1))

591− (Bind (UN "y") (Pi (V 1))

595+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))

596+ (Bind (sUN "b") (Pi (TType (UVar (-3))))

597+ (Bind (sUN "x") (Pi (V 1))

598+ (Bind (sUN "y") (Pi (V 1))

592599 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

593600 [V 3, V 2, V 1, V 0]]))))

594601 elabSynEq

595− = do let synEq = UN "prim__syntactic_eq"

602+ = do let synEq = sUN "prim__syntactic_eq"

596603

597604 updateContext (addOperator synEq synEqTy 4 p_synEq)

598605 setTotality synEq (Total [])

@@ -630,7 +637,7 @@ elabProvider info syn fc n ty tm

630637 -- Execute the type provider and normalise the result

631638 -- use 'run__provider' to convert to a primitive IO action

632639

633− rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)

640+ rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)

634641 [Erased, e])

635642 let rhs' = normalise ctxt [] rhs

636643 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

@@ -648,9 +655,10 @@ elabProvider info syn fc n ty tm

648655

649656 isProviderOf :: TT Name -> TT Name -> Bool

650657 isProviderOf tp prov

651− | (P _ (UN "IO") _, [prov']) <- unApply prov

652− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'

653− , tp == tp' = True

658+ | (P _ (UN io) _, [prov']) <- unApply prov

659+ , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'

660+ , tp == tp', io == txt "IO"

661+ , prov == txt "Provider" && provs == txt "Providers" = True

654662 isProviderOf _ _ = False

655663

656664-- | Elaborate a type provider

@@ -660,8 +668,8 @@ elabTransform info fc safe lhs_in rhs_in

660668 i <- getIState

661669 let lhs = addImplPat i lhs_in

662670 ((lhs', dlhs, []), _) <-

663− tclift $ elaborate ctxt (MN 0 "transLHS") infP []

664− (erun fc (buildTC i info True [] (UN "transform")

671+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

672+ (erun fc (buildTC i info True [] (sUN "transform")

665673 (infTerm lhs)))

666674 let lhs_tm = orderPats (getInferTerm lhs')

667675 let lhs_ty = getInferType lhs'

@@ -671,10 +679,10 @@ elabTransform info fc safe lhs_in rhs_in

671679 logLvl 3 ("Transform LHS " ++ show clhs_tm)

672680 let rhs = addImplBound i (map fst newargs) rhs_in

673681 ((rhs', defer), _) <-

674− tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []

682+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

675683 (do pbinds lhs_tm

676684 setNextName

677− erun fc (build i info False [] (UN "transform") rhs)

685+ erun fc (build i info False [] (sUN "transform") rhs)

678686 erun fc $ psolve lhs_tm

679687 tt <- get_term

680688 return (runState (collectDeferred Nothing tt) []))

@@ -744,18 +752,18 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

744752 getRecTy (PPi _ n ty s) = getRecTy s

745753 getRecTy t = t

746754

747− rec = MN 0 "rec"

755+ rec = sMN 0 "rec"

748756

749− mkp (UN n) = MN 0 ("p_" ++ n)

750− mkp (MN i n) = MN i ("p_" ++ n)

757+ mkp (UN n) = sMN 0 ("p_" ++ str n)

758+ mkp (MN i n) = sMN i ("p_" ++ str n)

751759 mkp (NS n s) = NS (mkp n) s

752760

753− mkImp (UN n) = UN ("implicit_" ++ n)

754− mkImp (MN i n) = MN i ("implicit_" ++ n)

761+ mkImp (UN n) = sUN ("implicit_" ++ str n)

762+ mkImp (MN i n) = sMN i ("implicit_" ++ str n)

755763 mkImp (NS n s) = NS (mkImp n) s

756764

757− mkType (UN n) = UN ("set_" ++ n)

758− mkType (MN i n) = MN i ("set_" ++ n)

765+ mkType (UN n) = sUN ("set_" ++ str n)

766+ mkType (MN i n) = sMN i ("set_" ++ str n)

759767 mkType (NS n s) = NS (mkType n) s

760768

761769 mkProj recty substs cimp ((pn_in, pty), pos)

@@ -778,11 +786,11 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

778786

779787 mkUpdate recty k num ((pn, pty), pos)

780788 = do let setname = expandNS syn $ mkType pn

781− let valname = MN 0 "updateval"

789+ let valname = sMN 0 "updateval"

782790 let pt = k (PPi expl pn pty

783791 (PPi expl rec recty recty))

784792 let pfnTy = PTy "" defaultSyntax fc [] setname pt

785− let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]

793+ let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

786794 let lhsArgs = pls

787795 let rhsArgs = take pos pls ++ (PRef fc valname) :

788796 drop (pos + 1) pls

@@ -1145,7 +1153,7 @@ elabPE info fc caller r =

11451153 _ -> error "Can't happen (getSpecTy)"

11461154

11471155 getSpecClause ist (n, args)

1148− = let newnm = UN ("__"++show (nsroot n) ++ "_" ++

1156+ = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++

11491157 showSep "_" (map showArg args)) in

11501158 -- UN (show n ++ show (map snd args)) in

11511159 (n, newnm, mkPE_TermDecl ist newnm n args)

@@ -1170,8 +1178,8 @@ elabValBind info aspat tm_in

11701178 ((tm', defer, is), _) <-

11711179-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

11721180-- (build i info aspat (MN 0 "val") tm))

1173− tclift (elaborate ctxt (MN 0 "val") infP []

1174− (build i info aspat [Reflection] (MN 0 "val") (infTerm tm)))

1181+ tclift (elaborate ctxt (sMN 0 "val") infP []

1182+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

11751183 let vtm = orderPats (getInferTerm tm')

11761184

11771185 def' <- checkDef (fileFC "(input)") defer

@@ -1201,7 +1209,7 @@ checkPossible info fc tcgen fname lhs_in

12011209 i <- getIState

12021210 let lhs = addImpl i lhs_in

12031211 -- if the LHS type checks, it is possible

1204− case elaborate ctxt (MN 0 "patLHS") infP []

1212+ case elaborate ctxt (sMN 0 "patLHS") infP []

12051213 (erun fc (buildTC i info True [] fname (infTerm lhs))) of

12061214 OK ((lhs', _, _), _) ->

12071215 do let lhs_tm = orderPats (getInferTerm lhs')

@@ -1256,7 +1264,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

12561264 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

12571265

12581266 ((lhs', dlhs, []), _) <-

1259− tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1267+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

12601268 (errAt "left hand side of " fname

12611269 (erun fc (buildTC i info True opts fname (infTerm lhs))))

12621270 let lhs_tm = orderPats (getInferTerm lhs')

@@ -1300,7 +1308,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

13001308 ctxt <- getContext -- new context with where block added

13011309 logLvl 5 "STARTING CHECK"

13021310 ((rhs', defer, is), _) <-

1303− tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

1311+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

13041312 (do pbinds lhs_tm

13051313 setNextName

13061314 (_, _, is) <- errAt "right hand side of " fname

@@ -1436,7 +1444,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

14361444 let lhs = addImplPat i (stripLinear i lhs_in)

14371445 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

14381446 ((lhs', dlhs, []), _) <-

1439− tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1447+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

14401448 (errAt "left hand side of with in " fname

14411449 (erun fc (buildTC i info True opts fname (infTerm lhs))) )

14421450 let lhs_tm = orderPats (getInferTerm lhs')

@@ -1450,7 +1458,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

14501458 logLvl 5 ("Checking " ++ showImp Nothing True False wval)

14511459 -- Elaborate wval in this context

14521460 ((wval', defer, is), _) <-

1453− tclift $ elaborate ctxt (MN 0 "withRHS")

1461+ tclift $ elaborate ctxt (sMN 0 "withRHS")

14541462 (bindTyArgs PVTy bargs infP) []

14551463 (do pbinds lhs_tm

14561464 setNextName

@@ -1483,11 +1491,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

14831491 let wargtype = getRetTy cwvaltyN

14841492 logLvl 5 ("Abstract over " ++ show wargval)

14851493 let wtype = bindTyArgs Pi (bargs_pre ++

1486− (MN 0 "warg", wargtype) :

1487− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)

1488− (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)

1494+ (sMN 0 "warg", wargtype) :

1495+ map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

1496+ (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

14891497 logLvl 3 ("New function type " ++ show wtype)

1490− let wname = MN windex (show fname)

1498+ let wname = sMN windex (show fname)

14911499

14921500 let imps = getImps wtype -- add to implicits context

14931501 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

@@ -1515,7 +1523,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

15151523 ctxt <- getContext -- New context with block added

15161524 i <- getIState

15171525 ((rhs', defer, is), _) <-

1518− tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

1526+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

15191527 (do pbinds lhs_tm

15201528 setNextName

15211529 (_, d, is) <- erun fc (build i info False opts fname rhs)

@@ -1596,7 +1604,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

15961604 FC -> [PTerm] ->

15971605 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

15981606elabClass info syn doc fc constraints tn ps ds

1599− = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1607+ = do let cn = sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

16001608 let tty = pibind ps PType

16011609 let constraint = PApp fc (PRef fc tn)

16021610 (map (pexp . PRef fc) (map fst ps))

@@ -1657,7 +1665,7 @@ elabClass info syn doc fc constraints tn ps ds

16571665

16581666 impbind [] x = x

16591667 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

1660− conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

1668+ conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

16611669 conbind [] x = x

16621670

16631671 getMName (PTy _ _ _ _ n _) = nsroot n

@@ -1681,7 +1689,7 @@ elabClass info syn doc fc constraints tn ps ds

16811689 _ -> ifail $ show n ++ " is not a method"

16821690 defdecl _ _ _ = ifail "Can't happen (defdecl)"

16831691

1684− defaultdec (UN n) = UN ("default#" ++ n)

1692+ defaultdec (UN n) = sUN ("default#" ++ str n)

16851693 defaultdec (NS n ns) = NS (defaultdec n) ns

16861694

16871695 tydecl (PTy _ _ _ _ _ _) = True

@@ -1693,13 +1701,13 @@ elabClass info syn doc fc constraints tn ps ds

16931701

16941702 -- Generate a function for chasing a dictionary constraint

16951703 cfun cn c syn all con

1696− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)

1704+ = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

16971705 -- SN (ParentN cn (show con))

1698− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

1706+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

16991707 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

17001708 let lhs = PApp fc (PRef fc cfn) [pconst capp]

17011709 let rhs = PResolveTC (fileFC "HACK")

1702− let ty = PPi constraint (MN 0 "pc") c con

1710+ let ty = PPi constraint (sMN 0 "pc") c con

17031711 iLOG (showImp Nothing True False ty)

17041712 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

17051713 i <- getIState

@@ -1719,10 +1727,10 @@ elabClass info syn doc fc constraints tn ps ds

17191727 -- dictionary (this is inlinable, always)

17201728 tfun cn c syn all (m, (doc, o, ty))

17211729 = do let ty' = insertConstraint c ty

1722− let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

1730+ let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

17231731 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

17241732 let margs = getMArgs ty

1725− let anames = map (\x -> MN x "arg") [0..]

1733+ let anames = map (\x -> sMN x "arg") [0..]

17261734 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

17271735 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

17281736 iLOG (showImp Nothing True False ty)

@@ -1751,7 +1759,7 @@ elabClass info syn doc fc constraints tn ps ds

17511759

17521760 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

17531761 = PPi p n ty (insertConstraint c sc)

1754− insertConstraint c sc = PPi constraint (MN 0 "class") c sc

1762+ insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

17551763

17561764 -- make arguments explicit and don't bind class parameters

17571765 toExp ns e (PPi (Imp l s _ p) n ty sc)

@@ -1834,7 +1842,7 @@ elabInstance info syn fc cs n ps t expn ds

18341842

18351843 mkiname n' ps' expn' =

18361844 case expn' of

1837− Nothing -> SN (InstanceN n' (map show ps'))

1845+ Nothing -> SN (sInstanceN n' (map show ps'))

18381846 Just nm -> nm

18391847

18401848 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

@@ -1882,14 +1890,14 @@ elabInstance info syn fc cs n ps t expn ds

18821890 mkMethApp (n, _, _, ty)

18831891 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

18841892 lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'

1885− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

1893+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

18861894 lamBind i (PPi _ n ty sc) sc'

1887− = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

1895+ = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

18881896 lamBind i _ sc = sc

18891897 methArgs i (PPi (Imp _ _ _ _) n ty sc)

1890− = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1898+ = PImp 0 True False n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

18911899 methArgs i (PPi (Exp _ _ _ _) n ty sc)

1892− = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1900+ = PExp 0 False (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

18931901 methArgs i (PPi (Constraint _ _ _) n ty sc)

18941902 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

18951903 methArgs i _ = []

@@ -1912,14 +1920,14 @@ elabInstance info syn fc cs n ps t expn ds

19121920

19131921 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

19141922

1915− conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

1923+ conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

19161924 conbind [] x = x

19171925

19181926 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

19191927 coninsert cs sc = conbind cs sc

19201928

19211929 insertDefaults :: IState -> Name ->

1922− [(Name, (Name, PDecl))] -> [String] ->

1930+ [(Name, (Name, PDecl))] -> [T.Text] ->

19231931 [PDecl] -> [PDecl]

19241932 insertDefaults i iname [] ns ds = ds

19251933 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds

src/Idris/ElabTerm.hs+103−99

@@ -173,18 +173,18 @@ elab ist info pattern opts fn tm

173173 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

174174 = do g <- goal; resolveTC 5 g fn ist

175175 elab' ina (PResolveTC fc)

176− | True = do c <- getNameFrom (MN 0 "class")

176+ | True = do c <- getNameFrom (sMN 0 "class")

177177 instanceArg c

178178 | otherwise = do g <- goal

179179 try (resolveTC 2 g fn ist)

180− (do c <- getNameFrom (MN 0 "class")

180+ (do c <- getNameFrom (sMN 0 "class")

181181 instanceArg c)

182182 elab' ina (PRefl fc t)

183− = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "A") Placeholder True,

184− pimp (MN 0 "x") t False])

183+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

184+ pimp (sMN 0 "x") t False])

185185 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

186− [pimp (MN 0 "A") Placeholder True,

187− pimp (MN 0 "B") Placeholder False,

186+ [pimp (sMN 0 "A") Placeholder True,

187+ pimp (sMN 0 "B") Placeholder False,

188188 pexp l, pexp r])

189189 elab' ina@(_, a, inty) (PPair fc l r)

190190 = do hnf_compute

@@ -193,8 +193,8 @@ elab ist info pattern opts fn tm

193193 TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)

194194 [pexp l,pexp r])

195195 _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)

196− [pimp (MN 0 "A") Placeholder True,

197− pimp (MN 0 "B") Placeholder True,

196+ [pimp (sMN 0 "A") Placeholder True,

197+ pimp (sMN 0 "B") Placeholder True,

198198 pexp l, pexp r])

199199 elab' ina (PDPair fc l@(PRef _ n) t r)

200200 = case t of

@@ -209,12 +209,12 @@ elab ist info pattern opts fn tm

209209 [pexp t,

210210 pexp (PLam n Placeholder r)])

211211 asValue = elab' ina (PApp fc (PRef fc existsCon)

212− [pimp (MN 0 "a") t False,

213− pimp (MN 0 "P") Placeholder True,

212+ [pimp (sMN 0 "a") t False,

213+ pimp (sMN 0 "P") Placeholder True,

214214 pexp l, pexp r])

215215 elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)

216− [pimp (MN 0 "a") t False,

217− pimp (MN 0 "P") Placeholder True,

216+ [pimp (sMN 0 "a") t False,

217+ pimp (sMN 0 "P") Placeholder True,

218218 pexp l, pexp r])

219219 elab' ina (PAlternative True as)

220220 = do hnf_compute

@@ -274,7 +274,7 @@ elab ist info pattern opts fn tm

274274 elab' ina@(_, a, inty) (PLam n ty sc)

275275 = do hsin <- get_holes

276276 ptmin <- get_term

277− tyn <- getNameFrom (MN 0 "lamty")

277+ tyn <- getNameFrom (sMN 0 "lamty")

278278 checkPiGoal n

279279 claim tyn RType

280280 explicit tyn

@@ -290,9 +290,9 @@ elab ist info pattern opts fn tm

290290 elabE (True, a, inty) sc

291291 solve

292292 elab' ina@(_, a, _) (PPi _ n Placeholder sc)

293− = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve

293+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve

294294 elab' ina@(_, a, _) (PPi _ n ty sc)

295− = do attack; tyn <- getNameFrom (MN 0 "ty")

295+ = do attack; tyn <- getNameFrom (sMN 0 "ty")

296296 claim tyn RType

297297 n' <- case n of

298298 MN _ _ -> unique_hole n

@@ -304,9 +304,9 @@ elab ist info pattern opts fn tm

304304 solve

305305 elab' ina@(_, a, inty) (PLet n ty val sc)

306306 = do attack;

307− tyn <- getNameFrom (MN 0 "letty")

307+ tyn <- getNameFrom (sMN 0 "letty")

308308 claim tyn RType

309− valn <- getNameFrom (MN 0 "letval")

309+ valn <- getNameFrom (sMN 0 "letval")

310310 claim valn (Var tyn)

311311 explicit valn

312312 letbind n (Var tyn) (Var valn)

@@ -327,9 +327,9 @@ elab ist info pattern opts fn tm

327327 elab' ina@(_, a, inty) (PGoal fc r n sc) = do

328328 rty <- goal

329329 attack

330− tyn <- getNameFrom (MN 0 "letty")

330+ tyn <- getNameFrom (sMN 0 "letty")

331331 claim tyn RType

332− valn <- getNameFrom (MN 0 "letval")

332+ valn <- getNameFrom (sMN 0 "letval")

333333 claim valn (Var tyn)

334334 letbind n (Var tyn) (Var valn)

335335 focus valn

@@ -348,7 +348,7 @@ elab ist info pattern opts fn tm

348348 -- new function name

349349 env <- get_env

350350 argTys <- claimArgTys env args

351− fn <- getNameFrom (MN 0 "inf_fn")

351+ fn <- getNameFrom (sMN 0 "inf_fn")

352352 let fty = fnTy argTys rty

353353-- trace (show (ptm, map fst argTys)) $ focus fn

354354 -- build and defer the function application

@@ -362,8 +362,8 @@ elab ist info pattern opts fn tm

362362 ans <- claimArgTys env xs

363363 return ((n, (False, forget nty)) : ans)

364364 claimArgTys env (_ : xs)

365− = do an <- getNameFrom (MN 0 "inf_argTy")

366− aval <- getNameFrom (MN 0 "inf_arg")

365+ = do an <- getNameFrom (sMN 0 "inf_argTy")

366+ aval <- getNameFrom (sMN 0 "inf_arg")

367367 claim an RType

368368 claim aval (Var an)

369369 ans <- claimArgTys env xs

@@ -383,7 +383,7 @@ elab ist info pattern opts fn tm

383383 mkN n@(NS _ _) = n

384384 mkN n@(SN _) = n

385385 mkN n = case namespace info of

386− Just xs@(_:_) -> NS n xs

386+ Just xs@(_:_) -> sNS n xs

387387 _ -> n

388388

389389 elab' ina (PMatchApp fc fn)

@@ -467,7 +467,7 @@ elab ist info pattern opts fn tm

467467 do attack; defer n'; solve

468468 where mkN n@(NS _ _) = n

469469 mkN n = case namespace info of

470− Just xs@(_:_) -> NS n xs

470+ Just xs@(_:_) -> sNS n xs

471471 _ -> n

472472 elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts

473473 elab' ina (PTactics ts)

@@ -476,11 +476,11 @@ elab ist info pattern opts fn tm

476476 elab' ina (PElabError e) = fail (pshow ist e)

477477 elab' ina (PRewrite fc r sc newg)

478478 = do attack

479− tyn <- getNameFrom (MN 0 "rty")

479+ tyn <- getNameFrom (sMN 0 "rty")

480480 claim tyn RType

481− valn <- getNameFrom (MN 0 "rval")

481+ valn <- getNameFrom (sMN 0 "rval")

482482 claim valn (Var tyn)

483− letn <- getNameFrom (MN 0 "rewrite_rule")

483+ letn <- getNameFrom (sMN 0 "rewrite_rule")

484484 letbind letn (Var tyn) (Var valn)

485485 focus valn

486486 elab' ina r

@@ -495,11 +495,11 @@ elab ist info pattern opts fn tm

495495 solve

496496 where doEquiv t sc =

497497 do attack

498− tyn <- getNameFrom (MN 0 "ety")

498+ tyn <- getNameFrom (sMN 0 "ety")

499499 claim tyn RType

500− valn <- getNameFrom (MN 0 "eqval")

500+ valn <- getNameFrom (sMN 0 "eqval")

501501 claim valn (Var tyn)

502− letn <- getNameFrom (MN 0 "equiv_val")

502+ letn <- getNameFrom (sMN 0 "equiv_val")

503503 letbind letn (Var tyn) (Var valn)

504504 focus tyn

505505 elab' ina t

@@ -509,10 +509,10 @@ elab ist info pattern opts fn tm

509509 solve

510510 elab' ina@(_, a, inty) c@(PCase fc scr opts)

511511 = do attack

512− tyn <- getNameFrom (MN 0 "scty")

512+ tyn <- getNameFrom (sMN 0 "scty")

513513 claim tyn RType

514− valn <- getNameFrom (MN 0 "scval")

515− scvn <- getNameFrom (MN 0 "scvar")

514+ valn <- getNameFrom (sMN 0 "scval")

515+ scvn <- getNameFrom (sMN 0 "scvar")

516516 claim valn (Var tyn)

517517 letbind scvn (Var tyn) (Var valn)

518518 focus valn

@@ -538,7 +538,7 @@ elab ist info pattern opts fn tm

538538-- mkCaseName (MN i x) = MN i (x ++ "_case")

539539 mkN n@(NS _ _) = n

540540 mkN n = case namespace info of

541− Just xs@(_:_) -> NS n xs

541+ Just xs@(_:_) -> sNS n xs

542542 _ -> n

543543 elab' ina (PUnifyLog t) = do unifyLog True

544544 elab' ina t

@@ -618,8 +618,8 @@ elab ist info pattern opts fn tm

618618 = elabArgs ina failed fc r ns args

619619 elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

620620 | lazy && not pattern

621− = do elabArg n (PApp bi (PRef bi (UN "lazy"))

622− [pimp (UN "a") Placeholder True,

621+ = do elabArg n (PApp bi (PRef bi (sUN "lazy"))

622+ [pimp (sUN "a") Placeholder True,

623623 pexp t]);

624624 | otherwise = elabArg n t

625625 where elabArg n t

@@ -699,9 +699,9 @@ findInstances ist t

699699 | otherwise = []

700700

701701trivial' ist

702− = trivial (elab ist toplevel False [] (MN 0 "tac")) ist

702+ = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

703703proofSearch' ist top n hints

704− = proofSearch (elab ist toplevel False [] (MN 0 "tac")) top n hints ist

704+ = proofSearch (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

705705

706706

707707resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

@@ -737,12 +737,15 @@ resolveTC depth topg fn ist

737737

738738 -- HACK! Rather than giving a special name, better to have some kind

739739 -- of flag in ClassInfo structure

740− chaser (UN ('@':'@':_)) = True -- old way

740+ chaser (UN nm)

741+ | ('@':'@':_) <- str nm = True -- old way

741742 chaser (SN (ParentN _ _)) = True

742743 chaser (NS n _) = chaser n

743744 chaser _ = False

744745

745− needsDefault t num@(P _ (NS (UN "Num") ["Classes","Prelude"]) _) [P Bound a _]

746+ numclass = sNS (sUN "Num") ["Classes","Prelude"]

747+

748+ needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass

746749 = do focus a

747750 fill (RConstant (AType (ATInt ITBig))) -- default Integer

748751 solve

@@ -830,7 +833,7 @@ runTac autoSolve ist tac

830833 where

831834 bname (Bind n _ _) = Just n

832835 bname _ = Nothing

833− runT (Exact tm) = do elab ist toplevel False [] (MN 0 "tac") tm

836+ runT (Exact tm) = do elab ist toplevel False [] (sMN 0 "tac") tm

834837 when autoSolve solveAll

835838 runT (MatchRefine fn)

836839 = do fnimps <-

@@ -870,27 +873,27 @@ runTac autoSolve ist tac

870873 when autoSolve solveAll

871874 runT (Equiv tm) -- let bind tm, then

872875 = do attack

873− tyn <- getNameFrom (MN 0 "ety")

876+ tyn <- getNameFrom (sMN 0 "ety")

874877 claim tyn RType

875− valn <- getNameFrom (MN 0 "eqval")

878+ valn <- getNameFrom (sMN 0 "eqval")

876879 claim valn (Var tyn)

877− letn <- getNameFrom (MN 0 "equiv_val")

880+ letn <- getNameFrom (sMN 0 "equiv_val")

878881 letbind letn (Var tyn) (Var valn)

879882 focus tyn

880− elab ist toplevel False [] (MN 0 "tac") tm

883+ elab ist toplevel False [] (sMN 0 "tac") tm

881884 focus valn

882885 when autoSolve solveAll

883886 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

884887 = do attack; -- (h:_) <- get_holes

885− tyn <- getNameFrom (MN 0 "rty")

888+ tyn <- getNameFrom (sMN 0 "rty")

886889 -- start_unify h

887890 claim tyn RType

888− valn <- getNameFrom (MN 0 "rval")

891+ valn <- getNameFrom (sMN 0 "rval")

889892 claim valn (Var tyn)

890− letn <- getNameFrom (MN 0 "rewrite_rule")

893+ letn <- getNameFrom (sMN 0 "rewrite_rule")

891894 letbind letn (Var tyn) (Var valn)

892895 focus valn

893− elab ist toplevel False [] (MN 0 "tac") tm

896+ elab ist toplevel False [] (sMN 0 "tac") tm

894897 rewrite (Var letn)

895898 when autoSolve solveAll

896899 runT (Induction nm)

@@ -898,27 +901,27 @@ runTac autoSolve ist tac

898901 when autoSolve solveAll

899902 runT (LetTac n tm)

900903 = do attack

901− tyn <- getNameFrom (MN 0 "letty")

904+ tyn <- getNameFrom (sMN 0 "letty")

902905 claim tyn RType

903− valn <- getNameFrom (MN 0 "letval")

906+ valn <- getNameFrom (sMN 0 "letval")

904907 claim valn (Var tyn)

905908 letn <- unique_hole n

906909 letbind letn (Var tyn) (Var valn)

907910 focus valn

908− elab ist toplevel False [] (MN 0 "tac") tm

911+ elab ist toplevel False [] (sMN 0 "tac") tm

909912 when autoSolve solveAll

910913 runT (LetTacTy n ty tm)

911914 = do attack

912− tyn <- getNameFrom (MN 0 "letty")

915+ tyn <- getNameFrom (sMN 0 "letty")

913916 claim tyn RType

914− valn <- getNameFrom (MN 0 "letval")

917+ valn <- getNameFrom (sMN 0 "letval")

915918 claim valn (Var tyn)

916919 letn <- unique_hole n

917920 letbind letn (Var tyn) (Var valn)

918921 focus tyn

919− elab ist toplevel False [] (MN 0 "tac") ty

922+ elab ist toplevel False [] (sMN 0 "tac") ty

920923 focus valn

921− elab ist toplevel False [] (MN 0 "tac") tm

924+ elab ist toplevel False [] (sMN 0 "tac") tm

922925 when autoSolve solveAll

923926 runT Compute = compute

924927 runT Trivial = do trivial' ist; when autoSolve solveAll

@@ -931,16 +934,16 @@ runTac autoSolve ist tac

931934 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

932935 tgoal <- goal -- store the goal

933936 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

934− script <- getNameFrom (MN 0 "script")

937+ script <- getNameFrom (sMN 0 "script")

935938 claim script scriptTy

936− scriptvar <- getNameFrom (MN 0 "scriptvar" )

939+ scriptvar <- getNameFrom (sMN 0 "scriptvar" )

937940 letbind scriptvar scriptTy (Var script)

938941 focus script

939− elab ist toplevel False [] (MN 0 "tac") tm

942+ elab ist toplevel False [] (sMN 0 "tac") tm

940943 (script', _) <- get_type_val (Var scriptvar)

941944 -- now that we have the script apply

942945 -- it to the reflected goal and context

943− restac <- getNameFrom (MN 0 "restac")

946+ restac <- getNameFrom (sMN 0 "restac")

944947 claim restac tacticTy

945948 focus restac

946949 fill (raw_apply (forget script')

@@ -954,27 +957,27 @@ runTac autoSolve ist tac

954957 let tactic = normalise ctxt env restac'

955958 runReflected tactic

956959 where tacticTy = Var (reflm "Tactic")

957− listTy = Var (NS (UN "List") ["List", "Prelude"])

958− scriptTy = (RBind (UN "__pi_arg")

960+ listTy = Var (sNS (sUN "List") ["List", "Prelude"])

961+ scriptTy = (RBind (sUN "__pi_arg")

959962 (Pi (RApp listTy envTupleType))

960− (RBind (UN "__pi_arg1")

963+ (RBind (sUN "__pi_arg1")

961964 (Pi (Var $ reflm "TT")) tacticTy))

962965 runT (ByReflection tm) -- run the reflection function 'tm' on the

963966 -- goal, then apply the resulting reflected Tactic

964967 = do tgoal <- goal

965968 attack

966− script <- getNameFrom (MN 0 "script")

969+ script <- getNameFrom (sMN 0 "script")

967970 claim script scriptTy

968− scriptvar <- getNameFrom (MN 0 "scriptvar" )

971+ scriptvar <- getNameFrom (sMN 0 "scriptvar" )

969972 letbind scriptvar scriptTy (Var script)

970973 focus script

971974 ptm <- get_term

972− elab ist toplevel False [] (MN 0 "tac")

975+ elab ist toplevel False [] (sMN 0 "tac")

973976 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

974977 (script', _) <- get_type_val (Var scriptvar)

975978 -- now that we have the script apply

976979 -- it to the reflected goal

977− restac <- getNameFrom (MN 0 "restac")

980+ restac <- getNameFrom (sMN 0 "restac")

978981 claim restac tacticTy

979982 focus restac

980983 fill (forget script')

@@ -990,28 +993,28 @@ runTac autoSolve ist tac

990993 scriptTy = tacticTy

991994

992995 runT (Reflect v) = do attack -- let x = reflect v in ...

993− tyn <- getNameFrom (MN 0 "letty")

996+ tyn <- getNameFrom (sMN 0 "letty")

994997 claim tyn RType

995− valn <- getNameFrom (MN 0 "letval")

998+ valn <- getNameFrom (sMN 0 "letval")

996999 claim valn (Var tyn)

997− letn <- getNameFrom (MN 0 "letvar")

1000+ letn <- getNameFrom (sMN 0 "letvar")

9981001 letbind letn (Var tyn) (Var valn)

9991002 focus valn

1000− elab ist toplevel False [] (MN 0 "tac") v

1003+ elab ist toplevel False [] (sMN 0 "tac") v

10011004 (value, _) <- get_type_val (Var letn)

10021005 ctxt <- get_context

10031006 env <- get_env

10041007 let value' = hnf ctxt env value

10051008 runTac autoSolve ist (Exact $ PQuote (reflect value'))

10061009 runT (Fill v) = do attack -- let x = fill x in ...

1007− tyn <- getNameFrom (MN 0 "letty")

1010+ tyn <- getNameFrom (sMN 0 "letty")

10081011 claim tyn RType

1009− valn <- getNameFrom (MN 0 "letval")

1012+ valn <- getNameFrom (sMN 0 "letval")

10101013 claim valn (Var tyn)

1011− letn <- getNameFrom (MN 0 "letvar")

1014+ letn <- getNameFrom (sMN 0 "letvar")

10121015 letbind letn (Var tyn) (Var valn)

10131016 focus valn

1014− elab ist toplevel False [] (MN 0 "tac") v

1017+ elab ist toplevel False [] (sMN 0 "tac") v

10151018 (value, _) <- get_type_val (Var letn)

10161019 ctxt <- get_context

10171020 env <- get_env

@@ -1021,7 +1024,7 @@ runTac autoSolve ist tac

10211024 runT (GoalType n tac) = do g <- goal

10221025 case unApply g of

10231026 (P _ n' _, _) ->

1024− if nsroot n' == UN n

1027+ if nsroot n' == sUN n

10251028 then runT tac

10261029 else fail "Wrong goal type"

10271030 _ -> fail "Wrong goal type"

@@ -1034,7 +1037,7 @@ runTac autoSolve ist tac

10341037

10351038-- | Prefix a name with the "Language.Reflection" namespace

10361039reflm :: String -> Name

1037−reflm n = NS (UN n) ["Reflection", "Language"]

1040+reflm n = sNS (sUN n) ["Reflection", "Language"]

10381041

10391042

10401043-- | Reify tactics from their reflected representation

@@ -1056,7 +1059,7 @@ reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist

10561059reifyApp ist t [Constant (Str n), x]

10571060 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

10581061reifyApp _ t [Constant (Str n)]

1059− | t == reflm "Intro" = return $ Intro [UN n]

1062+ | t == reflm "Intro" = return $ Intro [sUN n]

10601063reifyApp ist t [t']

10611064 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

10621065reifyApp ist t [t']

@@ -1147,13 +1150,13 @@ reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

11471150

11481151reifyTTNameApp :: Name -> [Term] -> ElabD Name

11491152reifyTTNameApp t [Constant (Str n)]

1150− | t == reflm "UN" = return $ UN n

1153+ | t == reflm "UN" = return $ sUN n

11511154reifyTTNameApp t [n, ns]

11521155 | t == reflm "NS" = do n' <- reifyTTName n

11531156 ns' <- reifyTTNamespace ns

1154− return $ NS n' ns'

1157+ return $ sNS n' ns'

11551158reifyTTNameApp t [Constant (I i), Constant (Str n)]

1156− | t == reflm "MN" = return $ MN i n

1159+ | t == reflm "MN" = return $ sMN i n

11571160reifyTTNameApp t []

11581161 | t == reflm "NErased" = return NErased

11591162reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

@@ -1162,9 +1165,9 @@ reifyTTNamespace :: Term -> ElabD [String]

11621165reifyTTNamespace t@(App _ _)

11631166 = case unApply t of

11641167 (P _ f _, [Constant StrType])

1165− | f == NS (UN "Nil") ["List", "Prelude"] -> return []

1168+ | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

11661169 (P _ f _, [Constant StrType, Constant (Str n), ns])

1167− | f == NS (UN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)

1170+ | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)

11681171 _ -> fail ("Unknown reflection namespace arg: " ++ show t)

11691172reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

11701173

@@ -1286,19 +1289,19 @@ reflectNameType (TCon x y)

12861289 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

12871290

12881291reflectName :: Name -> Raw

1289−reflectName (UN str)

1290− = reflCall "UN" [RConstant (Str str)]

1292+reflectName (UN s)

1293+ = reflCall "UN" [RConstant (Str (str s))]

12911294reflectName (NS n ns)

12921295 = reflCall "NS" [ reflectName n

12931296 , foldr (\ n s ->

1294− raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )

1297+ raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )

12951298 [ RConstant StrType, RConstant (Str n), s ])

1296− ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )

1299+ ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )

12971300 [ RConstant StrType ])

1298− ns

1301+ (map str ns)

12991302 ]

13001303reflectName (MN i n)

1301− = reflCall "MN" [RConstant (I i), RConstant (Str n)]

1304+ = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]

13021305reflectName (NErased) = Var (reflm "NErased")

13031306reflectName n = Var (reflm "NErased") -- special name, not yet implemented

13041307

@@ -1355,7 +1358,7 @@ reflectEnv = foldr consToEnvList emptyEnvList

13551358 where

13561359 consToEnvList :: (Name, Binder Term) -> Raw -> Raw

13571360 consToEnvList (n, b) l

1358− = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))

1361+ = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))

13591362 [ envTupleType

13601363 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

13611364 , (RApp (Var $ reflm "Binder")

@@ -1367,19 +1370,19 @@ reflectEnv = foldr consToEnvList emptyEnvList

13671370 ]

13681371

13691372 emptyEnvList :: Raw

1370− emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))

1373+ emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

13711374 [envTupleType]

13721375

13731376-- | Reflect an error into the internal datatype of Idris -- TODO

13741377rawBool :: Bool -> Raw

1375−rawBool True = Var (NS (UN "True") ["Bool", "Prelude"])

1376−rawBool False = Var (NS (UN "False") ["Bool", "Prelude"])

1378+rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

1379+rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

13771380

13781381rawNil :: Raw -> Raw

1379−rawNil ty = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"])) [ty]

1382+rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]

13801383

13811384rawCons :: Raw -> Raw -> Raw -> Raw

1382−rawCons ty hd tl = raw_apply (Var (NS (UN "::") ["List", "Prelude"])) [ty, hd, tl]

1385+rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]

13831386

13841387rawList :: Raw -> [Raw] -> Raw

13851388rawList ty = foldr (rawCons ty) (rawNil ty)

@@ -1445,7 +1448,7 @@ reflectErr (NotInjective t1 t2 t3) =

14451448reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

14461449reflectErr (CantResolveAlts ss) =

14471450 raw_apply (Var $ reflErrName "CantResolve")

1448− [rawList (Var $ (UN "String")) (map (RConstant . Str) ss)]

1451+ [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

14491452reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

14501453reflectErr UniverseError = Var $ reflErrName "UniverseError"

14511454reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

@@ -1470,7 +1473,7 @@ reflectErr (ProviderError str) =

14701473 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

14711474reflectErr (LoadingFailed str err) =

14721475 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

1473−reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

1476+reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

14741477

14751478withErrorReflection :: Idris a -> Idris a

14761479withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

@@ -1504,11 +1507,12 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

15041507 parts -> ReflectionError errorparts e

15051508

15061509 fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1507− fromTTMaybe (App (App (P (DCon _ _) (NS (UN "Just") _) _) ty) tm) = Just tm

1510+ fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1511+ | just == txt "Just" = Just tm

15081512 fromTTMaybe x = Nothing

15091513

15101514reflErrName :: String -> Name

1511−reflErrName n = NS (UN n) ["Errors", "Reflection", "Language"]

1515+reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

15121516

15131517reifyReportPart :: Term -> Idris ErrorReportPart

15141518reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

src/Idris/IBC.hs+8−1

@@ -14,6 +14,8 @@ import Data.Binary

1414import Data.Vector.Binary

1515import Data.List

1616import Data.ByteString.Lazy as B hiding (length, elem, map)

17+import qualified Data.Text as T

18+

1719import Control.Monad

1820import Control.Monad.State hiding (get, put)

1921import qualified Control.Monad.State as ST

@@ -26,7 +28,7 @@ import Debug.Trace

2628import Paths_idris

2729

2830ibcVersion :: Word8

29−ibcVersion = 53

31+ibcVersion = 54

3032

3133data IBCFile = IBCFile { ver :: Word8,

3234 sourcefile :: FilePath,

@@ -498,6 +500,11 @@ instance Binary Name where

498500 return (SymRef x1)

499501 _ -> error "Corrupted binary data for Name"

500502

503+instance Binary T.Text where

504+ put x = put (str x)

505+ get = do x <- get

506+ return (txt x)

507+

501508instance Binary SpecialName where

502509 put x

503510 = case x of

src/Idris/ParseData.hs+1−1

@@ -144,7 +144,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

144144 mkPApp fc t [] = t

145145 mkPApp fc t xs = PApp fc t (map pexp xs)

146146 bindArgs :: [PTerm] -> PTerm -> PTerm

147− bindArgs xs t = foldr (PPi expl (MN 0 "_t")) t xs

147+ bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

148148 combineDataOpts :: DataOpts -> DataOpts

149149 combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts

150150

src/Idris/ParseExpr.hs+26−26

@@ -295,7 +295,7 @@ simpleExpr syn =

295295 fc <- getFC

296296 return (modifyConst syn fc (PConstant c)))

297297 <|> try (do symbol "'"; fc <- getFC; str <- name

298− return (PApp fc (PRef fc (UN "Symbol_"))

298+ return (PApp fc (PRef fc (sUN "Symbol_"))

299299 [pexp (PConstant (Str (show str)))]))

300300 <|> do fc <- getFC

301301 x <- fnName

@@ -360,12 +360,12 @@ bracketed syn =

360360 l <- expr' syn

361361 o <- operator

362362 lchar ')'

363− return $ PLam (MN 1000 "ARG") Placeholder

364− (PApp fc0 (PRef fc0 (UN o)) [pexp l,

365− pexp (PRef fc0 (MN 1000 "ARG"))]))

363+ return $ PLam (sMN 1000 "ARG") Placeholder

364+ (PApp fc0 (PRef fc0 (sUN o)) [pexp l,

365+ pexp (PRef fc0 (sMN 1000 "ARG"))]))

366366 <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

367− return $ PLam (MN 1000 "ARG") Placeholder

368− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),

367+ return $ PLam (sMN 1000 "ARG") Placeholder

368+ (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

369369 pexp e]))

370370 <|> try (do ln <- name; lchar ':'

371371 lty <- expr syn

@@ -388,7 +388,7 @@ modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

388388modifyConst syn fc (PConstant (BI x))

389389 | not (inPattern syn)

390390 = PAlternative False

391− (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]

391+ (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]

392392 : consts)

393393 | otherwise = PAlternative False consts

394394 where

@@ -420,8 +420,8 @@ listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lc

420420 <?> "list expression"

421421 where

422422 mkList :: FC -> [PTerm] -> PTerm

423− mkList fc [] = PRef fc (UN "Nil")

424− mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]

423+ mkList fc [] = PRef fc (sUN "Nil")

424+ mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

425425

426426

427427{- | Parses an alternative expression

@@ -466,10 +466,10 @@ matchApp syn = do ty <- simpleExpr syn

466466 symbol "<=="

467467 fc <- getFC

468468 f <- fnName

469− return (PLet (MN 0 "match")

469+ return (PLet (sMN 0 "match")

470470 ty

471471 (PMatchApp fc f)

472− (PRef fc (MN 0 "match")))

472+ (PRef fc (sMN 0 "match")))

473473 <?> "matching application expression"

474474

475475{- | Parses a unification log expression

@@ -512,12 +512,12 @@ app syn = do f <- reserved "mkForeign"

512512 i <- get

513513 -- mkForeign f args ==>

514514 -- liftPrimIO (\w => mkForeignPrim f args w)

515− let ap = PApp fc (PRef fc (UN "liftPrimIO"))

516− [pexp (PLam (MN 0 "w")

515+ let ap = PApp fc (PRef fc (sUN "liftPrimIO"))

516+ [pexp (PLam (sMN 0 "w")

517517 Placeholder

518− (PApp fc (PRef fc (UN "mkForeignPrim"))

518+ (PApp fc (PRef fc (sUN "mkForeignPrim"))

519519 (fn : args ++

520− [pexp (PRef fc (MN 0 "w"))])))]

520+ [pexp (PRef fc (sMN 0 "w"))])))]

521521 return (dslify i ap)

522522

523523 <|> do f <- simpleExpr syn

@@ -611,8 +611,8 @@ recordType syn

611611 rec <- optional (simpleExpr syn)

612612 case rec of

613613 Nothing ->

614− return (PLam (MN 0 "fldx") Placeholder

615− (applyAll fc fields (PRef fc (MN 0 "fldx"))))

614+ return (PLam (sMN 0 "fldx") Placeholder

615+ (applyAll fc fields (PRef fc (sMN 0 "fldx"))))

616616 Just v -> return (applyAll fc fields v)

617617 <?> "record setting expression"

618618 where fieldType :: IdrisParser (Name, PTerm)

@@ -628,8 +628,8 @@ recordType syn

628628

629629-- | Creates setters for record types on necessary functions

630630mkType :: Name -> Name

631−mkType (UN n) = UN ("set_" ++ n)

632−mkType (MN 0 n) = MN 0 ("set_" ++ n)

631+mkType (UN n) = sUN ("set_" ++ str n)

632+mkType (MN 0 n) = sMN 0 ("set_" ++ str n)

633633mkType (NS n s) = NS (mkType n) s

634634

635635{- | Parses a type signature

@@ -645,7 +645,7 @@ TypeExpr ::= ConstraintList? Expr;

645645typeExpr :: SyntaxInfo -> IdrisParser PTerm

646646typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

647647 sc <- expr syn

648− return (bindList (PPi constraint) (map (\x -> (MN 0 "constrarg", x)) cs) sc)

648+ return (bindList (PPi constraint) (map (\x -> (sMN 0 "constrarg", x)) cs) sc)

649649 <?> "type signature"

650650

651651{- | Parses a lambda expression

@@ -678,8 +678,8 @@ lambda syn = do lchar '\\'

678678 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

679679 pmList [] sc = sc

680680 pmList ((i, (fc, x)) : xs) sc

681− = PLam (MN i "lamp") Placeholder

682− (PCase fc (PRef fc (MN i "lamp"))

681+ = PLam (sMN i "lamp") Placeholder

682+ (PCase fc (PRef fc (sMN i "lamp"))

683683 [(x, pmList xs sc)])

684684

685685{- | Parses a term rewrite expression

@@ -696,7 +696,7 @@ rewriteTerm syn = do reserved "rewrite"

696696 giving <- optional (do symbol "==>"; expr' syn)

697697 reserved "in"; sc <- expr syn

698698 return (PRewrite fc

699− (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc

699+ (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

700700 giving)

701701 <?> "term rewrite expression"

702702

@@ -861,7 +861,7 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

861861 where nameOrPlaceholder :: IdrisParser Name

862862 nameOrPlaceholder = fnName

863863 <|> do symbol "_"

864− return (MN 0 "underscore")

864+ return (sMN 0 "underscore")

865865 <?> "name or placeholder"

866866

867867{- | Parses a list comprehension

@@ -885,11 +885,11 @@ comprehension syn

885885 qs <- sepBy1 (do_ syn) (lchar ',')

886886 lchar ']'

887887 return (PDoBlock (map addGuard qs ++

888− [DoExp fc (PApp fc (PRef fc (UN "return"))

888+ [DoExp fc (PApp fc (PRef fc (sUN "return"))

889889 [pexp pat])]))

890890 <?> "list comprehension"

891891 where addGuard :: PDo -> PDo

892− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))

892+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

893893 [pexp e])

894894 addGuard x = x

895895

src/Idris/ParseHelpers.hs+2−2

@@ -230,8 +230,8 @@ initsEndAt p (x:xs) | p x = [] : x_inits_xs

230230 namespace.

231231-}

232232mkName :: (String, String) -> Name

233−mkName (n, "") = UN n

234−mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

233+mkName (n, "") = sUN n

234+mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))

235235 where parseNS x = case span (/= '.') x of

236236 (x, "") -> [x]

237237 (x, '.':y) -> x : parseNS y

src/Idris/ParseOps.hs+5−5

@@ -33,21 +33,21 @@ import qualified Data.ByteString.UTF8 as UTF8

3333-- using pre-build and user-defined operator/fixity declarations

3434table :: [FixDecl] -> OperatorTable IdrisParser PTerm

3535table fixes

36− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

37− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

36+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (sUN "-"))

37+ [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

3838 ++ toTable (reverse fixes) ++

3939 [[backtick],

4040 [binary "=" PEq AssocLeft],

41− [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

41+ [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]

4242

4343-- | Calculates table for fixtiy declarations

4444toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

4545toTable fs = map (map toBin)

4646 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

4747 where toBin (Fix (PrefixN _) op) = prefix op

48− (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])

48+ (\fc x -> PApp fc (PRef fc (sUN op)) [pexp x])

4949 toBin (Fix f op)

50− = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)

50+ = binary op (\fc x y -> PApp fc (PRef fc (sUN op)) [pexp x,pexp y]) (assoc f)

5151 assoc (Infixl _) = AssocLeft

5252 assoc (Infixr _) = AssocRight

5353 assoc (InfixN _) = AssocNone

src/Idris/Parser.hs+9−9

@@ -300,9 +300,9 @@ fnDecl' syn = checkFixity $

300300 getName (PTy _ _ _ _ n _) = Just n

301301 getName _ = Nothing

302302 fixityOK (NS n _) = fixityOK n

303− fixityOK (UN n) | all (flip elem opChars) n =

303+ fixityOK (UN n) | all (flip elem opChars) (str n) =

304304 do fixities <- fmap idris_infixes get

305− return . elem n . map (\ (Fix _ op) -> op) $ fixities

305+ return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities

306306 | otherwise = return True

307307 fixityOK _ = return True

308308

@@ -517,7 +517,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

517517 cn <- name

518518 args <- many (simpleExpr syn)

519519 let sc = PApp fc (PRef fc cn) (map pexp args)

520− let t = bindList (PPi constraint) (map (\x -> (MN 0 "constraint", x)) cs) sc

520+ let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc

521521 ds <- option [] (instanceBlock syn)

522522 return [PInstance syn fc cs cn args t en ds]

523523 <?> "instance declaration"

@@ -575,7 +575,7 @@ Pattern ::= Clause;

575575pattern :: SyntaxInfo -> IdrisParser PDecl

576576pattern syn = do fc <- getFC

577577 clause <- clause syn

578− return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later

578+ return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later

579579 <?> "pattern"

580580

581581{- | Parse a constant applicative form declaration

@@ -617,7 +617,7 @@ rhs syn n = do lchar '='; expr syn

617617 <|> do reserved "impossible"; return PImpossible

618618 <?> "function right hand side"

619619 where mkN :: Name -> Name

620− mkN (UN x) = UN (x++"_lemma_1")

620+ mkN (UN x) = sUN (str x++"_lemma_1")

621621 mkN (NS x n) = NS (mkN x) n

622622 n' :: Name

623623 n' = mkN n

@@ -625,7 +625,7 @@ rhs syn n = do lchar '='; expr syn

625625 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)

626626 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)

627627 where addLetC (l, r) = (l, addLet nm r)

628− addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))

628+ addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))

629629

630630{- |Parses a function clause

631631RHSOrWithBlock ::= RHS WhereOrTerminator

@@ -679,10 +679,10 @@ clause syn

679679 return x,

680680 do terminator

681681 return ([], [])]

682− let capp = PLet (MN 0 "match")

682+ let capp = PLet (sMN 0 "match")

683683 ty

684684 (PMatchApp fc n)

685− (PRef fc (MN 0 "match"))

685+ (PRef fc (sMN 0 "match"))

686686 ist <- get

687687 put (ist { lastParse = Just n })

688688 return $ PClause fc n capp [] r wheres

@@ -693,7 +693,7 @@ clause syn

693693 when (op == "=" || op == "?=" ) $

694694 fail "infix clause definition with \"=\" and \"?=\" not supported "

695695 return (l, op))

696− let n = expandNS syn (UN op)

696+ let n = expandNS syn (sUN op)

697697 r <- argExpr syn

698698 fc <- getFC

699699 wargs <- many (wExpr syn)

src/Idris/PartialEval.hs+2−2

@@ -54,7 +54,7 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

5454 sc' <- unifyEq xs sc

5555 return (Bind n (Pi t) sc')

5656 unifyEq xs t = do args <- get

57− put (args ++ (zip xs (repeat (UN "_"))))

57+ put (args ++ (zip xs (repeat (sUN "_"))))

5858 return t

5959

6060mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

@@ -122,7 +122,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

122122 | x && imparg imp = (ImplicitS, tm)

123123 | x = (ExplicitS, tm)

124124 | imparg imp = (ImplicitD, tm)

125− | otherwise = (ExplicitD, (P Ref (UN (show n ++ "arg")) Erased))

125+ | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126126

127127 imparg (PExp _ _ _ _) = False

128128 imparg _ = True

src/Idris/Primitives.hs+50−50

@@ -26,7 +26,7 @@ data Prim = Prim { p_name :: Name,

2626

2727ty :: [Const] -> Const -> Type

2828ty [] x = Constant x

29−ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)

29+ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t)) (ty ts x)

3030

3131total, partial :: Totality

3232total = Total []

@@ -94,83 +94,83 @@ primitives =

9494 iCoerce ITNative (ITFixed IT64) "trunc" trunc LTrunc,

9595 iCoerce ITBig ITChar "trunc" trunc LTrunc,

9696

97− Prim (UN "prim__addFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (+))

97+ Prim (sUN "prim__addFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (+))

9898 (2, LPlus ATFloat) total,

99− Prim (UN "prim__subFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (-))

99+ Prim (sUN "prim__subFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (-))

100100 (2, LMinus ATFloat) total,

101− Prim (UN "prim__mulFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (*))

101+ Prim (sUN "prim__mulFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (*))

102102 (2, LTimes ATFloat) total,

103− Prim (UN "prim__divFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (/))

103+ Prim (sUN "prim__divFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (/))

104104 (2, LSDiv ATFloat) total,

105− Prim (UN "prim__eqFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (==))

105+ Prim (sUN "prim__eqFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (==))

106106 (2, LEq ATFloat) total,

107− Prim (UN "prim__sltFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<))

107+ Prim (sUN "prim__sltFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<))

108108 (2, LSLt ATFloat) total,

109− Prim (UN "prim__slteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<=))

109+ Prim (sUN "prim__slteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<=))

110110 (2, LSLe ATFloat) total,

111− Prim (UN "prim__sgtFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>))

111+ Prim (sUN "prim__sgtFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>))

112112 (2, LSGt ATFloat) total,

113− Prim (UN "prim__sgteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>=))

113+ Prim (sUN "prim__sgteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>=))

114114 (2, LSGe ATFloat) total,

115− Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

115+ Prim (sUN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

116116 (2, LStrConcat) total,

117− Prim (UN "prim__eqString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (==))

117+ Prim (sUN "prim__eqString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (==))

118118 (2, LStrEq) total,

119− Prim (UN "prim__ltString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (<))

119+ Prim (sUN "prim__ltString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (<))

120120 (2, LStrLt) total,

121− Prim (UN "prim_lenString") (ty [StrType] (AType (ATInt ITNative))) 1 (p_strLen)

121+ Prim (sUN "prim_lenString") (ty [StrType] (AType (ATInt ITNative))) 1 (p_strLen)

122122 (1, LStrLen) total,

123123 -- Conversions

124− Prim (UN "prim__charToInt") (ty [(AType (ATInt ITChar))] (AType (ATInt ITNative))) 1 (c_charToInt)

124+ Prim (sUN "prim__charToInt") (ty [(AType (ATInt ITChar))] (AType (ATInt ITNative))) 1 (c_charToInt)

125125 (1, LChInt ITNative) total,

126− Prim (UN "prim__intToChar") (ty [(AType (ATInt ITNative))] (AType (ATInt ITChar))) 1 (c_intToChar)

126+ Prim (sUN "prim__intToChar") (ty [(AType (ATInt ITNative))] (AType (ATInt ITChar))) 1 (c_intToChar)

127127 (1, LIntCh ITNative) total,

128− Prim (UN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)

128+ Prim (sUN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)

129129 (1, LStrFloat) total,

130− Prim (UN "prim__floatToStr") (ty [(AType ATFloat)] StrType) 1 (c_floatToStr)

130+ Prim (sUN "prim__floatToStr") (ty [(AType ATFloat)] StrType) 1 (c_floatToStr)

131131 (1, LFloatStr) total,

132132

133− Prim (UN "prim__floatExp") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatExp)

133+ Prim (sUN "prim__floatExp") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatExp)

134134 (1, LFExp) total,

135− Prim (UN "prim__floatLog") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatLog)

135+ Prim (sUN "prim__floatLog") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatLog)

136136 (1, LFLog) total,

137− Prim (UN "prim__floatSin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSin)

137+ Prim (sUN "prim__floatSin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSin)

138138 (1, LFSin) total,

139− Prim (UN "prim__floatCos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCos)

139+ Prim (sUN "prim__floatCos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCos)

140140 (1, LFCos) total,

141− Prim (UN "prim__floatTan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatTan)

141+ Prim (sUN "prim__floatTan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatTan)

142142 (1, LFTan) total,

143− Prim (UN "prim__floatASin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatASin)

143+ Prim (sUN "prim__floatASin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatASin)

144144 (1, LFASin) total,

145− Prim (UN "prim__floatACos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatACos)

145+ Prim (sUN "prim__floatACos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatACos)

146146 (1, LFACos) total,

147− Prim (UN "prim__floatATan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatATan)

147+ Prim (sUN "prim__floatATan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatATan)

148148 (1, LFATan) total,

149− Prim (UN "prim__floatSqrt") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSqrt)

149+ Prim (sUN "prim__floatSqrt") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSqrt)

150150 (1, LFSqrt) total,

151− Prim (UN "prim__floatFloor") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatFloor)

151+ Prim (sUN "prim__floatFloor") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatFloor)

152152 (1, LFFloor) total,

153− Prim (UN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)

153+ Prim (sUN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)

154154 (1, LFCeil) total,

155155

156− Prim (UN "prim__strHead") (ty [StrType] (AType (ATInt ITChar))) 1 (p_strHead)

156+ Prim (sUN "prim__strHead") (ty [StrType] (AType (ATInt ITChar))) 1 (p_strHead)

157157 (1, LStrHead) partial,

158− Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

158+ Prim (sUN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

159159 (1, LStrTail) partial,

160− Prim (UN "prim__strCons") (ty [(AType (ATInt ITChar)), StrType] StrType) 2 (p_strCons)

160+ Prim (sUN "prim__strCons") (ty [(AType (ATInt ITChar)), StrType] StrType) 2 (p_strCons)

161161 (2, LStrCons) total,

162− Prim (UN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] (AType (ATInt ITChar))) 2 (p_strIndex)

162+ Prim (sUN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] (AType (ATInt ITChar))) 2 (p_strIndex)

163163 (2, LStrIndex) partial,

164− Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

164+ Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

165165 (1, LStrRev) total,

166− Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

166+ Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

167167 (1, LReadStr) partial,

168− Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

168+ Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

169169 (0, LVMPtr) total,

170170 -- Streams

171− Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

171+ Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172172 (0, LStdIn) partial,

173− Prim (UN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

173+ Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

174174 (0, LNullPtr) total

175175 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

176176 ++ concatMap vecOps vecTypes

@@ -221,13 +221,13 @@ intArith ity =

221221

222222intConv :: IntTy -> [Prim]

223223intConv ity =

224− [ Prim (UN $ "prim__toStr" ++ intTyName ity) (ty [AType . ATInt $ ity] StrType) 1 intToStr

224+ [ Prim (sUN $ "prim__toStr" ++ intTyName ity) (ty [AType . ATInt $ ity] StrType) 1 intToStr

225225 (1, LIntStr ity) total

226− , Prim (UN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (AType . ATInt $ ity)) 1 (strToInt ity)

226+ , Prim (sUN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (AType . ATInt $ ity)) 1 (strToInt ity)

227227 (1, LStrInt ity) total

228− , Prim (UN $ "prim__toFloat" ++ intTyName ity) (ty [AType . ATInt $ ity] (AType ATFloat)) 1 intToFloat

228+ , Prim (sUN $ "prim__toFloat" ++ intTyName ity) (ty [AType . ATInt $ ity] (AType ATFloat)) 1 intToFloat

229229 (1, LIntFloat ity) total

230− , Prim (UN $ "prim__fromFloat" ++ intTyName ity) (ty [AType ATFloat] (AType . ATInt $ ity)) 1 (floatToInt ity)

230+ , Prim (sUN $ "prim__fromFloat" ++ intTyName ity) (ty [AType ATFloat] (AType . ATInt $ ity)) 1 (floatToInt ity)

231231 (1, LFloatInt ity) total

232232 ]

233233

@@ -246,13 +246,13 @@ vecCmps ity =

246246

247247vecOps :: IntTy -> [Prim]

248248vecOps ity@(ITVec elem count) =

249− [ Prim (UN $ "prim__mk" ++ intTyName ity)

249+ [ Prim (sUN $ "prim__mk" ++ intTyName ity)

250250 (ty (replicate count . AType . ATInt . ITFixed $ elem) (AType . ATInt $ ity))

251251 count (mkVecCon elem count) (count, LMkVec elem count) total

252− , Prim (UN $ "prim__index" ++ intTyName ity)

252+ , Prim (sUN $ "prim__index" ++ intTyName ity)

253253 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32))] (AType . ATInt . ITFixed $ elem))

254254 2 (mkVecIndex count) (2, LIdxVec elem count) partial -- TODO: Ensure this reduces

255− , Prim (UN $ "prim__update" ++ intTyName ity)

255+ , Prim (sUN $ "prim__update" ++ intTyName ity)

256256 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32)), AType . ATInt . ITFixed $ elem]

257257 (AType . ATInt $ ity))

258258 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces

@@ -260,7 +260,7 @@ vecOps ity@(ITVec elem count) =

260260

261261bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim

262262bitcastPrim from to impl prim =

263− Prim (UN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)

263+ Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)

264264 (1, prim) total

265265

266266vecBitcasts :: [IntTy] -> [Prim]

@@ -377,23 +377,23 @@ intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show cou

377377

378378iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

379379iCmp ity op self impl irop totality

380− = Prim (UN $ "prim__" ++ op ++ intTyName ity)

380+ = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

381381 (ty (replicate 2 . AType . ATInt $ ity) (AType (ATInt (if self then ity else ITNative))))

382382 2 impl (2, irop ity) totality

383383

384384iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

385385iBinOp ity op impl irop totality

386− = Prim (UN $ "prim__" ++ op ++ intTyName ity)

386+ = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

387387 (ty (replicate 2 . AType . ATInt $ ity) (AType . ATInt $ ity))

388388 2 impl (2, irop ity) totality

389389iUnOp ity op impl irop totality

390− = Prim (UN $ "prim__" ++ op ++ intTyName ity)

390+ = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

391391 (ty [AType . ATInt $ ity] (AType . ATInt $ ity))

392392 1 impl (1, irop ity) totality

393393

394394iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim

395395iCoerce from to op impl irop =

396− Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

396+ Prim (sUN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

397397 (ty [AType . ATInt $ from] (AType . ATInt $ to)) 1 (impl from to) (1, irop from to) total

398398

399399fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const

src/Idris/Prover.hs+2−1

@@ -102,7 +102,8 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d

102102 tPretty t = pretty $ delab ist t

103103

104104 prettyPs [] = empty

105− prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs

105+ prettyPs ((MN _ r, _) : bs)

106+ | r == txt "rewrite_rule" = prettyPs bs

106107 prettyPs ((n, Let t v) : bs) =

107108 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>

108109 tPretty t $$ prettyPs bs)

src/Idris/Providers.hs+14−7

@@ -11,17 +11,24 @@ import Debug.Trace

1111

1212-- | Wrap a type provider in the type of type providers

1313providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]

14+providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 False tm ""]

15+

16+ioret = sUN "prim_io_return"

17+ermod = sNS (sUN "Error") ["Providers"]

18+prmod = sNS (sUN "Provide") ["Providers"]

1519

1620-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

1721getProvided :: TT Name -> Idris (TT Name)

18−getProvided tm | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm

19− , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =

20− case err of

22+getProvided tm | (P _ pioret _, [tp, result]) <- unApply tm

23+ , (P _ nm _, [_, err]) <- unApply result

24+ , pioret == ioret && nm == ermod

25+ = case err of

2126 Constant (Str msg) -> ierror . ProviderError $ msg

2227 _ -> ifail "Internal error in type provider, non-normalised error"

23− | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm

24− , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =

25− return res

28+ | (P _ pioret _, [tp, result]) <- unApply tm

29+ , (P _ nm _, [_, res]) <- unApply result

30+ , pioret == ioret && nm == prmod

31+ = return res

2632 | otherwise = ifail $ "Internal type provider error: result was not " ++

2733 "IO (Provider a), or perhaps missing normalisation."

34+

src/Idris/REPL.hs+15−15

@@ -247,19 +247,19 @@ ideslave orig mods

247247 Just x -> iPrintError $ "didn't load " ++ filename

248248 ideslave orig [filename]

249249 Just (IdeSlave.TypeOf name) ->

250− process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

250+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (sUN name)))

251251 Just (IdeSlave.CaseSplit line name) ->

252− process stdout fn (CaseSplitAt False line (UN name))

252+ process stdout fn (CaseSplitAt False line (sUN name))

253253 Just (IdeSlave.AddClause line name) ->

254− process stdout fn (AddClauseFrom False line (UN name))

254+ process stdout fn (AddClauseFrom False line (sUN name))

255255 Just (IdeSlave.AddProofClause line name) ->

256− process stdout fn (AddProofClauseFrom False line (UN name))

256+ process stdout fn (AddProofClauseFrom False line (sUN name))

257257 Just (IdeSlave.AddMissing line name) ->

258− process stdout fn (AddMissing False line (UN name))

258+ process stdout fn (AddMissing False line (sUN name))

259259 Just (IdeSlave.MakeWithBlock line name) ->

260− process stdout fn (MakeWith False line (UN name))

260+ process stdout fn (MakeWith False line (sUN name))

261261 Just (IdeSlave.ProofSearch line name hints) ->

262− process stdout fn (DoProofSearch False line (UN name) (map UN hints))

262+ process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

263263 Nothing -> do iPrintError "did not understand")

264264 (\e -> do iPrintError $ show e))

265265 (\e -> do iPrintError $ show e)

@@ -408,7 +408,7 @@ edit f orig

408408 , idris_colourTheme = idris_colourTheme i

409409 }

410410 loadInputs stdout [f]

411− clearOrigPats

411+-- clearOrigPats

412412 iucheck

413413 return ()

414414 where getEditor env | Just ed <- lookup "EDITOR" env = ed

@@ -444,7 +444,7 @@ process h fn (Eval t)

444444 let tm' = force (normaliseAll ctxt [] tm)

445445 let ty' = force (normaliseAll ctxt [] ty)

446446 -- Add value to context, call it "it"

447− updateContext (addCtxtDef (UN "it") (Function ty' tm'))

447+ updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

448448 ist <- getIState

449449 logLvl 3 $ "Raw: " ++ show (tm', ty')

450450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

@@ -485,7 +485,7 @@ process h fn (Check (PRef _ n))

485485 = let current = " " ++

486486 (case n of

487487 MN _ _ -> "_"

488− UN ('_':'_':_) -> "_"

488+ UN nm | ('_':'_':_) <- str nm -> "_"

489489 _ -> showName (Just ist) [] False c n) ++

490490 " : " ++ showImp (Just ist) imp c t ++ "\n"

491491 in

@@ -852,8 +852,8 @@ process h fn (TestInline t)

852852process h fn Execute

853853 = do (m, _) <- elabVal toplevel False

854854 (PApp fc

855− (PRef fc (UN "run__IO"))

856− [pexp $ PRef fc (NS (UN "main") ["Main"])])

855+ (PRef fc (sUN "run__IO"))

856+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

857857-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

858858 (tmpn, tmph) <- runIO tempfile

859859 runIO $ hClose tmph

@@ -864,8 +864,8 @@ process h fn Execute

864864 where fc = fileFC "main"

865865process h fn (Compile codegen f)

866866 = do (m, _) <- elabVal toplevel False

867− (PApp fc (PRef fc (UN "run__IO"))

868− [pexp $ PRef fc (NS (UN "main") ["Main"])])

867+ (PApp fc (PRef fc (sUN "run__IO"))

868+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

869869 compile codegen f m

870870 where fc = fileFC "main"

871871process h fn (LogLvl i) = setLogLevel i

@@ -1221,7 +1221,7 @@ idrisMain opts =

12211221 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

12221222

12231223 when (runrepl && not idesl) $ do

1224− clearOrigPats

1224+-- clearOrigPats

12251225 initScript

12261226 startServer orig inputs

12271227 runInputT (replSettings (Just historyFile)) $ repl orig inputs

src/Idris/Transforms.hs+3−3

@@ -39,8 +39,8 @@ instance Transform CaseAlt where

3939

4040natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]

4141

42−zname = NS (UN "Z") ["Nat","Prelude"]

43−sname = NS (UN "S") ["Nat","Prelude"]

42+zname = sNS (sUN "Z") ["Nat","Prelude"]

43+sname = sNS (sUN "S") ["Nat","Prelude"]

4444

4545zero :: TT Name -> TT Name

4646zero (P _ n _) | n == zname

@@ -49,7 +49,7 @@ zero x = x

4949

5050suc :: TT Name -> TT Name

5151suc (App (P _ s _) a) | s == sname

52− = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]

52+ = mkApp (P Ref (sUN "prim__addBigInt") Erased) [Constant (BI 1), a]

5353suc x = x

5454

5555natcase :: SC -> SC

src/Pkg/PParser.hs+1−1

@@ -27,7 +27,7 @@ data PkgDesc = PkgDesc { pkgname :: String,

2727 }

2828 deriving Show

2929

30−defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (UN "") Nothing

30+defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing

3131

3232parseDesc :: FilePath -> IO PkgDesc

3333parseDesc fp = do p <- readFile fp

src/Pkg/Package.hs+3−3

@@ -108,8 +108,8 @@ testLib warn p f

108108rmIBC :: Name -> IO ()

109109rmIBC m = rmFile $ toIBCFile m

110110

111−toIBCFile (UN n) = n ++ ".ibc"

112−toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : ns))

111+toIBCFile (UN n) = str n ++ ".ibc"

112+toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))

113113

114114installIBC :: String -> Name -> IO ()

115115installIBC p m = do let f = toIBCFile m

@@ -120,7 +120,7 @@ installIBC p m = do let f = toIBCFile m

120120 copyFile f (destdir </> takeFileName f)

121121 return ()

122122 where getDest (UN n) = ""

123− getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : ns))

123+ getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

124124

125125installObj :: String -> String -> IO ()

126126installObj p o = do d <- getTargetDir