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

git.iko.soy/Idris-dev

on master help sign in

Use Data.Text for variable names

46e894dEdwin Brady13 years ago

src/IRTS/CodegenC.hs+1−1

compare with master

unifiedsplit

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

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

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

446

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 ++ "))"

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

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

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

src/IRTS/CodegenJava.hs+5−5

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

369 | otherwise = decls

370 where

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

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

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

373 findMain (_:decls) = findMain decls

374 findMain [] = False

375

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

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

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

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

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

379 findMainMethod (_:decls) = findMainMethod decls

380 findMainMethod [] = False

381

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

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

391 , jConst "args"

392 ]

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

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

394 ]

395

396-----------------------------------------------------------------------

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

749

750mkThread :: LVar -> CodeGeneration Exp

751mkThread arg =

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

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

753

754

src/IRTS/CodegenJavaScript.hs+12−10

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

606 mainFun = jsTailcall $ jsCall runMain []

607

608 runMain :: String

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

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

610

611 invokeLoop :: String

612 invokeLoop = compileJS $ jsCall "main" []

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

671

672translateNamespace :: Name -> String

673translateNamespace (UN _) = idrNamespace

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

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

675translateNamespace (MN _ _) = idrNamespace

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

677translateNamespace NErased = idrNamespace

678

679translateName :: Name -> String

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

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

681translateName (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

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

684translateName NErased = "e"

685

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

688 | WhereN i m n <- name =

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

690 | InstanceN n s <- name =

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

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

692 | ParentN n s <- name =

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

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

694 | MethodN n <- name =

695 'm' : translateName n

696 | CaseN n <- name =

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

714

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

716translateDeclaration (path, SFun name params stackSize body)

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

717+ | (MN _ ap) <- name

718 , (SLet var val next) <- body

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

719+ , (SChkCase cvar cases) <- next

720+ , ap == txt "APPLY" =

720 let lvar = translateVariableName var

721 let lvar = translateVariableName var

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

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

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

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

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

735 )

736 )

736 ]

737 ]

737

738

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

739+ | (MN _ ev) <- name

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

740+ , (SChkCase var cases) <- body

741+ , ev == txt "EVAL" =

740 JSSeq [ lookupTable [] var cases

742 JSSeq [ lookupTable [] var cases

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

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

742 JSTernary (

744 JSTernary (

src/IRTS/Compiler.hs+34−31

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

40 = do checkMVs

41 let tmnames = namesUsed (STerm tm)

42 usedIn <- mapM (allNames []) tmnames

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

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

44 defsIn <- mkDecls tm (concat used)

45 findUnusedArgs (concat used)

46 maindef <- irMain tm

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

49 flags <- getFlags codegen

50 hdrs <- getHdrs codegen

51 impdirs <- allImportDirs

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

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

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

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

55 let ctxtIn = addAlist tagged emptyContext

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

108

109irMain :: TT Name -> Idris LDecl

110irMain tm = do i <- ir tm

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

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

112

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

114mkDecls t used

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

137 = do i <- getIState

138 case lookup n (idris_scprims i) of

139 Just (ar, op) ->

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

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

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

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

143 _ -> do def <- mkLDecl n d

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

168instance ToIR (TT Name) where

169 ir tm = ir' [] tm where

170 ir' env tm@(App f a)

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

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

172+ m == txt "mkForeignPrim"

172 = doForeign env args

173 = doForeign env args

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

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

175+ u == txt "unsafePerformPrimIO"

174 = ir' env arg

176 = ir' env arg

175 -- TMP HACK - until we get inlining.

177 -- TMP HACK - until we get inlining.

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

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

179+ r == txt "replace"

177 = ir' env arg

180 = ir' env arg

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

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

182+ l == txt "lazy"

179 = do arg' <- ir' env arg

183 = do arg' <- ir' env arg

180 return $ LLazyExp arg'

184 return $ LLazyExp arg'

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

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

186+ a == txt "assert_smaller"

182 = ir' env arg

187 = ir' env arg

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

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

189+ p == txt "par"

184 = do arg' <- ir' env arg

190 = do arg' <- ir' env arg

185 return $ LOp LPar [LLazyExp arg']

191 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"

187 = do arg' <- ir' env arg

194 = do arg' <- ir' env arg

188 return $ LOp LFork [LLazyExp arg']

195 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"

201 = do size' <- ir' env size

198 = do size' <- ir' env size

202 t' <- ir' env t

199 t' <- ir' env t

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

200 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"

205 = do t' <- ir' env t

203 = do t' <- ir' env t

206 return t' -- TODO

204 return t' -- TODO

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

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

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

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

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

273 return $ LLam extra sc'

271 return $ LLam extra sc'

274

272

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

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

276

274

277 buildApp env e [] = return e

275 buildApp env e [] = return e

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

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

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

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

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

301 _ -> Nothing

299 _ -> Nothing

302

300

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

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

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

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

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

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

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

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

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

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

307mkIty' _ = FAny

310mkIty' _ = FAny

308

311

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

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

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

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

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

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

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

339

342

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

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

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

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

342

345

343instance ToIR ([Name], SC) where

346instance ToIR ([Name], SC) where

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

347 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)

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

144

145 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

147

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

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

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

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

172 needsEval x _ = False

173

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

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

175

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

177 | ApplyCase a

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

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

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

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

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

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

202 : mkApplyCase fname (n + 1) ar

203

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

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

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

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

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

207 (mapMaybe evalCase xs ++

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

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

209 where

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

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

211 evalCase _ = Nothing

212

213mkApply :: [(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"]

215 (case mapMaybe applyCase xs of

216 [] -> DNothing

217 cases ->

218− mkBigCase (MN 0 "APPLY") 256

218+ mkBigCase (sMN 0 "APPLY") 256

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

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

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

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

221 (cases ++

222 [DDefaultCase DNothing])))

223 where

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

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

232

233

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

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

235

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

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

237mkUnderCon n 0 = n

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

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

239

240instance Show DExp where

241 show e = show' [] e where

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

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

26 where

27 prefixCallNamespacesExp :: Ident -> SExp -> SExp

28 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

30 prefixCallNamespacesExp name (SLet var e1 e2) =

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

32 prefixCallNamespacesExp name (SUpdate var e) =

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

63 . parser ident

64 . (prefix ++)

65 . cleanNonLetter

66− $ cleanWs False name

66+ $ cleanWs False (str name)

67 where

68 cleanNonLetter (x:xs)

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

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

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

97 | otherwise = x : (cleanWs False xs)

98 cleanWs _ [] = []

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

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

100

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

102mangle = mangleWithPrefix "__IDRCG__"

src/IRTS/Lang.hs+1−1

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

102

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

104lname (UN n) i = MN i n

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

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

106

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

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

src/IRTS/Simplified.hs+1−1

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

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

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

96 i <- hvar

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

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

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

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

src/Idris/AbsSyntax.hs+34−31

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

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

181

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

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

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

184getNameHints i n =

185 case lookupCtxt n (idris_namehints i) of

186 [ns] -> ns

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

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

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

202 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)

204 putIState $ ist { idris_classes = cs }

205 where addI i ins | int = i : ins

206 | chaser n = ins ++ [i]

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

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

210 | otherwise = n : insI i ns

211

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

212+ chaser (UN nm)

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

213 chaser (NS n _) = chaser n

214 chaser (NS n _) = chaser n

214 chaser _ = False

215 chaser _ = False

215

216

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

689

690

690bi = fileFC "builtin"

691bi = fileFC "builtin"

691

692

692−inferTy = MN 0 "__Infer"

693+inferTy = sMN 0 "__Infer"

693−inferCon = MN 0 "__infer"

694+inferCon = sMN 0 "__infer"

694inferDecl = PDatadecl inferTy

695inferDecl = PDatadecl inferTy

695 PType

696 PType

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

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

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

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

698 (PRef bi inferTy)), bi)]

699 (PRef bi inferTy)), bi)]

699inferOpts = []

700inferOpts = []

700

701

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]

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

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

703

704

704getInferTerm, getInferType :: Term -> Term

705getInferTerm, getInferType :: Term -> Term

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

715 falseTy, pairTy, pairCon,

716 falseTy, pairTy, pairCon,

716 eqTy, eqCon, inferTy, inferCon]

717 eqTy, eqCon, inferTy, inferCon]

717

718

718−unitTy = MN 0 "__Unit"

719+unitTy = sMN 0 "__Unit"

719−unitCon = MN 0 "__II"

720+unitCon = sMN 0 "__II"

720unitDecl = PDatadecl unitTy PType

721unitDecl = PDatadecl unitTy PType

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

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

722unitOpts = [DefaultEliminator]

723unitOpts = [DefaultEliminator]

723

724

724−falseTy = MN 0 "__False"

725+falseTy = sMN 0 "__False"

725falseDecl = PDatadecl falseTy PType []

726falseDecl = PDatadecl falseTy PType []

726falseOpts = []

727falseOpts = []

727

728

728−pairTy = MN 0 "__Pair"

729+pairTy = sMN 0 "__Pair"

729−pairCon = MN 0 "__MkPair"

730+pairCon = sMN 0 "__MkPair"

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

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

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

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

732 PPi impl (n "B") PType (

733 PPi impl (n "B") PType (

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

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

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

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

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

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

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

737− where n a = MN 0 a

738+ where n a = sMN 0 a

738pairOpts = []

739pairOpts = []

739

740

740−eqTy = UN "="

741+eqTy = sUN "="

741−eqCon = UN "refl"

742+eqCon = sUN "refl"

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

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

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

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

744 PType)

745 PType)

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

748 pimp (n "B") Placeholder False,

749 pimp (n "B") Placeholder False,

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

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

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

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

751− where n a = MN 0 a

752+ where n a = sMN 0 a

752eqOpts = []

753eqOpts = []

753

754

754−elimName = UN "__Elim"

755+elimName = sUN "__Elim"

755−elimMethElimTy = UN "__elimTy"

756+elimMethElimTy = sUN "__elimTy"

756−elimMethElim = UN "elim"

757+elimMethElim = sUN "elim"

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

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

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

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

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

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

760

761

761-- Defined in builtins.idr

762-- Defined in builtins.idr

762−sigmaTy = UN "Exists"

763+sigmaTy = sUN "Exists"

763−existsCon = UN "Ex_intro"

764+existsCon = sUN "Ex_intro"

764

765

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

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

766piBind = piBindp expl

767piBind = piBindp expl

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

898 updateps yn nm [] = []

899 updateps yn nm [] = []

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

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

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

901 | (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

902

903

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

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

904

905

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

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

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

1038 doAdd (UConstraint c args : cs) ns t

1039 doAdd (UConstraint c args : cs) ns t

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

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

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

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

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

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

1042 | otherwise = doAdd cs ns t

1043 | otherwise = doAdd cs ns t

1043

1044

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

1461 fullApp x = x

1462 fullApp x = x

1462

1463

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1471 | length args == length args'

1474 | length args == length args'

1472 = do mf <- match' f f'

1475 = do mf <- match' f f'

src/Idris/AbsSyntaxTree.hs+21−19

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

156deriving instance NFData CGInfo

157!-}

158

159−primDefs = [UN "unsafePerformPrimIO",

159+primDefs = [sUN "unsafePerformPrimIO",

160− UN "mkLazyForeignPrim",

160+ sUN "mkLazyForeignPrim",

161− UN "mkForeignPrim",

161+ sUN "mkForeignPrim",

162− UN "FalseElim"]

162+ sUN "FalseElim"]

163

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

165data IBCWrite = IBCFix FixDecl

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

844deriving instance NFData SSymbol

845!-}

846

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

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

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

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

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

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

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

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

851 Nothing

852 Nothing

853 Nothing

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

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

884expandNS syn n = case syn_namespace syn of

885 [] -> n

886− xs -> NS n xs

886+ xs -> sNS n xs

887

888

889--- Pretty printing declarations and terms

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

980 prettyBasic n

981 where

982 prettyBasic n@(UN _) = pretty n

983− prettyBasic (MN _ s) = text s

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

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

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

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

986 prettySe p (PLam n ty sc) =

987 bracket p 2 $

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

1052 | not impl = pretty f

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

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

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

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

1056+ | not (tnull nm) &&

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

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

1057 let [l, r] = getExps args in

1058 let [l, r] = getExps args in

1058 bracket p 1 $

1059 bracket p 1 $

1059 if size r > breakingSize then

1060 if size r > breakingSize then

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

1166 Nothing -> showbasic n

1167 Nothing -> showbasic n

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

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

1168 showbasic n@(UN _) = showCG n

1169 showbasic n@(UN _) = showCG n

1169− showbasic (MN _ s) = s

1170+ showbasic (MN _ s) = str s

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

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

1171 showbasic (SN s) = show s

1172 showbasic (SN s) = show s

1172 fst3 (x, _, _) = x

1173 fst3 (x, _, _) = x

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

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

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

1241 | not impl = se p bnd hd

1242 | not impl = se p bnd hd

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

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

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

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

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

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

1246+ | not (tnull nm) &&

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

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

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

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

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

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

1248 se p bnd (PApp _ f as)

1250 se p bnd (PApp _ f as)

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

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

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

1291

1293

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

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

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

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

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

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

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

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

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

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

1297 all isImp imps,

1299 all isImp imps,

1298 Just tl' <- slist' p bnd tl

1300 Just tl' <- slist' p bnd tl

src/Idris/CaseSplit.hs+13−12

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

91 Nothing -> []

92 Just t -> getNameHints ist t

93 let nsupp = case n of

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

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

95+ -> mkSupply (supp ++ varlist)

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

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

96 x -> mkSupply (x : supp)

97 x -> mkSupply (x : supp)

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

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

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

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

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

107 where mkSupply' xs ns' = xs ++ mkSupply ns'

108 where mkSupply' xs ns' = xs ++ mkSupply ns'

108

109

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

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

110

111

111stripNS tm = mapPT dens tm where

112stripNS tm = mapPT dens tm where

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

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

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

164 = case lookupTy n (tt_ctxt ist) of

165 = case lookupTy n (tt_ctxt ist) of

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

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

166 _ -> repeat Nothing

167 _ -> repeat Nothing

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

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

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

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

169 | otherwise = Nothing

170 | otherwise = Nothing

170argTys _ _ = repeat Nothing

171argTys _ _ = repeat Nothing

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

264

265

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

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

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

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

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

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

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

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

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

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

270 nshow t = show t

271 nshow t = show t

271

272

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

296getUniq nm i

297getUniq nm i

297 = do ist <- getIState

298 = do ist <- getIState

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

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

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

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

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

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

301 _ -> getUniq nm (i+1)

302 _ -> getUniq nm (i+1)

302

303

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

324 mkApp i _ _ = ""

325 mkApp i _ _ = ""

325

326

326 getNameFrom i used (PPi _ _ _ _)

327 getNameFrom i used (PPi _ _ _ _)

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

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

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

329 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

330 getNameFrom i used (PRef fc f)

331 getNameFrom i used (PRef fc f)

331 = case getNameHints i f of

332 = case getNameHints i f of

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

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

333 ns -> uniqueNameFrom (mkSupply ns) used

334 ns -> uniqueNameFrom (mkSupply ns) used

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

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

335

336

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

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

337 -> Name -- ^ Function name

338 -> Name -- ^ Function name

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

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

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

364nameMissing ps = do ist <- get

365nameMissing ps = do ist <- get

365 newPats <- mapM nm ps

366 newPats <- mapM nm ps

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

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

367 newPats

368 newPats

368 return (map fst newPats')

369 return (map fst newPats')

369 where

370 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)

371 base t = t

372 base t = t

372

373

373 nm ptm = do mptm <- elabNewPat ptm

374 nm ptm = do mptm <- elabNewPat ptm

src/Idris/Completion.hs+3−3

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

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

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

56nameString :: Name -> Maybe String

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

57+nameString (UN nm)

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

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

59−nameString (UN n) = Just n

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

60nameString (NS n _) = nameString n

61nameString _ = Nothing

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

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

216 then return t

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

218 Error err -> Error (At fc err)

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

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

220 defaultCase True = STerm Erased

221 defaultCase False = UnmatchedCase "Error"

222 fstT (x, _, _) = x

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

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

301 return $ PCon n t args'

302 -- n + 1

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

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

304− [p, Constant (BI 1)]

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

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

306 return $ PSuc p'

307 -- Typecase

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

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

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

335 sc' <- toPat' sc []

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

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

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

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

339 return $ PReflected n args'

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

490 uniq i n = n

491

492getVar :: 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)

494

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

496groupCons cs = gc [] cs

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

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

445

446 mkMN n@(MN i _) = n

447 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)

449 mkMN (NS n xs) = NS (mkMN n) xs

450

451 rebind hs (Bind n t sc)

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

564 = do g <- goal

565 case g of

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

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

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

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

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

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

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

570 claim a RType

571 claim b RType

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

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

578

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

580simple_app fun arg appstr =

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

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

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

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

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

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

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

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

585 claim a RType

586 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))

588 tm <- get_term

589 start_unify s

590 claim s (Var a)

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

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

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

101simplify ctxt env t

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

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

103− (UN "assert_smaller", 0),

103+ (sUN "assert_smaller", 0),

104− (UN "par", 0),

104+ (sUN "par", 0),

105− (UN "prim__syntactic_eq", 0),

105+ (sUN "prim__syntactic_eq", 0),

106− (UN "fork", 0)]

106+ (sUN "fork", 0)]

107 (map finalEntry env) (finalise t)

108 [Simplify]

109 quote 0 val) initEval

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

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

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

113rt_simplify ctxt env t

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

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

115− (UN "assert_smaller", 0),

115+ (sUN "assert_smaller", 0),

116− (UN "par", 0),

116+ (sUN "par", 0),

117− (UN "prim__syntactic_eq", 0),

117+ (sUN "prim__syntactic_eq", 0),

118− (UN "prim_fork", 0)]

118+ (sUN "prim_fork", 0)]

119 (map finalEntry env) (finalise t)

120 [RunTT]

121 quote 0 val) initEval

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

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

191 | Simplify `elem` opts

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

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

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

194 | otherwise = False

195

196 getCases cd | simpl = cases_totcheck cd

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

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

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

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

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

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

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

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

418 chooseAlt _ _ _ alts amap

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

492 = do sc' <- quote i sc

493 t' <- quote i t

494 v' <- quote i v

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

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

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

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

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

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

891lookupDefAcc n mkpublic ctxt

892 = map mkp $ lookupCtxt n (definitions ctxt)

893 -- 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"))

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

896

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

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

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

96toTT (EType u) = return $ TType u

97toTT EErased = return Erased

98toTT (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

100toTT (EHandle _) = return Erased

101

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

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

173 Right tm' -> return tm'

174

175ioWrap :: 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]

177

178ioUnit :: ExecVal

179ioUnit = ioWrap (EP Ref unitCon EErased)

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

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

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

221 newArgs <- mapM argExec (zip args laziness)

222− execApp' env ctxt newF newArgs

222+ res <- execApp' env ctxt newF newArgs

223+ return res

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

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

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

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

225 let argInfo = exec_implicits est

226 let argInfo = exec_implicits est

226 case lookupCtxtName n argInfo of

227 case lookupCtxtName n argInfo of

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

235

236

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

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

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

238execApp' 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 (EP _ fp _) (ty:action:rest)

240+ | fp == upio,

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

239− execApp' env ctxt v rest

242+ = execApp' env ctxt v rest

240−

243+

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

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

245+ | fp == piobind,

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

242 do v'' <- tryForce v'

247 do v'' <- tryForce v'

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

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

244 execApp' env ctxt res rest

249 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 =

246 do v' <- tryForce v

252 do v' <- tryForce v

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

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

248

254

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

255-- 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)

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

257+ | fp == mkfprim,

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

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

252 = do execIO (putStr arg)

259 = do execIO (putStr arg)

253 execApp' env ctxt ioUnit rest

260 execApp' env ctxt ioUnit rest

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

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

262+ | fp == mkfprim,

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

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

256 = do contents <- execIO $ hGetLine h

264 = do contents <- execIO $ hGetLine h

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

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

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

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

267+ | fp == mkfprim,

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

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

260 = do m <- case mode of

269 = do m <- case mode of

261 "r" -> return ReadMode

270 "r" -> return ReadMode

262 "w" -> return WriteMode

271 "w" -> return WriteMode

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

268 h <- execIO $ openFile f m

277 h <- execIO $ openFile f m

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

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

270

279

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

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

281+ | fp == mkfprim,

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

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

273 = do eofp <- execIO $ hIsEOF h

283 = do eofp <- execIO $ hIsEOF h

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

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

275 execApp' env ctxt res (tail rest)

285 execApp' env ctxt res (tail rest)

276

286

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

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

288+ | fp == mkfprim,

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

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

279 = do execIO $ hClose h

290 = do execIO $ hClose h

280 execApp' env ctxt ioUnit (tail rest)

291 execApp' env ctxt ioUnit (tail rest)

281

292

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

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

294+ | fp == mkfprim,

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

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

284 = let res = ioWrap . EConstant . I $

296 = let res = ioWrap . EConstant . I $

285 if p == nullPtr then 1 else 0

297 if p == nullPtr then 1 else 0

286 in execApp' env ctxt res (tail rest)

298 in execApp' env ctxt res (tail rest)

287

299

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

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

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

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

302+ | fp == mkfprim,

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

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

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

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

292 in execApp' env ctxt res (tail rest)

305 in execApp' env ctxt res (tail rest)

293

306

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

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

295

308

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

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

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

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

298− , length xs >= length argTs =

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

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

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

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

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

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

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

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

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

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

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

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

345

358

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+

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

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

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

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

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

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

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

370+getOp fn [EP _ fn' _]

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

350 Just $ do line <- execIO getLine

372 Just $ do line <- execIO getLine

351 return (EConstant (Str line))

373 return (EConstant (Str line))

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

374+getOp fn [EHandle h]

375+ | fn == prs =

353 Just $ do contents <- execIO $ hGetLine h

376 Just $ do contents <- execIO $ hGetLine h

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

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

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

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

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

478 argFTy <- sequence $ map getFTy argTy

501 argFTy <- sequence $ map getFTy argTy

479 retFTy <- getFTy ret

502 retFTy <- getFTy ret

480 return $ FFun name argFTy retFTy

503 return $ FFun name argFTy retFTy

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

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

482

505

483getFTy :: ExecVal -> Maybe FType

506getFTy :: ExecVal -> Maybe FType

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

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

508+ | fi == txt "FIntT" =

485− case intTy of

509+ case str intTy of

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

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

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

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

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

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

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

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

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

492 _ -> Nothing

516 _ -> Nothing

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

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

494− case t of

518+ case str t of

495 "FFloat" -> Just (FArith ATFloat)

519 "FFloat" -> Just (FArith ATFloat)

496 "FString" -> Just FString

520 "FString" -> Just FString

497 "FPtr" -> Just FPtr

521 "FPtr" -> Just FPtr

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

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

159hole (Guess _ _) = True

160hole _ = False

161

162−holeName i = MN i "hole"

162+holeName i = sMN i "hole"

163

164qshow :: Fails -> String

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

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

209getName tag = do ps <- get

210 let n = nextname ps

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

212− return $ MN n tag

212+ return $ sMN n tag

213

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

215action a = do ps <- get

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

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

569 let tmt' = normalise ctxt env tmt

570 case unApply tmt' of

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

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

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

573 let newt = mkP l r l t

574 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)))

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

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

578 return scv

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

580− where rname = MN 0 "replaced"

580+ where rname = sMN 0 "replaced"

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

582

583-- 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

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

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

635 _ -> fail "Unkown type for induction"

636− where scname = MN 0 "scarg"

636+ where scname = sMN 0 "scarg"

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

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

639 bindConsArgs [] v = v

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

642 splitTyArgs param_pos tyargs =

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

644 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) []

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

647 let var = P Bound idnm idxt

648 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(..))

25import Debug.Trace

26import qualified Data.Map.Strict as Map

27import Data.Char

28+import qualified Data.Text as T

28import Data.List

29import Data.List

29import Data.Vector.Unboxed (Vector)

30import Data.Vector.Unboxed (Vector)

30import qualified Data.Vector.Unboxed as V

31import qualified Data.Vector.Unboxed as V

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

240

241

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

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

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

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

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

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

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

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

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

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

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

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

247 | SN SpecialName -- ^ Decorated function names

248 | SN SpecialName -- ^ Decorated function names

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

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

249 deriving (Eq, Ord)

250 deriving (Eq, Ord)

250

251

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+

251{-!

274{-!

252deriving instance Binary Name

275deriving instance Binary Name

253deriving instance NFData Name

276deriving instance NFData Name

254!-}

277!-}

255

278

256data SpecialName = WhereN Int Name Name

279data SpecialName = WhereN Int Name Name

257− | InstanceN Name [String]

280+ | InstanceN Name [T.Text]

258− | ParentN Name String

281+ | ParentN Name T.Text

259 | MethodN Name

282 | MethodN Name

260 | CaseN Name

283 | CaseN Name

261 | ElimN Name

284 | ElimN Name

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

265deriving instance NFData SpecialName

288deriving instance NFData SpecialName

266!-}

289!-}

267

290

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+

268instance Sized Name where

297instance Sized Name where

269 size (UN n) = 1

298 size (UN n) = 1

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

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

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

272 size _ = 1

301 size _ = 1

273

302

274instance Pretty Name where

303instance Pretty Name where

275− pretty (UN n) = text n

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

276 pretty (NS n s) = pretty n

305 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

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

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

279

308

280instance Show Name where

309instance Show Name where

281− show (UN n) = n

310+ show (UN n) = str n

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

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

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

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

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

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

285 show (SN s) = show s

314 show (SN s) = show s

286 show NErased = "_"

315 show NErased = "_"

287

316

288instance Show SpecialName where

317instance Show SpecialName where

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

318 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

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

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

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

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

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

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

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

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

295

324

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

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

297showCG :: Name -> String

326showCG :: Name -> String

298−showCG (UN n) = n

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

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

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

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

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

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

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

302showCG (SN s) = showCG' s

331showCG (SN s) = showCG' s

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

332 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)

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

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

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

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

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

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

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

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

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

318mapCtxt = fmap . fmap

347mapCtxt = fmap . fmap

319

348

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

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

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

321tcname (NS n _) = tcname n

351tcname (NS n _) = tcname n

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

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

323tcname (SN (MethodN _)) = True

353tcname (SN (MethodN _)) = True

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

325tcname _ = False

355tcname _ = False

326

356

327implicitable (NS n _) = implicitable n

357implicitable (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)

329implicitable (MN _ _) = True

360implicitable (MN _ _) = True

330implicitable _ = False

361implicitable _ = False

331

362

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

626 | otherwise = 1

657 | otherwise = 1

627 termsize n (V _) = 1

658 termsize n (V _) = 1

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

659 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

630 termsize rn v + termsize rn sc

661 termsize rn v + termsize rn sc

631 termsize n (Bind n' b sc)

662 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

633 termsize rn sc

664 termsize rn sc

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

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

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

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

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

889

920

890nextName (NS x s) = NS (nextName x) s

921nextName (NS x s) = NS (nextName x) s

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

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

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

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

893− nm = reverse nm'

924+ nm = T.reverse nm'

894− num = readN (reverse num') in

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

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

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

896 where

927 where

897− readN "" = 0

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

898− readN x = read x

929+ readN x = 0

899nextName (SN x) = SN (nextName' x)

930nextName (SN x) = SN (nextName' x)

900 where

931 where

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

932 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

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

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

1041 pureBinder t = pureTerm (binderTy t)

1072 pureBinder t = pureTerm (binderTy t)

1042

1073

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

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

1044 notClassName _ = True

1075 notClassName _ = True

1045

1076

1046pureTerm _ = True

1077pureTerm _ = True

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

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

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

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

90 -- 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)

92 (renameBinders (i+1) t)

93 renameBinders i sc = sc

94 chk env RType

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

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

277

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

279 | 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)))

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

282

283 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

31 return $ mkApp t' args'

32 toTT _ = do v <- get

33 put (v + 1)

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

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

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

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

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

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

167 otherPats o@(PPair fc l r)

168 = ops fc pairCon

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

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

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

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

171 [pexp l, pexp r]) o

172 otherPats o@(PDPair fc t _ v)

173− = ops fc (UN "Ex_intro")

173+ = ops fc (sUN "Ex_intro")

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

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

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

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

176 [pexp t,pexp v]) o

177 otherPats o@(PConstant c) = return o

178 otherPats arg = return Placeholder

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

191 getExpTm t = getTm t

192

193 -- 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"

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

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

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

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

197 | n == pairCon

198 | n == pairCon

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

258

259

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

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

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

261 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

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

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

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

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

264 let ctxt = tt_ctxt i

266 let ctxt = tt_ctxt i

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

405 findCalls (dePat rhs) (patvars lhs) pargs

407 findCalls (dePat rhs) (patvars lhs) pargs

406

408

407 findCalls ap@(App f a) pvs pargs

409 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"

409 = findCalls arg pvs pargs

412 = findCalls arg pvs pargs

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

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

411 = mkChange n args pargs ++

414 = mkChange n args pargs ++

src/Idris/DSL.hs+4−4

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

57 block b (DoBind fc n tm : rest)

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

59 block b (DoBindP fc p tm : rest)

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

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

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

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

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

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

64 = PLet n ty tm (block b rest)

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

67 block b (DoExp fc tm : rest)

68 = PApp fc b

69 [pexp tm,

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

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

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

73expandDo 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

131 db' (PAppBind fc t args)

132 = do args' <- dbs args

133 (bs, n) <- get

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

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

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

136 return (PRef fc nm)

137 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

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

39 -- 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

42 addCollapsibleArgs :: Int -> Type -> ForceMap -> ForceMap

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

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

73 guardedArgs t = bareArg t

75 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

77 bareArg _ = M.empty

78 bareArg _ = M.empty

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

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

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

227

228

228-- Run-time: do everything

229-- Run-time: do everything

229

230

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

232+

230instance Optimisable (TT Name) where

233instance Optimisable (TT Name) where

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

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

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

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

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

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

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

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

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

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

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

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

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

236 = applyOpts x

242 = applyOpts x

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

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

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

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

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

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

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

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

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

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

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

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

242 = do i <- getIState

250 = do i <- getIState

243 case lookupCtxt n (idris_optimisation i) of

251 case lookupCtxt n (idris_optimisation i) of

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

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

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

289 bind extra tm

297 bind extra tm

290 where

298 where

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

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

292

300

293 bind [] tm = tm

301 bind [] tm = tm

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

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

295

303

296 -- Nat special cases

304 -- Nat special cases

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

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

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

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

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

308+ = Constant (BI 0)

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

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

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

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

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

301

312

302 doOpts n args True _ = Erased

313 doOpts n args True _ = Erased

303 doOpts n args _ forceMap

314 doOpts n args _ forceMap

src/Idris/Delaborate.hs+9−9

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

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

44 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 ++ ""))

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

47 | n == unitCon = PTrue un

48 | n == falseTy = PFalse un

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

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

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

65 = 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

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

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

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

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

69 de env _ (Constant i) = PConstant i

70 de env _ Erased = Placeholder

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

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

83 | n == pairTy = PPair un (de env [] l) (de env [] r)

84 | n == eqCon = PRefl un (de env [] r)

85− | n == UN "lazy" = de env [] r

85+ | n == sUN "lazy" = de env [] r

86 deFn env (P _ n _) [ty, Bind x (Lam _) r]

87− | n == UN "Exists"

87+ | n == sUN "Exists"

88 = PDPair un (PRef un x) (de env [] ty)

89 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

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

91 | n == pairCon = PPair un (de env [] l) (de env [] r)

92 | n == eqTy = PEq un (de env [] l) (de env [] r)

93− | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder

93+ | n == sUN "Ex_intro" = PDPair un (de env [] l) Placeholder

94− (de env [] r)

94+ (de env [] r)

95 deFn env (P _ n _) args | not mvs

96 = case lookup n (idris_metavars ist) of

97 Just (Just _, mi, _) ->

@@ -220,8 +220,8 @@ showqual i n = showName (Just i) [] False False (dens n)

220 dens n = n

221

222showbasic n@(UN _) = show n

223−showbasic (MN _ s) = s

223+showbasic (MN _ s) = str s

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

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

225showbasic (SN s) = show s

226

227

src/Idris/Docs.hs+1−1

@@ -107,7 +107,7 @@ docFun n

107

108 return (Doc n docstr args (delab i ty) f)

109 where funName :: Name -> String

110− funName (UN n) = n

110+ funName (UN n) = str n

111 funName (NS n _) = funName n

112

113

src/Idris/ElabDecls.hs+83−75

@@ -34,6 +34,7 @@ import Data.Maybe

34import Debug.Trace

36import qualified Data.Map as Map

37+import qualified Data.Text as T

37import Data.Char(isLetter, toLower)

38import Data.Char(isLetter, toLower)

38import Data.List.Split (splitOn)

39import Data.List.Split (splitOn)

@@ -139,14 +140,20 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

139 | otherwise = mergeTy sc sc'

140 | otherwise = mergeTy sc sc'

140 mergeTy _ sc = sc

141 mergeTy _ sc = sc

141

142

143+ err = txt "Err"

144+ maybe = txt "Maybe"

145+ lst = txt "List"

146+ errrep = txt "ErrorReportPart"

147+

142− tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))

148+ tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))

143− (App (P _ (NS (UN "Maybe") ns2) _)

149+ (App (P _ (NS (UN m) ns2) _)

144− (App (P _ (NS (UN "List") ns3) _)

150+ (App (P _ (NS (UN l) ns3) _)

145− (P _ (NS (UN "ErrorReportPart") ns4) _))))

151+ (P _ (NS (UN r) ns4) _))))

152+ | e == err && m == maybe && l == lst && r == errrep

146− | ns1 == ["Errors","Reflection","Language"]

153+ , ns1 == map txt ["Errors","Reflection","Language"]

147− , ns2 == ["Maybe", "Prelude"]

154+ , ns2 == map txt ["Maybe", "Prelude"]

148− , ns3 == ["List", "Prelude"]

155+ , ns3 == map txt ["List", "Prelude"]

149− , ns4 == ["Errors","Reflection","Language"] = True

156+ , ns4 == map txt ["Errors","Reflection","Language"] = True

150 tyIsHandler _ = False

157 tyIsHandler _ = False

151

158

152

159

@@ -337,7 +344,7 @@ elabEliminator paramPos n ty cons info = do

337

344

338 applyNS :: Name -> [String] -> Name

345 applyNS :: Name -> [String] -> Name

339 applyNS n [] = n

346 applyNS n [] = n

340− applyNS n ns = NS n ns

347+ applyNS n ns = sNS n ns

341

348

342 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

349 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

343 splitPi = splitPi' []

350 splitPi = splitPi' []

@@ -376,11 +383,11 @@ elabEliminator paramPos n ty cons info = do

376

383

377 simpleName :: Name -> String

384 simpleName :: Name -> String

378 simpleName (NS n _) = simpleName n

385 simpleName (NS n _) = simpleName n

379− simpleName (MN i n) = n ++ show i

386+ simpleName (MN i n) = str n ++ show i

380 simpleName n = show n

387 simpleName n = show n

381

388

382 nameSpaces :: Name -> [String]

389 nameSpaces :: Name -> [String]

383− nameSpaces (NS _ ns) = ns

390+ nameSpaces (NS _ ns) = map str ns

384 nameSpaces _ = []

391 nameSpaces _ = []

385

392

386 freshName :: String -> EliminatorState Name

393 freshName :: String -> EliminatorState Name

@@ -389,16 +396,16 @@ elabEliminator paramPos n ty cons info = do

389 let i = fromMaybe 0 (Map.lookup key nameMap)

396 let i = fromMaybe 0 (Map.lookup key nameMap)

390 let name = key ++ show i

397 let name = key ++ show i

391 put $ Map.insert key (i+1) nameMap

398 put $ Map.insert key (i+1) nameMap

392− return (UN name)

399+ return (sUN name)

393

400

394 scrutineeName :: Name

401 scrutineeName :: Name

395− scrutineeName = UN "scrutinee"

402+ scrutineeName = sUN "scrutinee"

396

403

397 scrutineeArgName :: Name

404 scrutineeArgName :: Name

398− scrutineeArgName = UN "scrutineeArg"

405+ scrutineeArgName = sUN "scrutineeArg"

399

406

400 motiveName :: Name

407 motiveName :: Name

401− motiveName = UN "prop"

408+ motiveName = sUN "prop"

402

409

403 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

410 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

404 mkMotive n paramPos params indicies =

411 mkMotive n paramPos params indicies =

@@ -488,7 +495,7 @@ elabEliminator paramPos n ty cons info = do

488 let (_, consIdxs) = splitArgPms resTy

495 let (_, consIdxs) = splitArgPms resTy

489 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

496 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

490 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

497 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))

492 where (_, idxs) = splitArgPms ty

499 where (_, idxs) = splitArgPms ty

493

500

494 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

501 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

@@ -539,7 +546,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

539 (zip

546 (zip

540 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

547 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

541 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

548 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

542− addNameHint eqTy (UN "prf")

549+ addNameHint eqTy (sUN "prf")

543 elabDecl EAll toplevel elimDecl

550 elabDecl EAll toplevel elimDecl

544 mapM_ elabPrim primitives

551 mapM_ elabPrim primitives

545 -- Special case prim__believe_me because it doesn't work on just constants

552 -- Special case prim__believe_me because it doesn't work on just constants

@@ -562,11 +569,11 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

562

569

563 p_believeMe [_,_,x] = Just x

570 p_believeMe [_,_,x] = Just x

564 p_believeMe _ = Nothing

571 p_believeMe _ = Nothing

565− believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))

572+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))))

566− (Bind (UN "b") (Pi (TType (UVar (-2))))

573+ (Bind (sUN "b") (Pi (TType (UVar (-2))))

567− (Bind (UN "x") (Pi (V 1)) (V 1)))

574+ (Bind (sUN "x") (Pi (V 1)) (V 1)))

568 elabBelieveMe

575 elabBelieveMe

569− = do let prim__believe_me = (UN "prim__believe_me")

576+ = do let prim__believe_me = sUN "prim__believe_me"

570 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

577 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

571 setTotality prim__believe_me (Partial NotCovering)

578 setTotality prim__believe_me (Partial NotCovering)

572 i <- getIState

579 i <- getIState

@@ -580,19 +587,19 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

580 | otherwise = Just (VApp vnNothing VErased)

587 | otherwise = Just (VApp vnNothing VErased)

581 p_synEq args = Nothing

588 p_synEq args = Nothing

582

589

583− nMaybe = P (TCon 0 2) (NS (UN "Maybe") ["Maybe", "Prelude"]) Erased

590+ nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased

584− vnJust = VP (DCon 1 2) (NS (UN "Just") ["Maybe", "Prelude"]) VErased

591+ vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

585− vnNothing = VP (DCon 0 1) (NS (UN "Nothing") ["Maybe", "Prelude"]) VErased

592+ vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

586 vnRefl = VP (DCon 0 2) eqCon VErased

593 vnRefl = VP (DCon 0 2) eqCon VErased

587

594

588− synEqTy = Bind (UN "a") (Pi (TType (UVar (-3))))

595+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))

589− (Bind (UN "b") (Pi (TType (UVar (-3))))

596+ (Bind (sUN "b") (Pi (TType (UVar (-3))))

590− (Bind (UN "x") (Pi (V 1))

597+ (Bind (sUN "x") (Pi (V 1))

591− (Bind (UN "y") (Pi (V 1))

598+ (Bind (sUN "y") (Pi (V 1))

592 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

599 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

593 [V 3, V 2, V 1, V 0]]))))

600 [V 3, V 2, V 1, V 0]]))))

594 elabSynEq

601 elabSynEq

595− = do let synEq = UN "prim__syntactic_eq"

602+ = do let synEq = sUN "prim__syntactic_eq"

596

603

597 updateContext (addOperator synEq synEqTy 4 p_synEq)

604 updateContext (addOperator synEq synEqTy 4 p_synEq)

598 setTotality synEq (Total [])

605 setTotality synEq (Total [])

@@ -630,7 +637,7 @@ elabProvider info syn fc n ty tm

630 -- Execute the type provider and normalise the result

637 -- Execute the type provider and normalise the result

631 -- use 'run__provider' to convert to a primitive IO action

638 -- use 'run__provider' to convert to a primitive IO action

632

639

633− rhs <- execute (mkApp (P Ref (UN "run__provider") Erased)

640+ rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)

634 [Erased, e])

641 [Erased, e])

635 let rhs' = normalise ctxt [] rhs

642 let rhs' = normalise ctxt [] rhs

636 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

643 logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

@@ -648,9 +655,10 @@ elabProvider info syn fc n ty tm

648

655

649 isProviderOf :: TT Name -> TT Name -> Bool

656 isProviderOf :: TT Name -> TT Name -> Bool

650 isProviderOf tp prov

657 isProviderOf tp prov

651− | (P _ (UN "IO") _, [prov']) <- unApply prov

658+ | (P _ (UN io) _, [prov']) <- unApply prov

659+ , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'

660+ , tp == tp', io == txt "IO"

652− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'

661+ , prov == txt "Provider" && provs == txt "Providers" = True

653− , tp == tp' = True

654 isProviderOf _ _ = False

662 isProviderOf _ _ = False

655

663

656-- | Elaborate a type provider

664-- | Elaborate a type provider

@@ -660,8 +668,8 @@ elabTransform info fc safe lhs_in rhs_in

660 i <- getIState

668 i <- getIState

661 let lhs = addImplPat i lhs_in

669 let lhs = addImplPat i lhs_in

662 ((lhs', dlhs, []), _) <-

670 ((lhs', dlhs, []), _) <-

663− tclift $ elaborate ctxt (MN 0 "transLHS") infP []

671+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

664− (erun fc (buildTC i info True [] (UN "transform")

672+ (erun fc (buildTC i info True [] (sUN "transform")

665 (infTerm lhs)))

673 (infTerm lhs)))

666 let lhs_tm = orderPats (getInferTerm lhs')

674 let lhs_tm = orderPats (getInferTerm lhs')

667 let lhs_ty = getInferType lhs'

675 let lhs_ty = getInferType lhs'

@@ -671,10 +679,10 @@ elabTransform info fc safe lhs_in rhs_in

671 logLvl 3 ("Transform LHS " ++ show clhs_tm)

679 logLvl 3 ("Transform LHS " ++ show clhs_tm)

672 let rhs = addImplBound i (map fst newargs) rhs_in

680 let rhs = addImplBound i (map fst newargs) rhs_in

673 ((rhs', defer), _) <-

681 ((rhs', defer), _) <-

674− tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []

682+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

675 (do pbinds lhs_tm

683 (do pbinds lhs_tm

676 setNextName

684 setNextName

677− erun fc (build i info False [] (UN "transform") rhs)

685+ erun fc (build i info False [] (sUN "transform") rhs)

678 erun fc $ psolve lhs_tm

686 erun fc $ psolve lhs_tm

679 tt <- get_term

687 tt <- get_term

680 return (runState (collectDeferred Nothing tt) []))

688 return (runState (collectDeferred Nothing tt) []))

@@ -744,18 +752,18 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

744 getRecTy (PPi _ n ty s) = getRecTy s

752 getRecTy (PPi _ n ty s) = getRecTy s

745 getRecTy t = t

753 getRecTy t = t

746

754

747− rec = MN 0 "rec"

755+ rec = sMN 0 "rec"

748

756

749− mkp (UN n) = MN 0 ("p_" ++ n)

757+ mkp (UN n) = sMN 0 ("p_" ++ str n)

750− mkp (MN i n) = MN i ("p_" ++ n)

758+ mkp (MN i n) = sMN i ("p_" ++ str n)

751 mkp (NS n s) = NS (mkp n) s

759 mkp (NS n s) = NS (mkp n) s

752

760

753− mkImp (UN n) = UN ("implicit_" ++ n)

761+ mkImp (UN n) = sUN ("implicit_" ++ str n)

754− mkImp (MN i n) = MN i ("implicit_" ++ n)

762+ mkImp (MN i n) = sMN i ("implicit_" ++ str n)

755 mkImp (NS n s) = NS (mkImp n) s

763 mkImp (NS n s) = NS (mkImp n) s

756

764

757− mkType (UN n) = UN ("set_" ++ n)

765+ mkType (UN n) = sUN ("set_" ++ str n)

758− mkType (MN i n) = MN i ("set_" ++ n)

766+ mkType (MN i n) = sMN i ("set_" ++ str n)

759 mkType (NS n s) = NS (mkType n) s

767 mkType (NS n s) = NS (mkType n) s

760

768

761 mkProj recty substs cimp ((pn_in, pty), pos)

769 mkProj recty substs cimp ((pn_in, pty), pos)

@@ -778,11 +786,11 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

778

786

779 mkUpdate recty k num ((pn, pty), pos)

787 mkUpdate recty k num ((pn, pty), pos)

780 = do let setname = expandNS syn $ mkType pn

788 = do let setname = expandNS syn $ mkType pn

781− let valname = MN 0 "updateval"

789+ let valname = sMN 0 "updateval"

782 let pt = k (PPi expl pn pty

790 let pt = k (PPi expl pn pty

783 (PPi expl rec recty recty))

791 (PPi expl rec recty recty))

784 let pfnTy = PTy "" defaultSyntax fc [] setname pt

792 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]

786 let lhsArgs = pls

794 let lhsArgs = pls

787 let rhsArgs = take pos pls ++ (PRef fc valname) :

795 let rhsArgs = take pos pls ++ (PRef fc valname) :

788 drop (pos + 1) pls

796 drop (pos + 1) pls

@@ -1145,7 +1153,7 @@ elabPE info fc caller r =

1145 _ -> error "Can't happen (getSpecTy)"

1153 _ -> error "Can't happen (getSpecTy)"

1146

1154

1147 getSpecClause ist (n, args)

1155 getSpecClause ist (n, args)

1148− = let newnm = UN ("__"++show (nsroot n) ++ "_" ++

1156+ = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++

1149 showSep "_" (map showArg args)) in

1157 showSep "_" (map showArg args)) in

1150 -- UN (show n ++ show (map snd args)) in

1158 -- UN (show n ++ show (map snd args)) in

1151 (n, newnm, mkPE_TermDecl ist newnm n args)

1159 (n, newnm, mkPE_TermDecl ist newnm n args)

@@ -1170,8 +1178,8 @@ elabValBind info aspat tm_in

1170 ((tm', defer, is), _) <-

1178 ((tm', defer, is), _) <-

1171-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

1179-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

1172-- (build i info aspat (MN 0 "val") tm))

1180-- (build i info aspat (MN 0 "val") tm))

1173− tclift (elaborate ctxt (MN 0 "val") infP []

1181+ tclift (elaborate ctxt (sMN 0 "val") infP []

1174− (build i info aspat [Reflection] (MN 0 "val") (infTerm tm)))

1182+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

1175 let vtm = orderPats (getInferTerm tm')

1183 let vtm = orderPats (getInferTerm tm')

1176

1184

1177 def' <- checkDef (fileFC "(input)") defer

1185 def' <- checkDef (fileFC "(input)") defer

@@ -1201,7 +1209,7 @@ checkPossible info fc tcgen fname lhs_in

1201 i <- getIState

1209 i <- getIState

1202 let lhs = addImpl i lhs_in

1210 let lhs = addImpl i lhs_in

1203 -- if the LHS type checks, it is possible

1211 -- if the LHS type checks, it is possible

1204− case elaborate ctxt (MN 0 "patLHS") infP []

1212+ case elaborate ctxt (sMN 0 "patLHS") infP []

1205 (erun fc (buildTC i info True [] fname (infTerm lhs))) of

1213 (erun fc (buildTC i info True [] fname (infTerm lhs))) of

1206 OK ((lhs', _, _), _) ->

1214 OK ((lhs', _, _), _) ->

1207 do let lhs_tm = orderPats (getInferTerm lhs')

1215 do let lhs_tm = orderPats (getInferTerm lhs')

@@ -1256,7 +1264,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1256 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1264 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1257

1265

1258 ((lhs', dlhs, []), _) <-

1266 ((lhs', dlhs, []), _) <-

1259− tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1267+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1260 (errAt "left hand side of " fname

1268 (errAt "left hand side of " fname

1261 (erun fc (buildTC i info True opts fname (infTerm lhs))))

1269 (erun fc (buildTC i info True opts fname (infTerm lhs))))

1262 let lhs_tm = orderPats (getInferTerm lhs')

1270 let lhs_tm = orderPats (getInferTerm lhs')

@@ -1300,7 +1308,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1300 ctxt <- getContext -- new context with where block added

1308 ctxt <- getContext -- new context with where block added

1301 logLvl 5 "STARTING CHECK"

1309 logLvl 5 "STARTING CHECK"

1302 ((rhs', defer, is), _) <-

1310 ((rhs', defer, is), _) <-

1303− tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

1311+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1304 (do pbinds lhs_tm

1312 (do pbinds lhs_tm

1305 setNextName

1313 setNextName

1306 (_, _, is) <- errAt "right hand side of " fname

1314 (_, _, is) <- errAt "right hand side of " fname

@@ -1436,7 +1444,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1436 let lhs = addImplPat i (stripLinear i lhs_in)

1444 let lhs = addImplPat i (stripLinear i lhs_in)

1437 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1445 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1438 ((lhs', dlhs, []), _) <-

1446 ((lhs', dlhs, []), _) <-

1439− tclift $ elaborate ctxt (MN 0 "patLHS") infP []

1447+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1440 (errAt "left hand side of with in " fname

1448 (errAt "left hand side of with in " fname

1441 (erun fc (buildTC i info True opts fname (infTerm lhs))) )

1449 (erun fc (buildTC i info True opts fname (infTerm lhs))) )

1442 let lhs_tm = orderPats (getInferTerm lhs')

1450 let lhs_tm = orderPats (getInferTerm lhs')

@@ -1450,7 +1458,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1450 logLvl 5 ("Checking " ++ showImp Nothing True False wval)

1458 logLvl 5 ("Checking " ++ showImp Nothing True False wval)

1451 -- Elaborate wval in this context

1459 -- Elaborate wval in this context

1452 ((wval', defer, is), _) <-

1460 ((wval', defer, is), _) <-

1453− tclift $ elaborate ctxt (MN 0 "withRHS")

1461+ tclift $ elaborate ctxt (sMN 0 "withRHS")

1454 (bindTyArgs PVTy bargs infP) []

1462 (bindTyArgs PVTy bargs infP) []

1455 (do pbinds lhs_tm

1463 (do pbinds lhs_tm

1456 setNextName

1464 setNextName

@@ -1483,11 +1491,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1483 let wargtype = getRetTy cwvaltyN

1491 let wargtype = getRetTy cwvaltyN

1484 logLvl 5 ("Abstract over " ++ show wargval)

1492 logLvl 5 ("Abstract over " ++ show wargval)

1485 let wtype = bindTyArgs Pi (bargs_pre ++

1493 let wtype = bindTyArgs Pi (bargs_pre ++

1486− (MN 0 "warg", wargtype) :

1494+ (sMN 0 "warg", wargtype) :

1487− map (abstract (MN 0 "warg") wargval wargtype) bargs_post)

1495+ map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

1488− (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)

1496+ (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

1489 logLvl 3 ("New function type " ++ show wtype)

1497 logLvl 3 ("New function type " ++ show wtype)

1490− let wname = MN windex (show fname)

1498+ let wname = sMN windex (show fname)

1491

1499

1492 let imps = getImps wtype -- add to implicits context

1500 let imps = getImps wtype -- add to implicits context

1493 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

1501 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)

1515 ctxt <- getContext -- New context with block added

1523 ctxt <- getContext -- New context with block added

1516 i <- getIState

1524 i <- getIState

1517 ((rhs', defer, is), _) <-

1525 ((rhs', defer, is), _) <-

1518− tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

1526+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

1519 (do pbinds lhs_tm

1527 (do pbinds lhs_tm

1520 setNextName

1528 setNextName

1521 (_, d, is) <- erun fc (build i info False opts fname rhs)

1529 (_, d, is) <- erun fc (build i info False opts fname rhs)

@@ -1596,7 +1604,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

1596 FC -> [PTerm] ->

1604 FC -> [PTerm] ->

1597 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1605 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1598elabClass info syn doc fc constraints tn ps ds

1606elabClass 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)

1600 let tty = pibind ps PType

1608 let tty = pibind ps PType

1601 let constraint = PApp fc (PRef fc tn)

1609 let constraint = PApp fc (PRef fc tn)

1602 (map (pexp . PRef fc) (map fst ps))

1610 (map (pexp . PRef fc) (map fst ps))

@@ -1657,7 +1665,7 @@ elabClass info syn doc fc constraints tn ps ds

1657

1665

1658 impbind [] x = x

1666 impbind [] x = x

1659 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

1667 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)

1661 conbind [] x = x

1669 conbind [] x = x

1662

1670

1663 getMName (PTy _ _ _ _ n _) = nsroot n

1671 getMName (PTy _ _ _ _ n _) = nsroot n

@@ -1681,7 +1689,7 @@ elabClass info syn doc fc constraints tn ps ds

1681 _ -> ifail $ show n ++ " is not a method"

1689 _ -> ifail $ show n ++ " is not a method"

1682 defdecl _ _ _ = ifail "Can't happen (defdecl)"

1690 defdecl _ _ _ = ifail "Can't happen (defdecl)"

1683

1691

1684− defaultdec (UN n) = UN ("default#" ++ n)

1692+ defaultdec (UN n) = sUN ("default#" ++ str n)

1685 defaultdec (NS n ns) = NS (defaultdec n) ns

1693 defaultdec (NS n ns) = NS (defaultdec n) ns

1686

1694

1687 tydecl (PTy _ _ _ _ _ _) = True

1695 tydecl (PTy _ _ _ _ _ _) = True

@@ -1693,13 +1701,13 @@ elabClass info syn doc fc constraints tn ps ds

1693

1701

1694 -- Generate a function for chasing a dictionary constraint

1702 -- Generate a function for chasing a dictionary constraint

1695 cfun cn c syn all con

1703 cfun cn c syn all con

1696− = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)

1704+ = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

1697 -- SN (ParentN cn (show con))

1705 -- 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..]

1699 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1707 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1700 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1708 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1701 let rhs = PResolveTC (fileFC "HACK")

1709 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

1703 iLOG (showImp Nothing True False ty)

1711 iLOG (showImp Nothing True False ty)

1704 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1712 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1705 i <- getIState

1713 i <- getIState

@@ -1719,10 +1727,10 @@ elabClass info syn doc fc constraints tn ps ds

1719 -- dictionary (this is inlinable, always)

1727 -- dictionary (this is inlinable, always)

1720 tfun cn c syn all (m, (doc, o, ty))

1728 tfun cn c syn all (m, (doc, o, ty))

1721 = do let ty' = insertConstraint c ty

1729 = 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..]

1723 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1731 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1724 let margs = getMArgs ty

1732 let margs = getMArgs ty

1725− let anames = map (\x -> MN x "arg") [0..]

1733+ let anames = map (\x -> sMN x "arg") [0..]

1726 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1734 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1727 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1735 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1728 iLOG (showImp Nothing True False ty)

1736 iLOG (showImp Nothing True False ty)

@@ -1751,7 +1759,7 @@ elabClass info syn doc fc constraints tn ps ds

1751

1759

1752 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1760 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1753 = PPi p n ty (insertConstraint c sc)

1761 = 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

1755

1763

1756 -- make arguments explicit and don't bind class parameters

1764 -- make arguments explicit and don't bind class parameters

1757 toExp ns e (PPi (Imp l s _ p) n ty sc)

1765 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

1834

1842

1835 mkiname n' ps' expn' =

1843 mkiname n' ps' expn' =

1836 case expn' of

1844 case expn' of

1837− Nothing -> SN (InstanceN n' (map show ps'))

1845+ Nothing -> SN (sInstanceN n' (map show ps'))

1838 Just nm -> nm

1846 Just nm -> nm

1839

1847

1840 substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

1848 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

1882 mkMethApp (n, _, _, ty)

1890 mkMethApp (n, _, _, ty)

1883 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

1891 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

1884 lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'

1892 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')

1886 lamBind i (PPi _ n ty sc) sc'

1894 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')

1888 lamBind i _ sc = sc

1896 lamBind i _ sc = sc

1889 methArgs i (PPi (Imp _ _ _ _) n ty sc)

1897 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

1891 methArgs i (PPi (Exp _ _ _ _) n ty sc)

1899 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

1893 methArgs i (PPi (Constraint _ _ _) n ty sc)

1901 methArgs i (PPi (Constraint _ _ _) n ty sc)

1894 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

1902 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

1895 methArgs i _ = []

1903 methArgs i _ = []

@@ -1912,14 +1920,14 @@ elabInstance info syn fc cs n ps t expn ds

1912

1920

1913 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

1921 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

1914

1922

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)

1916 conbind [] x = x

1924 conbind [] x = x

1917

1925

1918 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

1926 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

1919 coninsert cs sc = conbind cs sc

1927 coninsert cs sc = conbind cs sc

1920

1928

1921 insertDefaults :: IState -> Name ->

1929 insertDefaults :: IState -> Name ->

1922− [(Name, (Name, PDecl))] -> [String] ->

1930+ [(Name, (Name, PDecl))] -> [T.Text] ->

1923 [PDecl] -> [PDecl]

1931 [PDecl] -> [PDecl]

1924 insertDefaults i iname [] ns ds = ds

1932 insertDefaults i iname [] ns ds = ds

1925 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds

1933 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

173 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

174 = do g <- goal; resolveTC 5 g fn ist

175 elab' ina (PResolveTC fc)

176− | True = do c <- getNameFrom (MN 0 "class")

176+ | True = do c <- getNameFrom (sMN 0 "class")

177 instanceArg c

178 | otherwise = do g <- goal

179 try (resolveTC 2 g fn ist)

180− (do c <- getNameFrom (MN 0 "class")

180+ (do c <- getNameFrom (sMN 0 "class")

181 instanceArg c)

182 elab' ina (PRefl fc t)

183− = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "A") Placeholder True,

183+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

184− pimp (MN 0 "x") t False])

184+ pimp (sMN 0 "x") t False])

185 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

186− [pimp (MN 0 "A") Placeholder True,

186+ [pimp (sMN 0 "A") Placeholder True,

187− pimp (MN 0 "B") Placeholder False,

187+ pimp (sMN 0 "B") Placeholder False,

188 pexp l, pexp r])

189 elab' ina@(_, a, inty) (PPair fc l r)

190 = do hnf_compute

@@ -193,8 +193,8 @@ elab ist info pattern opts fn tm

193 TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)

194 [pexp l,pexp r])

195 _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)

196− [pimp (MN 0 "A") Placeholder True,

196+ [pimp (sMN 0 "A") Placeholder True,

197− pimp (MN 0 "B") Placeholder True,

197+ pimp (sMN 0 "B") Placeholder True,

198 pexp l, pexp r])

199 elab' ina (PDPair fc l@(PRef _ n) t r)

200 = case t of

@@ -209,12 +209,12 @@ elab ist info pattern opts fn tm

209 [pexp t,

210 pexp (PLam n Placeholder r)])

211 asValue = elab' ina (PApp fc (PRef fc existsCon)

212− [pimp (MN 0 "a") t False,

212+ [pimp (sMN 0 "a") t False,

213− pimp (MN 0 "P") Placeholder True,

213+ pimp (sMN 0 "P") Placeholder True,

214 pexp l, pexp r])

215 elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)

216− [pimp (MN 0 "a") t False,

216+ [pimp (sMN 0 "a") t False,

217− pimp (MN 0 "P") Placeholder True,

217+ pimp (sMN 0 "P") Placeholder True,

218 pexp l, pexp r])

219 elab' ina (PAlternative True as)

220 = do hnf_compute

@@ -274,7 +274,7 @@ elab ist info pattern opts fn tm

274 elab' ina@(_, a, inty) (PLam n ty sc)

275 = do hsin <- get_holes

276 ptmin <- get_term

277− tyn <- getNameFrom (MN 0 "lamty")

277+ tyn <- getNameFrom (sMN 0 "lamty")

278 checkPiGoal n

279 claim tyn RType

280 explicit tyn

@@ -290,9 +290,9 @@ elab ist info pattern opts fn tm

290 elabE (True, a, inty) sc

291 solve

292 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

294 elab' ina@(_, a, _) (PPi _ n ty sc)

295− = do attack; tyn <- getNameFrom (MN 0 "ty")

295+ = do attack; tyn <- getNameFrom (sMN 0 "ty")

296 claim tyn RType

297 n' <- case n of

298 MN _ _ -> unique_hole n

@@ -304,9 +304,9 @@ elab ist info pattern opts fn tm

304 solve

305 elab' ina@(_, a, inty) (PLet n ty val sc)

306 = do attack;

307− tyn <- getNameFrom (MN 0 "letty")

307+ tyn <- getNameFrom (sMN 0 "letty")

308 claim tyn RType

309− valn <- getNameFrom (MN 0 "letval")

309+ valn <- getNameFrom (sMN 0 "letval")

310 claim valn (Var tyn)

311 explicit valn

312 letbind n (Var tyn) (Var valn)

@@ -327,9 +327,9 @@ elab ist info pattern opts fn tm

327 elab' ina@(_, a, inty) (PGoal fc r n sc) = do

328 rty <- goal

329 attack

330− tyn <- getNameFrom (MN 0 "letty")

330+ tyn <- getNameFrom (sMN 0 "letty")

331 claim tyn RType

332− valn <- getNameFrom (MN 0 "letval")

332+ valn <- getNameFrom (sMN 0 "letval")

333 claim valn (Var tyn)

334 letbind n (Var tyn) (Var valn)

335 focus valn

@@ -348,7 +348,7 @@ elab ist info pattern opts fn tm

348 -- new function name

349 env <- get_env

350 argTys <- claimArgTys env args

351− fn <- getNameFrom (MN 0 "inf_fn")

351+ fn <- getNameFrom (sMN 0 "inf_fn")

352 let fty = fnTy argTys rty

353-- trace (show (ptm, map fst argTys)) $ focus fn

354 -- build and defer the function application

@@ -362,8 +362,8 @@ elab ist info pattern opts fn tm

362 ans <- claimArgTys env xs

363 return ((n, (False, forget nty)) : ans)

364 claimArgTys env (_ : xs)

365− = do an <- getNameFrom (MN 0 "inf_argTy")

365+ = do an <- getNameFrom (sMN 0 "inf_argTy")

366− aval <- getNameFrom (MN 0 "inf_arg")

366+ aval <- getNameFrom (sMN 0 "inf_arg")

367 claim an RType

368 claim aval (Var an)

369 ans <- claimArgTys env xs

@@ -383,7 +383,7 @@ elab ist info pattern opts fn tm

383 mkN n@(NS _ _) = n

384 mkN n@(SN _) = n

385 mkN n = case namespace info of

386− Just xs@(_:_) -> NS n xs

386+ Just xs@(_:_) -> sNS n xs

387 _ -> n

388

389 elab' ina (PMatchApp fc fn)

@@ -467,7 +467,7 @@ elab ist info pattern opts fn tm

467 do attack; defer n'; solve

468 where mkN n@(NS _ _) = n

469 mkN n = case namespace info of

470− Just xs@(_:_) -> NS n xs

470+ Just xs@(_:_) -> sNS n xs

471 _ -> n

472 elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts

473 elab' ina (PTactics ts)

@@ -476,11 +476,11 @@ elab ist info pattern opts fn tm

476 elab' ina (PElabError e) = fail (pshow ist e)

477 elab' ina (PRewrite fc r sc newg)

478 = do attack

479− tyn <- getNameFrom (MN 0 "rty")

479+ tyn <- getNameFrom (sMN 0 "rty")

480 claim tyn RType

481− valn <- getNameFrom (MN 0 "rval")

481+ valn <- getNameFrom (sMN 0 "rval")

482 claim valn (Var tyn)

483− letn <- getNameFrom (MN 0 "rewrite_rule")

483+ letn <- getNameFrom (sMN 0 "rewrite_rule")

484 letbind letn (Var tyn) (Var valn)

485 focus valn

486 elab' ina r

@@ -495,11 +495,11 @@ elab ist info pattern opts fn tm

495 solve

496 where doEquiv t sc =

497 do attack

498− tyn <- getNameFrom (MN 0 "ety")

498+ tyn <- getNameFrom (sMN 0 "ety")

499 claim tyn RType

500− valn <- getNameFrom (MN 0 "eqval")

500+ valn <- getNameFrom (sMN 0 "eqval")

501 claim valn (Var tyn)

502− letn <- getNameFrom (MN 0 "equiv_val")

502+ letn <- getNameFrom (sMN 0 "equiv_val")

503 letbind letn (Var tyn) (Var valn)

504 focus tyn

505 elab' ina t

@@ -509,10 +509,10 @@ elab ist info pattern opts fn tm

509 solve

510 elab' ina@(_, a, inty) c@(PCase fc scr opts)

511 = do attack

512− tyn <- getNameFrom (MN 0 "scty")

512+ tyn <- getNameFrom (sMN 0 "scty")

513 claim tyn RType

514− valn <- getNameFrom (MN 0 "scval")

514+ valn <- getNameFrom (sMN 0 "scval")

515− scvn <- getNameFrom (MN 0 "scvar")

515+ scvn <- getNameFrom (sMN 0 "scvar")

516 claim valn (Var tyn)

517 letbind scvn (Var tyn) (Var valn)

518 focus valn

@@ -538,7 +538,7 @@ elab ist info pattern opts fn tm

538-- mkCaseName (MN i x) = MN i (x ++ "_case")

539 mkN n@(NS _ _) = n

540 mkN n = case namespace info of

541− Just xs@(_:_) -> NS n xs

541+ Just xs@(_:_) -> sNS n xs

542 _ -> n

543 elab' ina (PUnifyLog t) = do unifyLog True

544 elab' ina t

@@ -618,8 +618,8 @@ elab ist info pattern opts fn tm

618 = elabArgs ina failed fc r ns args

619 elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

620 | lazy && not pattern

621− = do elabArg n (PApp bi (PRef bi (UN "lazy"))

621+ = do elabArg n (PApp bi (PRef bi (sUN "lazy"))

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

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

623 pexp t]);

624 | otherwise = elabArg n t

625 where elabArg n t

@@ -699,9 +699,9 @@ findInstances ist t

699 | otherwise = []

700

701trivial' ist

702− = trivial (elab ist toplevel False [] (MN 0 "tac")) ist

702+ = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

703proofSearch' 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

705

706

707resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

@@ -737,12 +737,15 @@ resolveTC depth topg fn ist

737

738 -- HACK! Rather than giving a special name, better to have some kind

739 -- of flag in ClassInfo structure

740+ chaser (UN nm)

740− chaser (UN ('@':'@':_)) = True -- old way

741+ | ('@':'@':_) <- str nm = True -- old way

741 chaser (SN (ParentN _ _)) = True

742 chaser (SN (ParentN _ _)) = True

742 chaser (NS n _) = chaser n

743 chaser (NS n _) = chaser n

743 chaser _ = False

744 chaser _ = False

744

745

746+ numclass = sNS (sUN "Num") ["Classes","Prelude"]

747+

745− needsDefault t num@(P _ (NS (UN "Num") ["Classes","Prelude"]) _) [P Bound a _]

748+ needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass

746 = do focus a

749 = do focus a

747 fill (RConstant (AType (ATInt ITBig))) -- default Integer

750 fill (RConstant (AType (ATInt ITBig))) -- default Integer

748 solve

751 solve

@@ -830,7 +833,7 @@ runTac autoSolve ist tac

830 where

833 where

831 bname (Bind n _ _) = Just n

834 bname (Bind n _ _) = Just n

832 bname _ = Nothing

835 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

834 when autoSolve solveAll

837 when autoSolve solveAll

835 runT (MatchRefine fn)

838 runT (MatchRefine fn)

836 = do fnimps <-

839 = do fnimps <-

@@ -870,27 +873,27 @@ runTac autoSolve ist tac

870 when autoSolve solveAll

873 when autoSolve solveAll

871 runT (Equiv tm) -- let bind tm, then

874 runT (Equiv tm) -- let bind tm, then

872 = do attack

875 = do attack

873− tyn <- getNameFrom (MN 0 "ety")

876+ tyn <- getNameFrom (sMN 0 "ety")

874 claim tyn RType

877 claim tyn RType

875− valn <- getNameFrom (MN 0 "eqval")

878+ valn <- getNameFrom (sMN 0 "eqval")

876 claim valn (Var tyn)

879 claim valn (Var tyn)

877− letn <- getNameFrom (MN 0 "equiv_val")

880+ letn <- getNameFrom (sMN 0 "equiv_val")

878 letbind letn (Var tyn) (Var valn)

881 letbind letn (Var tyn) (Var valn)

879 focus tyn

882 focus tyn

880− elab ist toplevel False [] (MN 0 "tac") tm

883+ elab ist toplevel False [] (sMN 0 "tac") tm

881 focus valn

884 focus valn

882 when autoSolve solveAll

885 when autoSolve solveAll

883 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

886 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

884 = do attack; -- (h:_) <- get_holes

887 = do attack; -- (h:_) <- get_holes

885− tyn <- getNameFrom (MN 0 "rty")

888+ tyn <- getNameFrom (sMN 0 "rty")

886 -- start_unify h

889 -- start_unify h

887 claim tyn RType

890 claim tyn RType

888− valn <- getNameFrom (MN 0 "rval")

891+ valn <- getNameFrom (sMN 0 "rval")

889 claim valn (Var tyn)

892 claim valn (Var tyn)

890− letn <- getNameFrom (MN 0 "rewrite_rule")

893+ letn <- getNameFrom (sMN 0 "rewrite_rule")

891 letbind letn (Var tyn) (Var valn)

894 letbind letn (Var tyn) (Var valn)

892 focus valn

895 focus valn

893− elab ist toplevel False [] (MN 0 "tac") tm

896+ elab ist toplevel False [] (sMN 0 "tac") tm

894 rewrite (Var letn)

897 rewrite (Var letn)

895 when autoSolve solveAll

898 when autoSolve solveAll

896 runT (Induction nm)

899 runT (Induction nm)

@@ -898,27 +901,27 @@ runTac autoSolve ist tac

898 when autoSolve solveAll

901 when autoSolve solveAll

899 runT (LetTac n tm)

902 runT (LetTac n tm)

900 = do attack

903 = do attack

901− tyn <- getNameFrom (MN 0 "letty")

904+ tyn <- getNameFrom (sMN 0 "letty")

902 claim tyn RType

905 claim tyn RType

903− valn <- getNameFrom (MN 0 "letval")

906+ valn <- getNameFrom (sMN 0 "letval")

904 claim valn (Var tyn)

907 claim valn (Var tyn)

905 letn <- unique_hole n

908 letn <- unique_hole n

906 letbind letn (Var tyn) (Var valn)

909 letbind letn (Var tyn) (Var valn)

907 focus valn

910 focus valn

908− elab ist toplevel False [] (MN 0 "tac") tm

911+ elab ist toplevel False [] (sMN 0 "tac") tm

909 when autoSolve solveAll

912 when autoSolve solveAll

910 runT (LetTacTy n ty tm)

913 runT (LetTacTy n ty tm)

911 = do attack

914 = do attack

912− tyn <- getNameFrom (MN 0 "letty")

915+ tyn <- getNameFrom (sMN 0 "letty")

913 claim tyn RType

916 claim tyn RType

914− valn <- getNameFrom (MN 0 "letval")

917+ valn <- getNameFrom (sMN 0 "letval")

915 claim valn (Var tyn)

918 claim valn (Var tyn)

916 letn <- unique_hole n

919 letn <- unique_hole n

917 letbind letn (Var tyn) (Var valn)

920 letbind letn (Var tyn) (Var valn)

918 focus tyn

921 focus tyn

919− elab ist toplevel False [] (MN 0 "tac") ty

922+ elab ist toplevel False [] (sMN 0 "tac") ty

920 focus valn

923 focus valn

921− elab ist toplevel False [] (MN 0 "tac") tm

924+ elab ist toplevel False [] (sMN 0 "tac") tm

922 when autoSolve solveAll

925 when autoSolve solveAll

923 runT Compute = compute

926 runT Compute = compute

924 runT Trivial = do trivial' ist; when autoSolve solveAll

927 runT Trivial = do trivial' ist; when autoSolve solveAll

@@ -931,16 +934,16 @@ runTac autoSolve ist tac

931 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

934 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

932 tgoal <- goal -- store the goal

935 tgoal <- goal -- store the goal

933 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

936 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

934− script <- getNameFrom (MN 0 "script")

937+ script <- getNameFrom (sMN 0 "script")

935 claim script scriptTy

938 claim script scriptTy

936− scriptvar <- getNameFrom (MN 0 "scriptvar" )

939+ scriptvar <- getNameFrom (sMN 0 "scriptvar" )

937 letbind scriptvar scriptTy (Var script)

940 letbind scriptvar scriptTy (Var script)

938 focus script

941 focus script

939− elab ist toplevel False [] (MN 0 "tac") tm

942+ elab ist toplevel False [] (sMN 0 "tac") tm

940 (script', _) <- get_type_val (Var scriptvar)

943 (script', _) <- get_type_val (Var scriptvar)

941 -- now that we have the script apply

944 -- now that we have the script apply

942 -- it to the reflected goal and context

945 -- it to the reflected goal and context

943− restac <- getNameFrom (MN 0 "restac")

946+ restac <- getNameFrom (sMN 0 "restac")

944 claim restac tacticTy

947 claim restac tacticTy

945 focus restac

948 focus restac

946 fill (raw_apply (forget script')

949 fill (raw_apply (forget script')

@@ -954,27 +957,27 @@ runTac autoSolve ist tac

954 let tactic = normalise ctxt env restac'

957 let tactic = normalise ctxt env restac'

955 runReflected tactic

958 runReflected tactic

956 where tacticTy = Var (reflm "Tactic")

959 where tacticTy = Var (reflm "Tactic")

957− listTy = Var (NS (UN "List") ["List", "Prelude"])

960+ listTy = Var (sNS (sUN "List") ["List", "Prelude"])

958− scriptTy = (RBind (UN "__pi_arg")

961+ scriptTy = (RBind (sUN "__pi_arg")

959 (Pi (RApp listTy envTupleType))

962 (Pi (RApp listTy envTupleType))

960− (RBind (UN "__pi_arg1")

963+ (RBind (sUN "__pi_arg1")

961 (Pi (Var $ reflm "TT")) tacticTy))

964 (Pi (Var $ reflm "TT")) tacticTy))

962 runT (ByReflection tm) -- run the reflection function 'tm' on the

965 runT (ByReflection tm) -- run the reflection function 'tm' on the

963 -- goal, then apply the resulting reflected Tactic

966 -- goal, then apply the resulting reflected Tactic

964 = do tgoal <- goal

967 = do tgoal <- goal

965 attack

968 attack

966− script <- getNameFrom (MN 0 "script")

969+ script <- getNameFrom (sMN 0 "script")

967 claim script scriptTy

970 claim script scriptTy

968− scriptvar <- getNameFrom (MN 0 "scriptvar" )

971+ scriptvar <- getNameFrom (sMN 0 "scriptvar" )

969 letbind scriptvar scriptTy (Var script)

972 letbind scriptvar scriptTy (Var script)

970 focus script

973 focus script

971 ptm <- get_term

974 ptm <- get_term

972− elab ist toplevel False [] (MN 0 "tac")

975+ elab ist toplevel False [] (sMN 0 "tac")

973 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

976 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

974 (script', _) <- get_type_val (Var scriptvar)

977 (script', _) <- get_type_val (Var scriptvar)

975 -- now that we have the script apply

978 -- now that we have the script apply

976 -- it to the reflected goal

979 -- it to the reflected goal

977− restac <- getNameFrom (MN 0 "restac")

980+ restac <- getNameFrom (sMN 0 "restac")

978 claim restac tacticTy

981 claim restac tacticTy

979 focus restac

982 focus restac

980 fill (forget script')

983 fill (forget script')

@@ -990,28 +993,28 @@ runTac autoSolve ist tac

990 scriptTy = tacticTy

993 scriptTy = tacticTy

991

994

992 runT (Reflect v) = do attack -- let x = reflect v in ...

995 runT (Reflect v) = do attack -- let x = reflect v in ...

993− tyn <- getNameFrom (MN 0 "letty")

996+ tyn <- getNameFrom (sMN 0 "letty")

994 claim tyn RType

997 claim tyn RType

995− valn <- getNameFrom (MN 0 "letval")

998+ valn <- getNameFrom (sMN 0 "letval")

996 claim valn (Var tyn)

999 claim valn (Var tyn)

997− letn <- getNameFrom (MN 0 "letvar")

1000+ letn <- getNameFrom (sMN 0 "letvar")

998 letbind letn (Var tyn) (Var valn)

1001 letbind letn (Var tyn) (Var valn)

999 focus valn

1002 focus valn

1000− elab ist toplevel False [] (MN 0 "tac") v

1003+ elab ist toplevel False [] (sMN 0 "tac") v

1001 (value, _) <- get_type_val (Var letn)

1004 (value, _) <- get_type_val (Var letn)

1002 ctxt <- get_context

1005 ctxt <- get_context

1003 env <- get_env

1006 env <- get_env

1004 let value' = hnf ctxt env value

1007 let value' = hnf ctxt env value

1005 runTac autoSolve ist (Exact $ PQuote (reflect value'))

1008 runTac autoSolve ist (Exact $ PQuote (reflect value'))

1006 runT (Fill v) = do attack -- let x = fill x in ...

1009 runT (Fill v) = do attack -- let x = fill x in ...

1007− tyn <- getNameFrom (MN 0 "letty")

1010+ tyn <- getNameFrom (sMN 0 "letty")

1008 claim tyn RType

1011 claim tyn RType

1009− valn <- getNameFrom (MN 0 "letval")

1012+ valn <- getNameFrom (sMN 0 "letval")

1010 claim valn (Var tyn)

1013 claim valn (Var tyn)

1011− letn <- getNameFrom (MN 0 "letvar")

1014+ letn <- getNameFrom (sMN 0 "letvar")

1012 letbind letn (Var tyn) (Var valn)

1015 letbind letn (Var tyn) (Var valn)

1013 focus valn

1016 focus valn

1014− elab ist toplevel False [] (MN 0 "tac") v

1017+ elab ist toplevel False [] (sMN 0 "tac") v

1015 (value, _) <- get_type_val (Var letn)

1018 (value, _) <- get_type_val (Var letn)

1016 ctxt <- get_context

1019 ctxt <- get_context

1017 env <- get_env

1020 env <- get_env

@@ -1021,7 +1024,7 @@ runTac autoSolve ist tac

1021 runT (GoalType n tac) = do g <- goal

1024 runT (GoalType n tac) = do g <- goal

1022 case unApply g of

1025 case unApply g of

1023 (P _ n' _, _) ->

1026 (P _ n' _, _) ->

1024− if nsroot n' == UN n

1027+ if nsroot n' == sUN n

1025 then runT tac

1028 then runT tac

1026 else fail "Wrong goal type"

1029 else fail "Wrong goal type"

1027 _ -> fail "Wrong goal type"

1030 _ -> fail "Wrong goal type"

@@ -1034,7 +1037,7 @@ runTac autoSolve ist tac

1034

1037

1035-- | Prefix a name with the "Language.Reflection" namespace

1038-- | Prefix a name with the "Language.Reflection" namespace

1036reflm :: String -> Name

1039reflm :: String -> Name

1037−reflm n = NS (UN n) ["Reflection", "Language"]

1040+reflm n = sNS (sUN n) ["Reflection", "Language"]

1038

1041

1039

1042

1040-- | Reify tactics from their reflected representation

1043-- | 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

1056reifyApp ist t [Constant (Str n), x]

1059reifyApp ist t [Constant (Str n), x]

1057 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

1060 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

1058reifyApp _ t [Constant (Str n)]

1061reifyApp _ t [Constant (Str n)]

1059− | t == reflm "Intro" = return $ Intro [UN n]

1062+ | t == reflm "Intro" = return $ Intro [sUN n]

1060reifyApp ist t [t']

1063reifyApp ist t [t']

1061 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

1064 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

1062reifyApp ist t [t']

1065reifyApp ist t [t']

@@ -1147,13 +1150,13 @@ reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

1147

1150

1148reifyTTNameApp :: Name -> [Term] -> ElabD Name

1151reifyTTNameApp :: Name -> [Term] -> ElabD Name

1149reifyTTNameApp t [Constant (Str n)]

1152reifyTTNameApp t [Constant (Str n)]

1150− | t == reflm "UN" = return $ UN n

1153+ | t == reflm "UN" = return $ sUN n

1151reifyTTNameApp t [n, ns]

1154reifyTTNameApp t [n, ns]

1152 | t == reflm "NS" = do n' <- reifyTTName n

1155 | t == reflm "NS" = do n' <- reifyTTName n

1153 ns' <- reifyTTNamespace ns

1156 ns' <- reifyTTNamespace ns

1154− return $ NS n' ns'

1157+ return $ sNS n' ns'

1155reifyTTNameApp t [Constant (I i), Constant (Str n)]

1158reifyTTNameApp t [Constant (I i), Constant (Str n)]

1156− | t == reflm "MN" = return $ MN i n

1159+ | t == reflm "MN" = return $ sMN i n

1157reifyTTNameApp t []

1160reifyTTNameApp t []

1158 | t == reflm "NErased" = return NErased

1161 | t == reflm "NErased" = return NErased

1159reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

1162reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

@@ -1162,9 +1165,9 @@ reifyTTNamespace :: Term -> ElabD [String]

1162reifyTTNamespace t@(App _ _)

1165reifyTTNamespace t@(App _ _)

1163 = case unApply t of

1166 = case unApply t of

1164 (P _ f _, [Constant StrType])

1167 (P _ f _, [Constant StrType])

1165− | f == NS (UN "Nil") ["List", "Prelude"] -> return []

1168+ | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

1166 (P _ f _, [Constant StrType, Constant (Str n), ns])

1169 (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)

1168 _ -> fail ("Unknown reflection namespace arg: " ++ show t)

1171 _ -> fail ("Unknown reflection namespace arg: " ++ show t)

1169reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

1172reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

1170

1173

@@ -1286,19 +1289,19 @@ reflectNameType (TCon x y)

1286 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

1289 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

1287

1290

1288reflectName :: Name -> Raw

1291reflectName :: Name -> Raw

1289−reflectName (UN str)

1292+reflectName (UN s)

1290− = reflCall "UN" [RConstant (Str str)]

1293+ = reflCall "UN" [RConstant (Str (str s))]

1291reflectName (NS n ns)

1294reflectName (NS n ns)

1292 = reflCall "NS" [ reflectName n

1295 = reflCall "NS" [ reflectName n

1293 , foldr (\ n s ->

1296 , foldr (\ n s ->

1294− raw_apply ( Var $ NS (UN "::") ["List", "Prelude"] )

1297+ raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )

1295 [ RConstant StrType, RConstant (Str n), s ])

1298 [ RConstant StrType, RConstant (Str n), s ])

1296− ( raw_apply ( Var $ NS (UN "Nil") ["List", "Prelude"] )

1299+ ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )

1297 [ RConstant StrType ])

1300 [ RConstant StrType ])

1298− ns

1301+ (map str ns)

1299 ]

1302 ]

1300reflectName (MN i n)

1303reflectName (MN i n)

1301− = reflCall "MN" [RConstant (I i), RConstant (Str n)]

1304+ = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]

1302reflectName (NErased) = Var (reflm "NErased")

1305reflectName (NErased) = Var (reflm "NErased")

1303reflectName n = Var (reflm "NErased") -- special name, not yet implemented

1306reflectName n = Var (reflm "NErased") -- special name, not yet implemented

1304

1307

@@ -1355,7 +1358,7 @@ reflectEnv = foldr consToEnvList emptyEnvList

1355 where

1358 where

1356 consToEnvList :: (Name, Binder Term) -> Raw -> Raw

1359 consToEnvList :: (Name, Binder Term) -> Raw -> Raw

1357 consToEnvList (n, b) l

1360 consToEnvList (n, b) l

1358− = raw_apply (Var (NS (UN "::") ["List", "Prelude"]))

1361+ = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))

1359 [ envTupleType

1362 [ envTupleType

1360 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

1363 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

1361 , (RApp (Var $ reflm "Binder")

1364 , (RApp (Var $ reflm "Binder")

@@ -1367,19 +1370,19 @@ reflectEnv = foldr consToEnvList emptyEnvList

1367 ]

1370 ]

1368

1371

1369 emptyEnvList :: Raw

1372 emptyEnvList :: Raw

1370− emptyEnvList = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"]))

1373+ emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

1371 [envTupleType]

1374 [envTupleType]

1372

1375

1373-- | Reflect an error into the internal datatype of Idris -- TODO

1376-- | Reflect an error into the internal datatype of Idris -- TODO

1374rawBool :: Bool -> Raw

1377rawBool :: Bool -> Raw

1375−rawBool True = Var (NS (UN "True") ["Bool", "Prelude"])

1378+rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

1376−rawBool False = Var (NS (UN "False") ["Bool", "Prelude"])

1379+rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

1377

1380

1378rawNil :: Raw -> Raw

1381rawNil :: 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]

1380

1383

1381rawCons :: Raw -> Raw -> Raw -> Raw

1384rawCons :: 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]

1383

1386

1384rawList :: Raw -> [Raw] -> Raw

1387rawList :: Raw -> [Raw] -> Raw

1385rawList ty = foldr (rawCons ty) (rawNil ty)

1388rawList ty = foldr (rawCons ty) (rawNil ty)

@@ -1445,7 +1448,7 @@ reflectErr (NotInjective t1 t2 t3) =

1445reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

1448reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

1446reflectErr (CantResolveAlts ss) =

1449reflectErr (CantResolveAlts ss) =

1447 raw_apply (Var $ reflErrName "CantResolve")

1450 raw_apply (Var $ reflErrName "CantResolve")

1448− [rawList (Var $ (UN "String")) (map (RConstant . Str) ss)]

1451+ [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

1449reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

1452reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

1450reflectErr UniverseError = Var $ reflErrName "UniverseError"

1453reflectErr UniverseError = Var $ reflErrName "UniverseError"

1451reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

1454reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

@@ -1470,7 +1473,7 @@ reflectErr (ProviderError str) =

1470 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

1473 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

1471reflectErr (LoadingFailed str err) =

1474reflectErr (LoadingFailed str err) =

1472 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

1475 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]

1474

1477

1475withErrorReflection :: Idris a -> Idris a

1478withErrorReflection :: Idris a -> Idris a

1476withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1479withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

@@ -1504,11 +1507,12 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1504 parts -> ReflectionError errorparts e

1507 parts -> ReflectionError errorparts e

1505

1508

1506 fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1509 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

1508 fromTTMaybe x = Nothing

1512 fromTTMaybe x = Nothing

1509

1513

1510reflErrName :: String -> Name

1514reflErrName :: String -> Name

1511−reflErrName n = NS (UN n) ["Errors", "Reflection", "Language"]

1515+reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

1512

1516

1513reifyReportPart :: Term -> Idris ErrorReportPart

1517reifyReportPart :: Term -> Idris ErrorReportPart

1514reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

1518reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

src/Idris/IBC.hs+8−1

@@ -14,6 +14,8 @@ import Data.Binary

14import Data.Vector.Binary

15import Data.List

16import Data.ByteString.Lazy as B hiding (length, elem, map)

17+import qualified Data.Text as T

18+

17import Control.Monad

19import Control.Monad

18import Control.Monad.State hiding (get, put)

20import Control.Monad.State hiding (get, put)

19import qualified Control.Monad.State as ST

21import qualified Control.Monad.State as ST

@@ -26,7 +28,7 @@ import Debug.Trace

26import Paths_idris

28import Paths_idris

28ibcVersion :: Word8

30ibcVersion :: Word8

29−ibcVersion = 53

31+ibcVersion = 54

31data IBCFile = IBCFile { ver :: Word8,

33data IBCFile = IBCFile { ver :: Word8,

32 sourcefile :: FilePath,

34 sourcefile :: FilePath,

@@ -498,6 +500,11 @@ instance Binary Name where

498 return (SymRef x1)

500 return (SymRef x1)

499 _ -> error "Corrupted binary data for Name"

501 _ -> error "Corrupted binary data for Name"

500

502

503+instance Binary T.Text where

504+ put x = put (str x)

505+ get = do x <- get

506+ return (txt x)

507+

501instance Binary SpecialName where

508instance Binary SpecialName where

502 put x

509 put x

503 = case x of

510 = case x of

src/Idris/ParseData.hs+1−1

@@ -144,7 +144,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

144 mkPApp fc t [] = t

145 mkPApp fc t xs = PApp fc t (map pexp xs)

146 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

148 combineDataOpts :: DataOpts -> DataOpts

149 combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts

150

src/Idris/ParseExpr.hs+26−26

@@ -295,7 +295,7 @@ simpleExpr syn =

295 fc <- getFC

296 return (modifyConst syn fc (PConstant c)))

297 <|> try (do symbol "'"; fc <- getFC; str <- name

298− return (PApp fc (PRef fc (UN "Symbol_"))

298+ return (PApp fc (PRef fc (sUN "Symbol_"))

299 [pexp (PConstant (Str (show str)))]))

300 <|> do fc <- getFC

301 x <- fnName

@@ -360,12 +360,12 @@ bracketed syn =

360 l <- expr' syn

361 o <- operator

362 lchar ')'

363− return $ PLam (MN 1000 "ARG") Placeholder

363+ return $ PLam (sMN 1000 "ARG") Placeholder

364− (PApp fc0 (PRef fc0 (UN o)) [pexp l,

364+ (PApp fc0 (PRef fc0 (sUN o)) [pexp l,

365− pexp (PRef fc0 (MN 1000 "ARG"))]))

365+ pexp (PRef fc0 (sMN 1000 "ARG"))]))

366 <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

367− return $ PLam (MN 1000 "ARG") Placeholder

367+ return $ PLam (sMN 1000 "ARG") Placeholder

368− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),

368+ (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

369 pexp e]))

370 <|> try (do ln <- name; lchar ':'

371 lty <- expr syn

@@ -388,7 +388,7 @@ modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

388modifyConst syn fc (PConstant (BI x))

389 | not (inPattern syn)

390 = 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)))]

392 : consts)

393 | otherwise = PAlternative False consts

394 where

@@ -420,8 +420,8 @@ listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lc

420 <?> "list expression"

421 where

422 mkList :: FC -> [PTerm] -> PTerm

423− mkList fc [] = PRef fc (UN "Nil")

423+ mkList fc [] = PRef fc (sUN "Nil")

424− mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]

424+ mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

425

426

427{- | Parses an alternative expression

@@ -466,10 +466,10 @@ matchApp syn = do ty <- simpleExpr syn

466 symbol "<=="

467 fc <- getFC

468 f <- fnName

469− return (PLet (MN 0 "match")

469+ return (PLet (sMN 0 "match")

470 ty

471 (PMatchApp fc f)

472− (PRef fc (MN 0 "match")))

472+ (PRef fc (sMN 0 "match")))

473 <?> "matching application expression"

474

475{- | Parses a unification log expression

@@ -512,12 +512,12 @@ app syn = do f <- reserved "mkForeign"

512 i <- get

513 -- mkForeign f args ==>

514 -- liftPrimIO (\w => mkForeignPrim f args w)

515− let ap = PApp fc (PRef fc (UN "liftPrimIO"))

515+ let ap = PApp fc (PRef fc (sUN "liftPrimIO"))

516− [pexp (PLam (MN 0 "w")

516+ [pexp (PLam (sMN 0 "w")

517 Placeholder

518− (PApp fc (PRef fc (UN "mkForeignPrim"))

518+ (PApp fc (PRef fc (sUN "mkForeignPrim"))

519 (fn : args ++

520− [pexp (PRef fc (MN 0 "w"))])))]

520+ [pexp (PRef fc (sMN 0 "w"))])))]

521 return (dslify i ap)

522

523 <|> do f <- simpleExpr syn

@@ -611,8 +611,8 @@ recordType syn

611 rec <- optional (simpleExpr syn)

612 case rec of

613 Nothing ->

614− return (PLam (MN 0 "fldx") Placeholder

614+ return (PLam (sMN 0 "fldx") Placeholder

615− (applyAll fc fields (PRef fc (MN 0 "fldx"))))

615+ (applyAll fc fields (PRef fc (sMN 0 "fldx"))))

616 Just v -> return (applyAll fc fields v)

617 <?> "record setting expression"

618 where fieldType :: IdrisParser (Name, PTerm)

@@ -628,8 +628,8 @@ recordType syn

628

629-- | Creates setters for record types on necessary functions

630mkType :: Name -> Name

631−mkType (UN n) = UN ("set_" ++ n)

631+mkType (UN n) = sUN ("set_" ++ str n)

632−mkType (MN 0 n) = MN 0 ("set_" ++ n)

632+mkType (MN 0 n) = sMN 0 ("set_" ++ str n)

633mkType (NS n s) = NS (mkType n) s

634

635{- | Parses a type signature

@@ -645,7 +645,7 @@ TypeExpr ::= ConstraintList? Expr;

645typeExpr :: SyntaxInfo -> IdrisParser PTerm

646typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

647 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)

649 <?> "type signature"

650

651{- | Parses a lambda expression

@@ -678,8 +678,8 @@ lambda syn = do lchar '\\'

678 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

679 pmList [] sc = sc

680 pmList ((i, (fc, x)) : xs) sc

681− = PLam (MN i "lamp") Placeholder

681+ = PLam (sMN i "lamp") Placeholder

682− (PCase fc (PRef fc (MN i "lamp"))

682+ (PCase fc (PRef fc (sMN i "lamp"))

683 [(x, pmList xs sc)])

684

685{- | Parses a term rewrite expression

@@ -696,7 +696,7 @@ rewriteTerm syn = do reserved "rewrite"

696 giving <- optional (do symbol "==>"; expr' syn)

697 reserved "in"; sc <- expr syn

698 return (PRewrite fc

699− (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc

699+ (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

700 giving)

701 <?> "term rewrite expression"

702

@@ -861,7 +861,7 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

861 where nameOrPlaceholder :: IdrisParser Name

862 nameOrPlaceholder = fnName

863 <|> do symbol "_"

864− return (MN 0 "underscore")

864+ return (sMN 0 "underscore")

865 <?> "name or placeholder"

866

867{- | Parses a list comprehension

@@ -885,11 +885,11 @@ comprehension syn

885 qs <- sepBy1 (do_ syn) (lchar ',')

886 lchar ']'

887 return (PDoBlock (map addGuard qs ++

888− [DoExp fc (PApp fc (PRef fc (UN "return"))

888+ [DoExp fc (PApp fc (PRef fc (sUN "return"))

889 [pexp pat])]))

890 <?> "list comprehension"

891 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"))

893 [pexp e])

894 addGuard x = x

895

src/Idris/ParseHelpers.hs+2−2

@@ -230,8 +230,8 @@ initsEndAt p (x:xs) | p x = [] : x_inits_xs

230 namespace.

231-}

232mkName :: (String, String) -> Name

233−mkName (n, "") = UN n

233+mkName (n, "") = sUN n

234−mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

234+mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))

235 where parseNS x = case span (/= '.') x of

236 (x, "") -> [x]

237 (x, '.':y) -> x : parseNS y

src/Idris/ParseOps.hs+5−5

@@ -33,21 +33,21 @@ import qualified Data.ByteString.UTF8 as UTF8

33-- using pre-build and user-defined operator/fixity declarations

34table :: [FixDecl] -> OperatorTable IdrisParser PTerm

35table fixes

36− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

36+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (sUN "-"))

37− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

37+ [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [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]]

43-- | Calculates table for fixtiy declarations

44toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

45toTable fs = map (map toBin)

46 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

47 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])

49 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)

51 assoc (Infixl _) = AssocLeft

52 assoc (Infixr _) = AssocRight

53 assoc (InfixN _) = AssocNone

src/Idris/Parser.hs+9−9

@@ -300,9 +300,9 @@ fnDecl' syn = checkFixity $

300 getName (PTy _ _ _ _ n _) = Just n

301 getName _ = Nothing

302 fixityOK (NS n _) = fixityOK n

303− fixityOK (UN n) | all (flip elem opChars) n =

303+ fixityOK (UN n) | all (flip elem opChars) (str n) =

304 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

306 | otherwise = return True

307 fixityOK _ = return True

308

@@ -517,7 +517,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

517 cn <- name

518 args <- many (simpleExpr syn)

519 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

521 ds <- option [] (instanceBlock syn)

522 return [PInstance syn fc cs cn args t en ds]

523 <?> "instance declaration"

@@ -575,7 +575,7 @@ Pattern ::= Clause;

575pattern :: SyntaxInfo -> IdrisParser PDecl

576pattern syn = do fc <- getFC

577 clause <- clause syn

578− return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later

578+ return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later

579 <?> "pattern"

580

581{- | Parse a constant applicative form declaration

@@ -617,7 +617,7 @@ rhs syn n = do lchar '='; expr syn

617 <|> do reserved "impossible"; return PImpossible

618 <?> "function right hand side"

619 where mkN :: Name -> Name

620− mkN (UN x) = UN (x++"_lemma_1")

620+ mkN (UN x) = sUN (str x++"_lemma_1")

621 mkN (NS x n) = NS (mkN x) n

622 n' :: Name

623 n' = mkN n

@@ -625,7 +625,7 @@ rhs syn n = do lchar '='; expr syn

625 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)

626 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)

627 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))

629

630{- |Parses a function clause

631RHSOrWithBlock ::= RHS WhereOrTerminator

@@ -679,10 +679,10 @@ clause syn

679 return x,

680 do terminator

681 return ([], [])]

682− let capp = PLet (MN 0 "match")

682+ let capp = PLet (sMN 0 "match")

683 ty

684 (PMatchApp fc n)

685− (PRef fc (MN 0 "match"))

685+ (PRef fc (sMN 0 "match"))

686 ist <- get

687 put (ist { lastParse = Just n })

688 return $ PClause fc n capp [] r wheres

@@ -693,7 +693,7 @@ clause syn

693 when (op == "=" || op == "?=" ) $

694 fail "infix clause definition with \"=\" and \"?=\" not supported "

695 return (l, op))

696− let n = expandNS syn (UN op)

696+ let n = expandNS syn (sUN op)

697 r <- argExpr syn

698 fc <- getFC

699 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

54 sc' <- unifyEq xs sc

55 return (Bind n (Pi t) sc')

56 unifyEq xs t = do args <- get

57− put (args ++ (zip xs (repeat (UN "_"))))

57+ put (args ++ (zip xs (repeat (sUN "_"))))

58 return t

60mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

@@ -122,7 +122,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

122 | x && imparg imp = (ImplicitS, tm)

123 | x = (ExplicitS, tm)

124 | imparg imp = (ImplicitD, tm)

125− | otherwise = (ExplicitD, (P Ref (UN (show n ++ "arg")) Erased))

125+ | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126

127 imparg (PExp _ _ _ _) = False

128 imparg _ = True

src/Idris/Primitives.hs+50−50

@@ -26,7 +26,7 @@ data Prim = Prim { p_name :: Name,

27ty :: [Const] -> Const -> Type

28ty [] 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)

31total, partial :: Totality

32total = Total []

@@ -94,83 +94,83 @@ primitives =

94 iCoerce ITNative (ITFixed IT64) "trunc" trunc LTrunc,

95 iCoerce ITBig ITChar "trunc" trunc LTrunc,

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 (+))

98 (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 (-))

100 (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 (*))

102 (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 (/))

104 (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 (==))

106 (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 (<))

108 (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 (<=))

110 (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 (>))

112 (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 (>=))

114 (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 (++))

116 (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 (==))

118 (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 (<))

120 (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)

122 (1, LStrLen) total,

123 -- 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)

125 (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)

127 (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)

129 (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)

131 (1, LFloatStr) total,

132

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)

134 (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)

136 (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)

138 (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)

140 (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)

142 (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)

144 (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)

146 (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)

148 (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)

150 (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)

152 (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)

154 (1, LFCeil) total,

155

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)

157 (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)

159 (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)

161 (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)

163 (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)

165 (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)

167 (1, LReadStr) partial,

168− Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

168+ Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

169 (0, LVMPtr) total,

170 -- Streams

171− Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

171+ Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172 (0, LStdIn) partial,

173− Prim (UN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

173+ Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

174 (0, LNullPtr) total

175 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

176 ++ concatMap vecOps vecTypes

@@ -221,13 +221,13 @@ intArith ity =

221

222intConv :: IntTy -> [Prim]

223intConv 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

225 (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)

227 (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

229 (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)

231 (1, LFloatInt ity) total

232 ]

233

@@ -246,13 +246,13 @@ vecCmps ity =

246

247vecOps :: IntTy -> [Prim]

248vecOps ity@(ITVec elem count) =

249− [ Prim (UN $ "prim__mk" ++ intTyName ity)

249+ [ Prim (sUN $ "prim__mk" ++ intTyName ity)

250 (ty (replicate count . AType . ATInt . ITFixed $ elem) (AType . ATInt $ ity))

251 count (mkVecCon elem count) (count, LMkVec elem count) total

252− , Prim (UN $ "prim__index" ++ intTyName ity)

252+ , Prim (sUN $ "prim__index" ++ intTyName ity)

253 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32))] (AType . ATInt . ITFixed $ elem))

254 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)

256 (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32)), AType . ATInt . ITFixed $ elem]

257 (AType . ATInt $ ity))

258 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces

@@ -260,7 +260,7 @@ vecOps ity@(ITVec elem count) =

260

261bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim

262bitcastPrim 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)

264 (1, prim) total

265

266vecBitcasts :: [IntTy] -> [Prim]

@@ -377,23 +377,23 @@ intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show cou

377

378iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

379iCmp ity op self impl irop totality

380− = Prim (UN $ "prim__" ++ op ++ intTyName ity)

380+ = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

381 (ty (replicate 2 . AType . ATInt $ ity) (AType (ATInt (if self then ity else ITNative))))

382 2 impl (2, irop ity) totality

383

384iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

385iBinOp ity op impl irop totality

386− = Prim (UN $ "prim__" ++ op ++ intTyName ity)

386+ = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

387 (ty (replicate 2 . AType . ATInt $ ity) (AType . ATInt $ ity))

388 2 impl (2, irop ity) totality

389iUnOp ity op impl irop totality

390− = Prim (UN $ "prim__" ++ op ++ intTyName ity)

390+ = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

391 (ty [AType . ATInt $ ity] (AType . ATInt $ ity))

392 1 impl (1, irop ity) totality

393

394iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim

395iCoerce from to op impl irop =

396− Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

396+ Prim (sUN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

397 (ty [AType . ATInt $ from] (AType . ATInt $ to)) 1 (impl from to) (1, irop from to) total

398

399fBin :: (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

102 tPretty t = pretty $ delab ist t

103

104 prettyPs [] = empty

105− prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs

105+ prettyPs ((MN _ r, _) : bs)

106+ | r == txt "rewrite_rule" = prettyPs bs

106 prettyPs ((n, Let t v) : bs) =

107 prettyPs ((n, Let t v) : bs) =

107 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>

108 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>

108 tPretty t $$ prettyPs bs)

109 tPretty t $$ prettyPs bs)

src/Idris/Providers.hs+14−7

@@ -11,17 +11,24 @@ import Debug.Trace

12-- | Wrap a type provider in the type of type providers

13providerTy :: 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"]

16-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

20-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

17getProvided :: TT Name -> Idris (TT Name)

21getProvided :: TT Name -> Idris (TT Name)

18−getProvided tm | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm

22+getProvided tm | (P _ pioret _, [tp, result]) <- unApply tm

19− , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =

23+ , (P _ nm _, [_, err]) <- unApply result

24+ , pioret == ioret && nm == ermod

20− case err of

25+ = case err of

21 Constant (Str msg) -> ierror . ProviderError $ msg

26 Constant (Str msg) -> ierror . ProviderError $ msg

22 _ -> ifail "Internal error in type provider, non-normalised error"

27 _ -> ifail "Internal error in type provider, non-normalised error"

23− | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm

28+ | (P _ pioret _, [tp, result]) <- unApply tm

24− , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =

29+ , (P _ nm _, [_, res]) <- unApply result

30+ , pioret == ioret && nm == prmod

25− return res

31+ = return res

26 | otherwise = ifail $ "Internal type provider error: result was not " ++

32 | otherwise = ifail $ "Internal type provider error: result was not " ++

27 "IO (Provider a), or perhaps missing normalisation."

33 "IO (Provider a), or perhaps missing normalisation."

34+

src/Idris/REPL.hs+15−15

@@ -247,19 +247,19 @@ ideslave orig mods

247 Just x -> iPrintError $ "didn't load " ++ filename

248 ideslave orig [filename]

249 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)))

251 Just (IdeSlave.CaseSplit line name) ->

252− process stdout fn (CaseSplitAt False line (UN name))

252+ process stdout fn (CaseSplitAt False line (sUN name))

253 Just (IdeSlave.AddClause line name) ->

254− process stdout fn (AddClauseFrom False line (UN name))

254+ process stdout fn (AddClauseFrom False line (sUN name))

255 Just (IdeSlave.AddProofClause line name) ->

256− process stdout fn (AddProofClauseFrom False line (UN name))

256+ process stdout fn (AddProofClauseFrom False line (sUN name))

257 Just (IdeSlave.AddMissing line name) ->

258− process stdout fn (AddMissing False line (UN name))

258+ process stdout fn (AddMissing False line (sUN name))

259 Just (IdeSlave.MakeWithBlock line name) ->

260− process stdout fn (MakeWith False line (UN name))

260+ process stdout fn (MakeWith False line (sUN name))

261 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))

263 Nothing -> do iPrintError "did not understand")

264 (\e -> do iPrintError $ show e))

265 (\e -> do iPrintError $ show e)

@@ -408,7 +408,7 @@ edit f orig

408 , idris_colourTheme = idris_colourTheme i

409 }

410 loadInputs stdout [f]

411− clearOrigPats

411+-- clearOrigPats

412 iucheck

413 return ()

414 where getEditor env | Just ed <- lookup "EDITOR" env = ed

@@ -444,7 +444,7 @@ process h fn (Eval t)

444 let tm' = force (normaliseAll ctxt [] tm)

445 let ty' = force (normaliseAll ctxt [] ty)

446 -- Add value to context, call it "it"

447− updateContext (addCtxtDef (UN "it") (Function ty' tm'))

447+ updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

448 ist <- getIState

449 logLvl 3 $ "Raw: " ++ show (tm', ty')

450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

@@ -485,7 +485,7 @@ process h fn (Check (PRef _ n))

485 = let current = " " ++

486 (case n of

487 MN _ _ -> "_"

488− UN ('_':'_':_) -> "_"

488+ UN nm | ('_':'_':_) <- str nm -> "_"

489 _ -> showName (Just ist) [] False c n) ++

490 " : " ++ showImp (Just ist) imp c t ++ "\n"

491 in

@@ -852,8 +852,8 @@ process h fn (TestInline t)

852process h fn Execute

853 = do (m, _) <- elabVal toplevel False

854 (PApp fc

855− (PRef fc (UN "run__IO"))

855+ (PRef fc (sUN "run__IO"))

856− [pexp $ PRef fc (NS (UN "main") ["Main"])])

856+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

857-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

858 (tmpn, tmph) <- runIO tempfile

859 runIO $ hClose tmph

@@ -864,8 +864,8 @@ process h fn Execute

864 where fc = fileFC "main"

865process h fn (Compile codegen f)

866 = do (m, _) <- elabVal toplevel False

867− (PApp fc (PRef fc (UN "run__IO"))

867+ (PApp fc (PRef fc (sUN "run__IO"))

868− [pexp $ PRef fc (NS (UN "main") ["Main"])])

868+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

869 compile codegen f m

870 where fc = fileFC "main"

871process h fn (LogLvl i) = setLogLevel i

@@ -1221,7 +1221,7 @@ idrisMain opts =

1221 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

1222

1223 when (runrepl && not idesl) $ do

1224− clearOrigPats

1224+-- clearOrigPats

1225 initScript

1226 startServer orig inputs

1227 runInputT (replSettings (Just historyFile)) $ repl orig inputs

src/Idris/Transforms.hs+3−3

@@ -39,8 +39,8 @@ instance Transform CaseAlt where

40natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]

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

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

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

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

45zero :: TT Name -> TT Name

46zero (P _ n _) | n == zname

@@ -49,7 +49,7 @@ zero x = x

50suc :: TT Name -> TT Name

51suc (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]

53suc x = x

55natcase :: SC -> SC

src/Pkg/PParser.hs+1−1

@@ -27,7 +27,7 @@ data PkgDesc = PkgDesc { pkgname :: String,

27 }

28 deriving Show

30−defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (UN "") Nothing

30+defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing

32parseDesc :: FilePath -> IO PkgDesc

33parseDesc fp = do p <- readFile fp

src/Pkg/Package.hs+3−3

@@ -108,8 +108,8 @@ testLib warn p f

108rmIBC :: Name -> IO ()

109rmIBC m = rmFile $ toIBCFile m

110

111−toIBCFile (UN n) = n ++ ".ibc"

111+toIBCFile (UN n) = str n ++ ".ibc"

112−toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : ns))

112+toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : map str ns))

113

114installIBC :: String -> Name -> IO ()

115installIBC p m = do let f = toIBCFile m

@@ -120,7 +120,7 @@ installIBC p m = do let f = toIBCFile m

120 copyFile f (destdir </> takeFileName f)

121 return ()

122 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))

124

125installObj :: String -> String -> IO ()

126installObj p o = do d <- getTargetDir