From 32e26c5bd17f0b846530b4385560309d19f0c0c9 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Wed, 15 Sep 2021 13:20:58 +0100 Subject: [PATCH] [ refactor ] introduce UserName for (UN/RF) (#1926) Instead of having UN & RF (& Hole in the near future & maybe even more later e.g. operator names) we have a single UN constructor that takes a UserName instead of a String. UserName is (for now) ```idris data UserName : Type where Basic : String -> UserName -- default name constructor e.g. map Field : String -> UserName -- field accessor e.g. .fst Underscore : UserName -- no name e.g. _ ``` This is extracted from the draft PR #1852 which is too big to easily debug. Once this is working, I can go back to it. --- idris2api.ipkg | 1 + libs/base/Language/Reflection/TT.idr | 20 +- src/Compiler/Common.idr | 8 +- src/Compiler/CompileExpr.idr | 61 ++--- src/Compiler/ES/Codegen.idr | 51 ++-- src/Compiler/Inline.idr | 2 +- src/Compiler/Interpreter/VMCode.idr | 2 +- src/Compiler/LambdaLift.idr | 2 +- src/Compiler/RefC/RefC.idr | 41 ++-- src/Compiler/Scheme/Chez.idr | 2 +- src/Compiler/Scheme/Common.idr | 41 ++-- src/Compiler/Scheme/Gambit.idr | 2 +- src/Compiler/Scheme/Racket.idr | 2 +- src/Core/CaseBuilder.idr | 8 +- src/Core/CompileExpr.idr | 2 +- src/Core/Context.idr | 14 +- src/Core/Context/Context.idr | 6 +- src/Core/Env.idr | 2 +- src/Core/Name.idr | 143 ++++++++--- src/Core/Normalise/Eval.idr | 10 +- src/Core/Primitives.idr | 16 +- src/Core/Reflect.idr | 243 +++++++++--------- src/Core/TT.idr | 2 +- src/Core/TTC.idr | 12 +- src/Core/Termination.idr | 4 +- src/Core/UnifyState.idr | 3 +- src/Core/Value.idr | 2 +- src/Idris/Desugar.idr | 87 +++---- src/Idris/Doc/String.idr | 16 +- src/Idris/Elab/Implementation.idr | 19 +- src/Idris/Elab/Interface.idr | 28 ++- src/Idris/IDEMode/CaseSplit.idr | 4 +- src/Idris/IDEMode/Commands.idr | 4 - src/Idris/IDEMode/Holes.idr | 2 +- src/Idris/IDEMode/REPL.idr | 29 ++- src/Idris/Package.idr | 2 +- src/Idris/Parser.idr | 51 ++-- src/Idris/Parser/Let.idr | 10 +- src/Idris/Pretty.idr | 4 +- src/Idris/REPL.idr | 21 +- src/Idris/Resugar.idr | 32 +-- src/Idris/SetOptions.idr | 4 +- src/Idris/Syntax.idr | 21 +- src/Libraries/Data/ANameMap.idr | 6 +- src/Libraries/Data/StringMap.idr | 8 - src/Libraries/Data/UserNameMap.idr | 326 +++++++++++++++++++++++++ src/Parser/Lexer/Source.idr | 16 +- src/Parser/Rule/Source.idr | 12 +- src/TTImp/BindImplicits.idr | 26 +- src/TTImp/Elab/Ambiguity.idr | 6 +- src/TTImp/Elab/App.idr | 8 +- src/TTImp/Elab/Case.idr | 4 +- src/TTImp/Elab/Check.idr | 8 +- src/TTImp/Elab/Hole.idr | 4 +- src/TTImp/Elab/ImplicitBind.idr | 2 +- src/TTImp/Elab/Record.idr | 9 +- src/TTImp/Elab/RunElab.idr | 6 +- src/TTImp/Elab/Term.idr | 10 +- src/TTImp/Interactive/CaseSplit.idr | 8 +- src/TTImp/Interactive/ExprSearch.idr | 4 +- src/TTImp/Interactive/GenerateDef.idr | 8 +- src/TTImp/Interactive/MakeLemma.idr | 2 +- src/TTImp/Parser.idr | 21 +- src/TTImp/PartialEval.idr | 10 +- src/TTImp/ProcessDef.idr | 10 +- src/TTImp/ProcessRecord.idr | 8 +- src/TTImp/ProcessRunElab.idr | 4 +- src/TTImp/ProcessType.idr | 4 +- src/TTImp/Reflect.idr | 188 +++++++------- src/TTImp/TTImp.idr | 15 +- src/TTImp/Unelab.idr | 2 +- src/TTImp/Utils.idr | 20 +- src/TTImp/WithClause.idr | 8 +- tests/idris2/docs002/expected | 6 +- tests/idris2/docs003/expected | 10 +- tests/idris2/reflection001/expected | 10 +- tests/idris2/reflection004/refdecl.idr | 5 +- tests/idris2/reg033/DerivingEq.idr | 2 +- 78 files changed, 1152 insertions(+), 680 deletions(-) create mode 100644 src/Libraries/Data/UserNameMap.idr diff --git a/idris2api.ipkg b/idris2api.ipkg index 92e1f7ab4..28871ff74 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -147,6 +147,7 @@ modules = Libraries.Data.String.Iterator, Libraries.Data.StringMap, Libraries.Data.StringTrie, + Libraries.Data.UserNameMap, Libraries.Data.Version, Libraries.System.Directory.Tree, diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr index b53e609ee..db504415a 100644 --- a/libs/base/Language/Reflection/TT.idr +++ b/libs/base/Language/Reflection/TT.idr @@ -97,22 +97,32 @@ data Constant | WorldType public export -data Name = UN String -- user defined name +data UserName + = Basic String -- default name constructor e.g. map + | Field String -- field accessor e.g. .fst + | Underscore -- no name e.g. _ + +public export +data Name = NS Namespace Name -- name in a namespace + | UN UserName -- user defined name | MN String Int -- machine generated name - | NS Namespace Name -- name in a namespace | DN String Name -- a name and how to display it - | RF String -- record field name | Nested (Int, Int) Name -- nested function name | CaseBlock String Int -- case block nested in (resolved) name | WithBlock String Int -- with block nested in (resolved) name +export +Show UserName where + show (Basic n) = n + show (Field n) = "." ++ n + show Underscore = "_" + export Show Name where show (NS ns n) = show ns ++ "." ++ show n - show (UN x) = x + show (UN x) = show x show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}" show (DN str y) = str - show (RF n) = "." ++ n show (Nested (outer, idx) inner) = show outer ++ ":" ++ show idx ++ ":" ++ show inner show (CaseBlock outer i) = "case block in " ++ show outer diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 4a62cc79e..a6ce3661b 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -199,10 +199,10 @@ replaceEntry (i, Just (ns, b)) natHackNames : List Name natHackNames - = [UN "prim__add_Integer", - UN "prim__sub_Integer", - UN "prim__mul_Integer", - NS typesNS (UN "prim__integerToNat")] + = [UN (Basic "prim__add_Integer"), + UN (Basic "prim__sub_Integer"), + UN (Basic "prim__mul_Integer"), + NS typesNS (UN $ Basic "prim__integerToNat")] -- Hmm, these dump functions are all very similar aren't they... dumpCases : String -> List (Name,FC,NamedDef) -> Core () diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 5328241f0..846e41af6 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -181,33 +181,33 @@ magic ms e = go ms e where %inline magic__integerToNat : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars magic__integerToNat fc fc' [k] - = CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k] + = CApp fc (CRef fc' (NS typesNS (UN $ Basic "prim__integerToNat"))) [k] magic__natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars magic__natMinus fc fc' [m,n] = magic__integerToNat fc fc' - [CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]] + [CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, n]] -- We don't reuse natMinus here because we assume that unsuc will only be called -- on S-headed numbers so we do not need the truncating integerToNat call! magic__natUnsuc : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars magic__natUnsuc fc fc' [m] - = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, CPrimVal fc (BI 1)] + = CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, CPrimVal fc (BI 1)] -- TODO: next release remove this and use %builtin pragma natHack : List Magic natHack = - [ MagicCRef (NS typesNS (UN "natToInteger")) 1 (\ _, _, [k] => k) - , MagicCRef (NS typesNS (UN "integerToNat")) 1 magic__integerToNat - , MagicCRef (NS typesNS (UN "plus")) 2 - (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n]) - , MagicCRef (NS typesNS (UN "mult")) 2 - (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n]) - , MagicCRef (NS typesNS (UN "minus")) 2 magic__natMinus - , MagicCRef (NS typesNS (UN "equalNat")) 2 - (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__eq_Integer")) [m, n]) - , MagicCRef (NS typesNS (UN "compareNat")) 2 - (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN "compareInteger"))) [m, n]) + [ MagicCRef (NS typesNS (UN $ Basic "natToInteger")) 1 (\ _, _, [k] => k) + , MagicCRef (NS typesNS (UN $ Basic "integerToNat")) 1 magic__integerToNat + , MagicCRef (NS typesNS (UN $ Basic "plus")) 2 + (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__add_Integer")) [m, n]) + , MagicCRef (NS typesNS (UN $ Basic "mult")) 2 + (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__mul_Integer")) [m, n]) + , MagicCRef (NS typesNS (UN $ Basic "minus")) 2 magic__natMinus + , MagicCRef (NS typesNS (UN $ Basic "equalNat")) 2 + (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__eq_Integer")) [m, n]) + , MagicCRef (NS typesNS (UN $ Basic "compareNat")) 2 + (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN $ Basic "compareInteger"))) [m, n]) ] -- get all transformation from %builtin pragmas @@ -321,8 +321,9 @@ mutual (CLet fc x True !(toCExp m n val) sc') rig toCExpTm m n (Bind fc x (Pi _ c e ty) sc) - = pure $ CCon fc (UN "->") TYCON Nothing [!(toCExp m n ty), - CLam fc x !(toCExp m n sc)] + = pure $ CCon fc (UN (Basic "->")) TYCON Nothing + [ !(toCExp m n ty) + , CLam fc x !(toCExp m n sc)] toCExpTm m n (Bind fc x b tm) = pure $ CErased fc -- We'd expect this to have been dealt with in toCExp, but for completeness... toCExpTm m n (App fc tm arg) @@ -339,9 +340,9 @@ mutual = let t = constTag c in if t == 0 then pure $ CPrimVal fc c - else pure $ CCon fc (UN (show c)) TYCON Nothing [] + else pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] toCExpTm m n (Erased fc _) = pure $ CErased fc - toCExpTm m n (TType fc) = pure $ CCon fc (UN "Type") TYCON Nothing [] + toCExpTm m n (TType fc) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing [] toCExp : {vars : _} -> {auto c : Ref Ctxt Defs} -> @@ -576,15 +577,15 @@ getFieldArgs defs cl getNArgs : {auto c : Ref Ctxt Defs} -> Defs -> Name -> List (Closure []) -> Core NArgs -getNArgs defs (NS _ (UN "IORes")) [arg] = pure $ NIORes arg -getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr -getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr -getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr -getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr -getNArgs defs (NS _ (UN "Buffer")) [] = pure NBuffer -getNArgs defs (NS _ (UN "ForeignObj")) [] = pure NForeignObj -getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit -getNArgs defs (NS _ (UN "Struct")) [n, args] +getNArgs defs (NS _ (UN $ Basic "IORes")) [arg] = pure $ NIORes arg +getNArgs defs (NS _ (UN $ Basic "Ptr")) [arg] = pure NPtr +getNArgs defs (NS _ (UN $ Basic "AnyPtr")) [] = pure NPtr +getNArgs defs (NS _ (UN $ Basic "GCPtr")) [arg] = pure NGCPtr +getNArgs defs (NS _ (UN $ Basic "GCAnyPtr")) [] = pure NGCPtr +getNArgs defs (NS _ (UN $ Basic "Buffer")) [] = pure NBuffer +getNArgs defs (NS _ (UN $ Basic "ForeignObj")) [] = pure NForeignObj +getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit +getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args] = do NPrimVal _ (Str n') <- evalClosure defs n | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct") pure (Struct n' !(getFieldArgs defs args)) @@ -641,9 +642,9 @@ nfToCFType _ s (NTCon fc n_in _ _ args) carg <- nfToCFType fc s narg pure (CFIORes carg) nfToCFType _ s (NType _) - = pure (CFUser (UN "Type") []) + = pure (CFUser (UN (Basic "Type")) []) nfToCFType _ s (NErased _ _) - = pure (CFUser (UN "__") []) + = pure (CFUser (UN (Basic "__")) []) nfToCFType fc s t = do defs <- get Ctxt ty <- quote defs [] t @@ -766,7 +767,7 @@ compileExp : {auto c : Ref Ctxt Defs} -> compileExp tm = do m <- builtinMagic s <- newRef NextSucc 0 - exp <- toCExp m (UN "main") tm + exp <- toCExp m (UN $ Basic "main") tm pure exp ||| Given a name, look up an expression, and compile it to a CExp in the environment diff --git a/src/Compiler/ES/Codegen.idr b/src/Compiler/ES/Codegen.idr index 37a7e3707..e40137cb0 100644 --- a/src/Compiler/ES/Codegen.idr +++ b/src/Compiler/ES/Codegen.idr @@ -83,13 +83,17 @@ keywordSafe s = s -- JS Name -------------------------------------------------------------------------------- +jsUserName : UserName -> String +jsUserName (Basic n) = keywordSafe $ jsIdent n +jsUserName (Field n) = "rf__" ++ jsIdent n +jsUserName Underscore = keywordSafe $ jsIdent "_" + jsName : Name -> String jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n -jsName (UN n) = keywordSafe $ jsIdent n +jsName (UN n) = jsUserName n jsName (MN n i) = jsIdent n ++ "_" ++ show i jsName (PV n d) = "pat__" ++ jsName n jsName (DN _ n) = jsName n -jsName (RF n) = "rf__" ++ jsIdent n jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y @@ -515,32 +519,33 @@ foreignDecl n ccs = do -- implementations for external primitive functions. jsPrim : {auto c : Ref ESs ESSt} -> Name -> List Doc -> Core Doc -jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ hcat ["({value:", v, "})"] -jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ hcat ["(", r, ".value)"] -jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ hcat ["(", r, ".value=", v, ")"] -jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ hcat ["(Array(", s, ").fill(", v, "))"] -jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ hcat ["(", x, "[", p, "])"] -jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ hcat ["(", x, "[", p, "]=", v, ")"] -jsPrim (NS _ (UN "void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" -jsPrim (NS _ (UN "prim__void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" -jsPrim (NS _ (UN "prim__codegen")) [] = do +jsPrim nm docs = case (dropAllNS nm, docs) of + (UN (Basic "prim__newIORef"), [_,v,_]) => pure $ hcat ["({value:", v, "})"] + (UN (Basic "prim__readIORef"), [_,r,_]) => pure $ hcat ["(", r, ".value)"] + (UN (Basic "prim__writeIORef"), [_,r,v,_]) => pure $ hcat ["(", r, ".value=", v, ")"] + (UN (Basic "prim__newArray"), [_,s,v,_]) => pure $ hcat ["(Array(", s, ").fill(", v, "))"] + (UN (Basic "prim__arrayGet"), [_,x,p,_]) => pure $ hcat ["(", x, "[", p, "])"] + (UN (Basic "prim__arraySet"), [_,x,p,v,_]) => pure $ hcat ["(", x, "[", p, "]=", v, ")"] + (UN (Basic "void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" + (UN (Basic "prim__void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" + (UN (Basic "prim__codegen"), []) => do (cg :: _) <- ccTypes <$> get ESs | _ => pure "\"javascript\"" pure . Text $ jsString cg -- fix #1839: Only support `prim__os` in Node backend but not in browsers -jsPrim (NS _ (UN "prim__os")) [] = do - tys <- ccTypes <$> get ESs - case searchForeign tys ["node"] of - Right _ => do - addToPreamble "prim__os" $ - "const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++ - "(require('os').platform()));" - pure $ Text $ esName "sysos" - Left _ => - throw $ InternalError $ "prim not implemented: prim__os" + (UN (Basic "prim__os"), []) => do + tys <- ccTypes <$> get ESs + case searchForeign tys ["node"] of + Right _ => do + addToPreamble "prim__os" $ + "const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++ + "(require('os').platform()));" + pure $ Text $ esName "sysos" + Left _ => + throw $ InternalError $ "prim not implemented: prim__os" -jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x) + _ => throw $ InternalError $ "prim not implemented: " ++ show nm -------------------------------------------------------------------------------- -- Codegen @@ -696,7 +701,7 @@ foreign _ = pure [] -- name of the toplevel tail call loop from the -- preamble. tailRec : Name -tailRec = UN "__tailRec" +tailRec = UN $ Basic "__tailRec" ||| Compiles the given `ClosedTerm` for the list of supported ||| backends to JS code. diff --git a/src/Compiler/Inline.idr b/src/Compiler/Inline.idr index fb56e3388..419d77228 100644 --- a/src/Compiler/Inline.idr +++ b/src/Compiler/Inline.idr @@ -151,7 +151,7 @@ mutual -- whether they're safe to inline, but until then this gives such a huge -- boost by removing unnecessary lambdas that we'll keep the special case. eval rec env stk (CRef fc n) - = case (n == NS primIONS (UN "io_bind"), stk) of + = case (n == NS primIONS (UN $ Basic "io_bind"), stk) of (True, act :: cont :: world :: stk) => do xn <- genName "act" sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world]) diff --git a/src/Compiler/Interpreter/VMCode.idr b/src/Compiler/Interpreter/VMCode.idr index b7f7f2566..468645ec0 100644 --- a/src/Compiler/Interpreter/VMCode.idr +++ b/src/Compiler/Interpreter/VMCode.idr @@ -120,7 +120,7 @@ callPrim stk fn args = case the (Either Object (Vect ar Constant)) $ traverse ge getConst o = Left o NS_UN : Namespace -> String -> Name -NS_UN ns un = NS ns (UN un) +NS_UN ns un = NS ns (UN $ Basic un) argError : Ref State InterpState => Stack -> Vect h Object -> Core a argError stk obj = interpError stk $ "Unexpected arguments: " ++ foldMap ((" " ++) . showType) obj diff --git a/src/Compiler/LambdaLift.idr b/src/Compiler/LambdaLift.idr index 4c36b7888..03b4383ad 100644 --- a/src/Compiler/LambdaLift.idr +++ b/src/Compiler/LambdaLift.idr @@ -148,7 +148,7 @@ genName where mkName : Name -> Int -> Name mkName (NS ns b) i = NS ns (mkName b i) - mkName (UN n) i = MN n i + mkName (UN n) i = MN (displayUserName n) i mkName (DN _ n) i = mkName n i mkName (CaseBlock outer inner) i = MN ("case block in " ++ outer ++ " (" ++ show inner ++ ")") i mkName (WithBlock outer inner) i = MN ("with block in " ++ outer ++ " (" ++ show inner ++ ")") i diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 5aabe32f0..f4fec9198 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -63,14 +63,19 @@ showcCleanString (c ::cs) = (showcCleanStringChar c) . showcCleanString cs cCleanString : String -> String cCleanString cs = showcCleanString (unpack cs) "" +export +cUserName : UserName -> String +cUserName (Basic n) = cCleanString n +cUserName (Field n) = "rec__" ++ cCleanString n +cUserName Underscore = cCleanString "_" + export cName : Name -> String cName (NS ns n) = cCleanString (showNSWithSep "_" ns) ++ "_" ++ cName n -cName (UN n) = cCleanString n +cName (UN n) = cUserName n cName (MN n i) = cCleanString n ++ "_" ++ cCleanString (show i) cName (PV n d) = "pat__" ++ cName n cName (DN _ n) = cName n -cName (RF n) = "rec__" ++ cCleanString n cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y) cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y) @@ -228,20 +233,20 @@ Show ExtPrim where ||| Match on a user given name to get the scheme primitive toPrim : Name -> ExtPrim toPrim pn@(NS _ n) - = cond [(n == UN "prim__newIORef", NewIORef), - (n == UN "prim__readIORef", ReadIORef), - (n == UN "prim__writeIORef", WriteIORef), - (n == UN "prim__newArray", NewArray), - (n == UN "prim__arrayGet", ArrayGet), - (n == UN "prim__arraySet", ArraySet), - (n == UN "prim__getField", GetField), - (n == UN "prim__setField", SetField), - (n == UN "void", VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated - (n == UN "prim__void", VoidElim), - (n == UN "prim__os", SysOS), - (n == UN "prim__codegen", SysCodegen), - (n == UN "prim__onCollect", OnCollect), - (n == UN "prim__onCollectAny", OnCollectAny) + = cond [(n == UN (Basic "prim__newIORef"), NewIORef), + (n == UN (Basic "prim__readIORef"), ReadIORef), + (n == UN (Basic "prim__writeIORef"), WriteIORef), + (n == UN (Basic "prim__newArray"), NewArray), + (n == UN (Basic "prim__arrayGet"), ArrayGet), + (n == UN (Basic "prim__arraySet"), ArraySet), + (n == UN (Basic "prim__getField"), GetField), + (n == UN (Basic "prim__setField"), SetField), + (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated + (n == UN (Basic "prim__void"), VoidElim), + (n == UN (Basic "prim__os"), SysOS), + (n == UN (Basic "prim__codegen"), SysCodegen), + (n == UN (Basic "prim__onCollect"), OnCollect), + (n == UN (Basic "prim__onCollectAny"), OnCollectAny) ] (Unknown pn) toPrim pn = assert_total $ idris_crash ("INTERNAL ERROR: Unknown primitive: " ++ cName pn) @@ -909,8 +914,8 @@ createCFunctions n (MkAForeign ccs fargs ret) = do else CLangC let isStandardFFI = Prelude.elem lang ["RefC", "C"] let fctName = if isStandardFFI - then UN fctForeignName - else UN $ lang ++ "_" ++ fctForeignName + then UN $ Basic $ fctForeignName + else UN $ Basic $ lang ++ "_" ++ fctForeignName if isStandardFFI then case extLibOpts of [lib, header] => addHeader header diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 1818805d8..7a9211ed0 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -128,7 +128,7 @@ chezString cs = strCons '"' (showChezString (unpack cs) "\"") mutual handleRet : String -> String -> String - handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN "") (Just 0) []) + handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN $ Basic "") (Just 0) []) handleRet _ op = mkWorld op getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp)) diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index c225aa9c3..86d069cec 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -28,15 +28,20 @@ schString s = concatMap okchar (unpack s) then cast c else "C-" ++ show (cast {to=Int} c) +export +schUserName : UserName -> String +schUserName (Basic n) = "u--" ++ schString n +schUserName (Field n) = "rf--" ++ schString n +schUserName Underscore = "u--_" + export schName : Name -> String -schName (NS ns (UN n)) = schString (showNSWithSep "-" ns) ++ "-" ++ schString n +schName (NS ns (UN (Basic n))) = schString (showNSWithSep "-" ns) ++ "-" ++ schString n +schName (UN n) = schUserName n schName (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schName n -schName (UN n) = "u--" ++ schString n schName (MN n i) = schString n ++ "-" ++ show i schName (PV n d) = "pat--" ++ schName n schName (DN _ n) = schName n -schName (RF n) = "rf--" ++ schString n schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y @@ -222,21 +227,21 @@ Show ExtPrim where ||| Match on a user given name to get the scheme primitive toPrim : Name -> ExtPrim toPrim pn@(NS _ n) - = cond [(n == UN "prim__newIORef", NewIORef), - (n == UN "prim__readIORef", ReadIORef), - (n == UN "prim__writeIORef", WriteIORef), - (n == UN "prim__newArray", NewArray), - (n == UN "prim__arrayGet", ArrayGet), - (n == UN "prim__arraySet", ArraySet), - (n == UN "prim__getField", GetField), - (n == UN "prim__setField", SetField), - (n == UN "void", VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated - (n == UN "prim__void", VoidElim), - (n == UN "prim__os", SysOS), - (n == UN "prim__codegen", SysCodegen), - (n == UN "prim__onCollect", OnCollect), - (n == UN "prim__onCollectAny", OnCollectAny), - (n == UN "prim__makeFuture", MakeFuture) + = cond [(n == UN (Basic "prim__newIORef"), NewIORef), + (n == UN (Basic "prim__readIORef"), ReadIORef), + (n == UN (Basic "prim__writeIORef"), WriteIORef), + (n == UN (Basic "prim__newArray"), NewArray), + (n == UN (Basic "prim__arrayGet"), ArrayGet), + (n == UN (Basic "prim__arraySet"), ArraySet), + (n == UN (Basic "prim__getField"), GetField), + (n == UN (Basic "prim__setField"), SetField), + (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated + (n == UN (Basic "prim__void"), VoidElim), + (n == UN (Basic "prim__os"), SysOS), + (n == UN (Basic "prim__codegen"), SysCodegen), + (n == UN (Basic "prim__onCollect"), OnCollect), + (n == UN (Basic "prim__onCollectAny"), OnCollectAny), + (n == UN (Basic "prim__makeFuture"), MakeFuture) ] (Unknown pn) toPrim pn = Unknown pn diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 937b7f9d2..b90017068 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -75,7 +75,7 @@ gambitString cs = strCons '"' (showGambitString (unpack cs) "\"") mutual handleRet : String -> String -> String - handleRet "void" op = op ++ " " ++ mkWorld (schConstructor gambitString (UN "") (Just 0) []) + handleRet "void" op = op ++ " " ++ mkWorld (schConstructor gambitString (UN $ Basic "") (Just 0) []) handleRet _ op = mkWorld op getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp)) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 4a52a7e3f..67f558109 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -173,7 +173,7 @@ rktToC CFChar op = "(char->integer " ++ op ++ ")" rktToC _ op = op handleRet : CFType -> String -> String -handleRet CFUnit op = op ++ " " ++ mkWorld (schConstructor racketString (UN "") (Just 0) []) +handleRet CFUnit op = op ++ " " ++ mkWorld (schConstructor racketString (UN $ Basic "") (Just 0) []) handleRet ret op = mkWorld (cToRkt ret op) cCall : {auto f : Ref Done (List String) } -> diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr index b23188dab..1166a4814 100644 --- a/src/Core/CaseBuilder.idr +++ b/src/Core/CaseBuilder.idr @@ -507,7 +507,7 @@ groupCons fc fn pvars cs -- The type of 'ConGroup' ensures that we refer to the arguments by -- the same name in each of the clauses addConG {vars'} {todo'} n tag pargs pats pid rhs [] - = do cty <- if n == UN "->" + = do cty <- if n == UN (Basic "->") then pure $ NBind fc (MN "_" 0) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NType fc))) $ (\d, a => pure $ NBind fc (MN "_" 1) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NErased fc False))) (\d, a => pure $ NType fc)) @@ -626,7 +626,7 @@ groupCons fc fn pvars cs then addConG n 0 pargs pats pid rhs acc else throw (CaseCompile cfc fn (NotFullyApplied n)) addGroup (PArrow _ _ s t) pprf pats pid rhs acc - = addConG (UN "->") 0 [s, t] pats pid rhs acc + = addConG (UN $ Basic "->") 0 [s, t] pats pid rhs acc -- Go inside the delay; we'll flag the case as needing to force its -- scrutinee (need to check in 'caseGroups below) addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc @@ -1101,8 +1101,8 @@ mkPat args orig (TDelay fc r ty p) mkPat args orig (PrimVal fc c) = pure $ if constTag c == 0 then PConst fc c - else PTyCon fc (UN (show c)) 0 [] -mkPat args orig (TType fc) = pure $ PTyCon fc (UN "Type") 0 [] + else PTyCon fc (UN (Basic $ show c)) 0 [] +mkPat args orig (TType fc) = pure $ PTyCon fc (UN $ Basic "Type") 0 [] mkPat args orig tm = do log "compile.casetree" 10 $ "Catchall: marking " ++ show tm ++ " as unmatchable" diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index 2ccac80ca..b542dde5e 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -265,7 +265,7 @@ elem n [] = False elem n (x :: xs) = n == x || elem n xs tryNext : Name -> Name -tryNext (UN n) = MN n 0 +tryNext (UN n) = MN (displayUserName n) 0 tryNext (MN n i) = MN n (1 + i) tryNext n = MN (nameRoot n) 0 diff --git a/src/Core/Context.idr b/src/Core/Context.idr index ac5530295..bdaf76bd1 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -22,6 +22,7 @@ import Data.Maybe import Data.Nat import Libraries.Data.NameMap import Libraries.Data.StringMap +import Libraries.Data.UserNameMap import Libraries.Text.Distance.Levenshtein import System @@ -73,7 +74,7 @@ initCtxt : Core Context initCtxt = initCtxtS initSize addPossible : Name -> Int -> - StringMap (List PossibleName) -> StringMap (List PossibleName) + UserNameMap (List PossibleName) -> UserNameMap (List PossibleName) addPossible n i ps = case userNameRoot n of Nothing => ps @@ -83,7 +84,7 @@ addPossible n i ps Just nis => insert nr (Direct n i :: nis) ps addAlias : Name -> Name -> Int -> - StringMap (List PossibleName) -> StringMap (List PossibleName) + UserNameMap (List PossibleName) -> UserNameMap (List PossibleName) addAlias alias full i ps = case userNameRoot alias of Nothing => ps @@ -819,12 +820,12 @@ getFieldNames ctxt recNS -- Find similar looking names in the context export getSimilarNames : {auto c : Ref Ctxt Defs} -> Name -> Core (List String) -getSimilarNames nm = case userNameRoot nm of +getSimilarNames nm = case show <$> userNameRoot nm of Nothing => pure [] Just str => if length str <= 1 then pure [] else let threshold : Nat := max 1 (assert_total (divNat (length str) 3)) test : Name -> IO (Maybe Nat) := \ nm => do - let (Just str') = userNameRoot nm + let (Just str') = show <$> userNameRoot nm | _ => pure Nothing dist <- Levenshtein.compute str str' pure (dist <$ guard (dist <= threshold)) @@ -1180,8 +1181,6 @@ visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss reducibleIn : Namespace -> Name -> Visibility -> Bool reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace reducibleIn nspace (NS ns (UN n)) Private = isParentOf ns nspace -reducibleIn nspace (NS ns (RF n)) Export = isParentOf ns nspace -reducibleIn nspace (NS ns (RF n)) Private = isParentOf ns nspace reducibleIn nspace n _ = True export @@ -1713,9 +1712,6 @@ inCurrentNS n@(MN _ _) inCurrentNS n@(DN _ _) = do defs <- get Ctxt pure (NS (currentNS defs) n) -inCurrentNS n@(RF _) - = do defs <- get Ctxt - pure (NS (currentNS defs) n) inCurrentNS n = pure n export diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index 55c1a3426..2bff99d4a 100644 --- a/src/Core/Context/Context.idr +++ b/src/Core/Context/Context.idr @@ -18,7 +18,7 @@ import Data.Nat import Libraries.Data.IntMap import Libraries.Data.IOArray import Libraries.Data.NameMap -import Libraries.Data.StringMap +import Libraries.Data.UserNameMap import Libraries.Utils.Binary public export @@ -357,8 +357,8 @@ record Context where nextEntry : Int -- Map from full name to its position in the context resolvedAs : NameMap Int - -- Map from strings to all the possible names in all namespaces - possibles : StringMap (List PossibleName) + -- Map from usernames to all the possible names in all namespaces + possibles : UserNameMap (List PossibleName) -- Reference to the actual content, indexed by Int content : Ref Arr (IOArray ContextEntry) -- Branching depth, in a backtracking elaborator. 0 is top level; at lower diff --git a/src/Core/Env.idr b/src/Core/Env.idr index c73a3c9b8..4e1c63d53 100644 --- a/src/Core/Env.idr +++ b/src/Core/Env.idr @@ -266,7 +266,7 @@ uniqifyEnv env = uenv [] env where next : Name -> Name next (MN n i) = MN n (i + 1) - next (UN n) = MN n 0 + next (UN n) = MN (displayUserName n) 0 next (NS ns n) = NS ns (next n) next n = MN (show n) 0 diff --git a/src/Core/Name.idr b/src/Core/Name.idr index a92543b60..cdbe69404 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -6,28 +6,44 @@ import Data.Maybe import Decidable.Equality import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter.Util +import Libraries.Utils.String import public Core.Name.Namespace %default total +||| A username has some structure +public export +data UserName : Type where + Basic : String -> UserName -- default name constructor e.g. map + Field : String -> UserName -- field accessor e.g. .fst + Underscore : UserName -- no name e.g. _ + +||| A smart constructor taking a string and parsing it as the appropriate +||| username +export +mkUserName : String -> UserName +mkUserName "_" = Underscore +mkUserName str with (strM str) + mkUserName _ | StrCons '.' n = Field n + mkUserName str | _ = Basic str + ||| Name helps us track a name's structure as well as its origin: ||| was it user-provided or machine-manufactured? For what reason? public export data Name : Type where NS : Namespace -> Name -> Name -- in a namespace - UN : String -> Name -- user defined name + UN : UserName -> Name -- user defined name MN : String -> Int -> Name -- machine generated name PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id DN : String -> Name -> Name -- a name and how to display it - RF : String -> Name -- record field name Nested : (Int, Int) -> Name -> Name -- nested function name CaseBlock : String -> Int -> Name -- case block nested in (resolved) name WithBlock : String -> Int -> Name -- with block nested in (resolved) name Resolved : Int -> Name -- resolved, index into context export -mkNamespacedName : Maybe Namespace -> String -> Name +mkNamespacedName : Maybe Namespace -> UserName -> Name mkNamespacedName Nothing nm = UN nm mkNamespacedName (Just ns) nm = NS ns (UN nm) @@ -55,19 +71,24 @@ asName old new (NS ns n) asName _ _ n = n export -userNameRoot : Name -> Maybe String +userNameRoot : Name -> Maybe UserName userNameRoot (NS _ n) = userNameRoot n userNameRoot (UN n) = Just n userNameRoot (DN _ n) = userNameRoot n -userNameRoot (RF n) = Just ("." ++ n) -- TMP HACK userNameRoot _ = Nothing export isUnderscoreName : Name -> Bool -isUnderscoreName (UN "_") = True +isUnderscoreName (UN Underscore) = True isUnderscoreName (MN "_" _) = True isUnderscoreName _ = False +export +isPatternVariable : UserName -> Bool +isPatternVariable (Basic nm) = lowerFirst nm +isPatternVariable (Field _) = False +isPatternVariable Underscore = True + export isUserName : Name -> Bool isUserName (PV _ _) = False @@ -85,7 +106,6 @@ isSourceName (UN _) = True isSourceName (MN _ _) = False isSourceName (PV n _) = isSourceName n isSourceName (DN _ n) = isSourceName n -isSourceName (RF _) = True isSourceName (Nested _ n) = isSourceName n isSourceName (CaseBlock _ _) = False isSourceName (WithBlock _ _) = False @@ -94,22 +114,32 @@ isSourceName (Resolved _) = False export isRF : Name -> Maybe (Namespace, String) isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n) -isRF (RF n) = Just (emptyNS, n) +isRF (UN (Field n)) = Just (emptyNS, n) isRF _ = Nothing export -isUN : Name -> Maybe String -isUN (UN str) = Just str +isUN : Name -> Maybe UserName +isUN (UN un) = Just un isUN _ = Nothing +export +isBasic : UserName -> Maybe String +isBasic (Basic str) = Just str +isBasic _ = Nothing + +export +displayUserName : UserName -> String +displayUserName (Basic n) = n +displayUserName (Field n) = n +displayUserName Underscore = "_" + export nameRoot : Name -> String nameRoot (NS _ n) = nameRoot n -nameRoot (UN n) = n +nameRoot (UN n) = displayUserName n nameRoot (MN n _) = n nameRoot (PV n _) = nameRoot n nameRoot (DN _ n) = nameRoot n -nameRoot (RF n) = n nameRoot (Nested _ inner) = nameRoot inner nameRoot (CaseBlock n _) = "$" ++ show n nameRoot (WithBlock n _) = "$" ++ show n @@ -118,11 +148,10 @@ nameRoot (Resolved i) = "$" ++ show i export displayName : Name -> (Maybe Namespace, String) displayName (NS ns n) = mapFst (pure . maybe ns (ns <.>)) $ displayName n -displayName (UN n) = (Nothing, n) +displayName (UN n) = (Nothing, displayUserName n) displayName (MN n _) = (Nothing, n) displayName (PV n _) = displayName n displayName (DN n _) = (Nothing, n) -displayName (RF n) = (Nothing, n) displayName (Nested _ n) = displayName n displayName (CaseBlock outer _) = (Nothing, "case block in " ++ show outer) displayName (WithBlock outer _) = (Nothing, "with block in " ++ show outer) @@ -153,58 +182,82 @@ mbApplyNS (Just ns) n = NS ns n export isUnsafeBuiltin : Name -> Bool isUnsafeBuiltin nm = case splitNS nm of - (ns, UN str) => (ns == builtinNS || ns == emptyNS) - && any {t = List} id - [ "assert_" `isPrefixOf` str - , str `elem` [ "prim__believe_me", "believe_me" - , "prim__crash", "idris_crash" - ] - ] + (ns, UN (Basic str)) => + (ns == builtinNS || ns == emptyNS) + && any {t = List} id + [ "assert_" `isPrefixOf` str + , str `elem` [ "prim__believe_me", "believe_me" + , "prim__crash", "idris_crash" + ] + ] _ => False +export +Show UserName where + show (Basic n) = n + show (Field n) = "." ++ n + show Underscore = "_" + export Show Name where - show (NS ns n@(RF _)) = show ns ++ ".(" ++ show n ++ ")" + show (NS ns n@(UN (Field _))) = show ns ++ ".(" ++ show n ++ ")" show (NS ns n) = show ns ++ "." ++ show n - show (UN x) = x + show (UN x) = show x show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}" show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}" show (DN str n) = str - show (RF n) = "." ++ n show (Nested (outer, idx) inner) = show outer ++ ":" ++ show idx ++ ":" ++ show inner show (CaseBlock outer i) = "case block in " ++ outer show (WithBlock outer i) = "with block in " ++ outer show (Resolved x) = "$resolved" ++ show x +export +[RawUN] Show UserName where + show (Basic n) = "Basic " ++ n + show (Field n) = "Field " ++ n + show Underscore = "Underscore" + export [Raw] Show Name where show (NS ns n) = "NS " ++ show ns ++ " (" ++ show n ++ ")" - show (UN x) = "UN " ++ x + show (UN x) = "UN (" ++ show @{RawUN} x ++ ")" show (MN x y) = "MN (" ++ show x ++ ") " ++ show y show (PV n d) = "PV (" ++ show n ++ ") " ++ show d show (DN str n) = "DN " ++ str ++ " (" ++ show n ++ ")" - show (RF n) = "RF " ++ n show (Nested ij n) = "Nested " ++ show ij ++ " (" ++ show n ++ ")" show (CaseBlock str i) = "CaseBlock " ++ str ++ " " ++ show i show (WithBlock str i) = "CaseBlock " ++ str ++ " " ++ show i show (Resolved i) = "Resolved " ++ show i +export +Pretty UserName where + pretty (Basic n) = pretty n + pretty (Field n) = "." <+> pretty n + pretty Underscore = "_" + export Pretty Name where - pretty (NS ns n@(RF _)) = pretty ns <+> dot <+> parens (pretty n) + pretty (NS ns n@(UN (Field _))) = pretty ns <+> dot <+> parens (pretty n) pretty (NS ns n) = pretty ns <+> dot <+> pretty n pretty (UN x) = pretty x pretty (MN x y) = braces (pretty x <+> colon <+> pretty y) pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d) pretty (DN str _) = pretty str - pretty (RF n) = "." <+> pretty n pretty (Nested (outer, idx) inner) = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer pretty (Resolved x) = pretty "$resolved" <+> pretty x +export +Eq UserName where + (==) (Basic x) (Basic y) = x == y + (==) (Field x) (Field y) = x == y + (==) Underscore Underscore = True + (==) _ _ = False + + export Eq Name where (==) (NS ns n) (NS ns' n') = n == n' && ns == ns' @@ -212,20 +265,30 @@ Eq Name where (==) (MN x y) (MN x' y') = y == y' && x == x' (==) (PV x y) (PV x' y') = x == x' && y == y' (==) (DN _ n) (DN _ n') = n == n' - (==) (RF n) (RF n') = n == n' (==) (Nested x y) (Nested x' y') = x == x' && y == y' (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x' (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x' (==) (Resolved x) (Resolved x') = x == x' (==) _ _ = False +usernameTag : UserName -> Int +usernameTag (Basic _) = 0 +usernameTag (Field _) = 2 +usernameTag Underscore = 3 + +export +Ord UserName where + compare (Basic x) (Basic y) = compare x y + compare (Field x) (Field y) = compare x y + compare Underscore Underscore = EQ + compare x y = compare (usernameTag x) (usernameTag y) + nameTag : Name -> Int nameTag (NS _ _) = 0 nameTag (UN _) = 1 nameTag (MN _ _) = 2 nameTag (PV _ _) = 3 nameTag (DN _ _) = 4 -nameTag (RF _) = 5 nameTag (Nested _ _) = 6 nameTag (CaseBlock _ _) = 7 nameTag (WithBlock _ _) = 8 @@ -252,7 +315,6 @@ Ord Name where GT => GT LT => LT compare (DN _ n) (DN _ n') = compare n n' - compare (RF n) (RF n') = compare n n' compare (Nested x y) (Nested x' y') = case compare y y' of EQ => compare x x' @@ -273,6 +335,18 @@ Ord Name where compare x y = compare (nameTag x) (nameTag y) +export +userNameEq : (x, y : UserName) -> Maybe (x = y) +userNameEq (Basic x) (Basic y) with (decEq x y) + userNameEq (Basic x) (Basic y) | Yes prf = Just (cong Basic prf) + userNameEq (Basic x) (Basic y) | No nprf = Nothing +userNameEq (Field x) (Field y) with (decEq x y) + userNameEq (Field x) (Field y) | Yes prf = Just (cong Field prf) + userNameEq (Field x) (Field y) | No nprf = Nothing +userNameEq Underscore Underscore = Just Refl +userNameEq _ _ = Nothing + + export nameEq : (x : Name) -> (y : Name) -> Maybe (x = y) nameEq (NS xs x) (NS ys y) with (decEq xs ys) @@ -280,9 +354,7 @@ nameEq (NS xs x) (NS ys y) with (decEq xs ys) nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl nameEq (NS xs x) (NS ys y) | (No contra) = Nothing -nameEq (UN x) (UN y) with (decEq x y) - nameEq (UN y) (UN y) | (Yes Refl) = Just Refl - nameEq (UN x) (UN y) | (No contra) = Nothing +nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y) nameEq (MN x t) (MN x' t') with (decEq x x') nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t') nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl @@ -298,9 +370,6 @@ nameEq (DN x t) (DN y t') with (decEq x y) nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing nameEq (DN x t) (DN y t') | (No p) = Nothing -nameEq (RF x) (RF y) with (decEq x y) - nameEq (RF y) (RF y) | (Yes Refl) = Just Refl - nameEq (RF x) (RF y) | (No contra) = Nothing nameEq (Nested x y) (Nested x' y') with (decEq x x') nameEq (Nested x y) (Nested x' y') | (No p) = Nothing nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y') diff --git a/src/Core/Normalise/Eval.idr b/src/Core/Normalise/Eval.idr index d226bf065..fc5bde8bd 100644 --- a/src/Core/Normalise/Eval.idr +++ b/src/Core/Normalise/Eval.idr @@ -137,7 +137,7 @@ parameters (defs : Defs, topopts : EvalOpts) = do tm' <- eval env locs tm [] case tm' of NDelay fc r _ arg => - eval env (arg :: locs) (Local {name = UN "fvar"} fc Nothing _ First) stk + eval env (arg :: locs) (Local {name = UN (Basic "fvar")} fc Nothing _ First) stk _ => pure (NForce fc r tm' stk) eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c eval env locs (Erased fc i) stk = pure $ NErased fc i @@ -186,7 +186,7 @@ parameters (defs : Defs, topopts : EvalOpts) = do tm' <- applyToStack env cont tm [] case tm' of NDelay fc r _ arg => - eval env [arg] (Local {name = UN "fvar"} fc Nothing _ First) stk + eval env [arg] (Local {name = UN (Basic "fvar")} fc Nothing _ First) stk _ => pure (NForce fc r tm' (args ++ stk)) applyToStack env cont nf@(NPrimVal fc _) _ = pure nf applyToStack env cont nf@(NErased fc _) _ = pure nf @@ -340,16 +340,16 @@ parameters (defs : Defs, topopts : EvalOpts) -- Primitive type matching, in typecase tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag args sc) = case args of -- can't just test for it in the `if` for typing reasons - [] => if UN (show c) == nm + [] => if UN (Basic $ show c) == nm then evalTree env loc opts fc stk sc else pure NoMatch _ => pure NoMatch -- Type of type matching, in typecase - tryAlt env loc opts fc stk (NType _) (ConCase (UN "Type") tag [] sc) + tryAlt env loc opts fc stk (NType _) (ConCase (UN (Basic "Type")) tag [] sc) = evalTree env loc opts fc stk sc -- Arrow matching, in typecase tryAlt {more} - env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN "->") tag [s,t] sc) + env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN (Basic "->")) tag [s,t] sc) = evalConAlt {more} env loc opts fc stk [s,t] [aty, MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)] diff --git a/src/Core/Primitives.idr b/src/Core/Primitives.idr index 3b6dce05e..244752a82 100644 --- a/src/Core/Primitives.idr +++ b/src/Core/Primitives.idr @@ -603,17 +603,21 @@ cmpTy t = constTy t t IntType doubleTy : ClosedTerm doubleTy = predTy DoubleType DoubleType +pi : (x : String) -> RigCount -> PiInfo (Term xs) -> Term xs -> + Term (UN (Basic x) :: xs) -> Term xs +pi x rig plic ty sc = Bind emptyFC (UN (Basic x)) (Pi emptyFC rig plic ty) sc + believeMeTy : ClosedTerm believeMeTy - = Bind emptyFC (UN "a") (Pi emptyFC erased Explicit (TType emptyFC)) $ - Bind emptyFC (UN "b") (Pi emptyFC erased Explicit (TType emptyFC)) $ - Bind emptyFC (UN "x") (Pi emptyFC top Explicit (Local emptyFC Nothing _ (Later First))) $ + = pi "a" erased Explicit (TType emptyFC) $ + pi "b" erased Explicit (TType emptyFC) $ + pi "x" top Explicit (Local emptyFC Nothing _ (Later First)) $ Local emptyFC Nothing _ (Later First) crashTy : ClosedTerm crashTy - = Bind emptyFC (UN "a") (Pi emptyFC erased Explicit (TType emptyFC)) $ - Bind emptyFC (UN "msg") (Pi emptyFC top Explicit (PrimVal emptyFC StringType)) $ + = pi "a" erased Explicit (TType emptyFC) $ + pi "msg" top Explicit (PrimVal emptyFC StringType) $ Local emptyFC Nothing _ (Later First) castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars) @@ -682,7 +686,7 @@ getOp BelieveMe = believeMe getOp _ = const Nothing prim : String -> Name -prim str = UN $ "prim__" ++ str +prim str = UN $ Basic $ "prim__" ++ str export opName : {0 arity : Nat} -> PrimFn arity -> Name diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index 2f8932137..024814519 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -41,31 +41,31 @@ appCon fc defs n args export preludetypes : String -> Name -preludetypes n = NS typesNS (UN n) +preludetypes n = NS typesNS (UN $ Basic n) export basics : String -> Name -basics n = NS basicsNS (UN n) +basics n = NS basicsNS (UN $ Basic n) export builtin : String -> Name -builtin n = NS builtinNS (UN n) +builtin n = NS builtinNS (UN $ Basic n) export primio : String -> Name -primio n = NS primIONS (UN n) +primio n = NS primIONS (UN $ Basic n) export reflection : String -> Name -reflection n = NS reflectionNS (UN n) +reflection n = NS reflectionNS (UN $ Basic n) export reflectiontt : String -> Name -reflectiontt n = NS reflectionTTNS (UN n) +reflectiontt n = NS reflectionTTNS (UN $ Basic n) export reflectionttimp : String -> Name -reflectionttimp n = NS reflectionTTImpNS (UN n) +reflectionttimp n = NS reflectionTTImpNS (UN $ Basic n) export cantReify : NF vars -> String -> Core a @@ -133,9 +133,9 @@ Reflect Double where export Reify Bool where reify defs val@(NDCon _ n _ _ _) - = case !(full (gamma defs) n) of - NS _ (UN "True") => pure True - NS _ (UN "False") => pure False + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "True") => pure True + UN (Basic "False") => pure False _ => cantReify val "Bool" reify defs val = cantReify val "Bool" @@ -147,9 +147,9 @@ Reflect Bool where export Reify Nat where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "Z"), _) => pure Z - (NS _ (UN "S"), [(_, k)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Z"), _) => pure Z + (UN (Basic "S"), [(_, k)]) => do k' <- reify defs !(evalClosure defs k) pure (S k') _ => cantReify val "Nat" @@ -165,9 +165,9 @@ Reflect Nat where export Reify a => Reify (List a) where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "Nil"), _) => pure [] - (NS _ (UN "::"), [_, (_, x), (_, xs)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Nil"), _) => pure [] + (UN (Basic "::"), [_, (_, x), (_, xs)]) => do x' <- reify defs !(evalClosure defs x) xs' <- reify defs !(evalClosure defs xs) pure (x' :: xs') @@ -185,8 +185,8 @@ Reflect a => Reflect (List a) where export Reify a => Reify (List1 a) where reify defs val@(NDCon _ n _ _ [_, (_, x), (_, xs)]) - = case !(full (gamma defs) n) of - NS _ (UN ":::") + = case dropAllNS !(full (gamma defs) n) of + UN (Basic ":::") => do x' <- reify defs !(evalClosure defs x) xs' <- reify defs !(evalClosure defs xs) pure (x' ::: xs') @@ -198,14 +198,15 @@ Reflect a => Reflect (List1 a) where reflect fc defs lhs env xxs = do x' <- reflect fc defs lhs env (head xxs) xs' <- reflect fc defs lhs env (tail xxs) - appCon fc defs (NS (mkNamespace "Data.List1") (UN ":::")) [Erased fc False, x', xs'] + appCon fc defs (NS (mkNamespace "Data.List1") + (UN $ Basic ":::")) [Erased fc False, x', xs'] export Reify a => Reify (Maybe a) where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "Nothing"), _) => pure Nothing - (NS _ (UN "Just"), [_, (_, x)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Nothing"), _) => pure Nothing + (UN (Basic "Just"), [_, (_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (Just x') _ => cantReify val "Maybe" @@ -221,8 +222,8 @@ Reflect a => Reflect (Maybe a) where export (Reify a, Reify b) => Reify (a, b) where reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)]) - = case (!(full (gamma defs) n)) of - NS _ (UN "MkPair") + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "MkPair") => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) pure (x', y') @@ -239,8 +240,8 @@ export export Reify Namespace where reify defs val@(NDCon _ n _ _ [(_, ns)]) - = case (!(full (gamma defs) n)) of - NS _ (UN "MkNS") + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "MkNS") => do ns' <- reify defs !(evalClosure defs ns) pure (unsafeFoldNamespace ns') _ => cantReify val "Namespace" @@ -255,8 +256,8 @@ Reflect Namespace where export Reify ModuleIdent where reify defs val@(NDCon _ n _ _ [(_, ns)]) - = case (!(full (gamma defs) n)) of - NS _ (UN "MkMI") + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "MkMI") => do ns' <- reify defs !(evalClosure defs ns) pure (unsafeFoldModuleIdent ns') _ => cantReify val "ModuleIdent" @@ -268,37 +269,62 @@ Reflect ModuleIdent where = do ns' <- reflect fc defs lhs env (unsafeUnfoldModuleIdent ns) appCon fc defs (reflectiontt "MkMI") [ns'] +export +Reify UserName where + reify defs val@(NDCon _ n _ _ args) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Basic"), [(_, str)]) + => do str' <- reify defs !(evalClosure defs str) + pure (Basic str') + (UN (Basic "Field"), [(_, str)]) + => do str' <- reify defs !(evalClosure defs str) + pure (Field str') + (UN (Basic "Underscore"), []) + => pure Underscore + (NS _ (UN _), _) + => cantReify val "Name, reifying it is unimplemented or intentionally internal" + _ => cantReify val "Name, the name was not found in context" + reify defs val = cantReify val "Name, value is not an NDCon interally" + +export +Reflect UserName where + reflect fc defs lhs env (Basic x) + = do x' <- reflect fc defs lhs env x + appCon fc defs (reflectiontt "Basic") [x'] + reflect fc defs lhs env (Field x) + = do x' <- reflect fc defs lhs env x + appCon fc defs (reflectiontt "Field") [x'] + reflect fc defs lhs env Underscore + = do appCon fc defs (reflectiontt "Underscore") [] + export Reify Name where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "UN"), [(_, str)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "UN"), [(_, str)]) => do str' <- reify defs !(evalClosure defs str) pure (UN str') - (NS _ (UN "MN"), [(_, str), (_, i)]) + (UN (Basic "MN"), [(_, str), (_, i)]) => do str' <- reify defs !(evalClosure defs str) i' <- reify defs !(evalClosure defs i) pure (MN str' i') - (NS _ (UN "NS"), [(_, ns), (_, n)]) + (UN (Basic "NS"), [(_, ns), (_, n)]) => do ns' <- reify defs !(evalClosure defs ns) n' <- reify defs !(evalClosure defs n) pure (NS ns' n') - (NS _ (UN "DN"), [(_, str), (_, n)]) + (UN (Basic "DN"), [(_, str), (_, n)]) => do str' <- reify defs !(evalClosure defs str) n' <- reify defs !(evalClosure defs n) pure (DN str' n') - (NS _ (UN "RF"), [(_, str)]) - => do str' <- reify defs !(evalClosure defs str) - pure (RF str') - (NS _ (UN "Nested"), [(_, ix), (_, n)]) + (UN (Basic "Nested"), [(_, ix), (_, n)]) => do ix' <- reify defs !(evalClosure defs ix) n' <- reify defs !(evalClosure defs n) pure (Nested ix' n') - (NS _ (UN "CaseBlock"), [(_, outer), (_, i)]) + (UN (Basic "CaseBlock"), [(_, outer), (_, i)]) => do outer' <- reify defs !(evalClosure defs outer) i' <- reify defs !(evalClosure defs i) pure (CaseBlock outer' i') - (NS _ (UN "WithBlock"), [(_, outer), (_, i)]) + (UN (Basic "WithBlock"), [(_, outer), (_, i)]) => do outer' <- reify defs !(evalClosure defs outer) i' <- reify defs !(evalClosure defs i) pure (WithBlock outer' i') @@ -324,9 +350,6 @@ Reflect Name where = do str' <- reflect fc defs lhs env str n' <- reflect fc defs lhs env n appCon fc defs (reflectiontt "DN") [str', n'] - reflect fc defs lhs env (RF x) - = do x' <- reflect fc defs lhs env x - appCon fc defs (reflectiontt "RF") [x'] reflect fc defs lhs env (Nested ix n) = do ix' <- reflect fc defs lhs env ix n' <- reflect fc defs lhs env n @@ -350,14 +373,14 @@ Reflect Name where export Reify NameType where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "Bound"), _) => pure Bound - (NS _ (UN "Func"), _) => pure Func - (NS _ (UN "DataCon"), [(_, t), (_, i)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Bound"), _) => pure Bound + (UN (Basic "Func"), _) => pure Func + (UN (Basic "DataCon"), [(_, t), (_, i)]) => do t' <- reify defs !(evalClosure defs t) i' <- reify defs !(evalClosure defs i) pure (DataCon t' i') - (NS _ (UN "TyCon"), [(_, t),(_, i)]) + (UN (Basic "TyCon"), [(_, t),(_, i)]) => do t' <- reify defs !(evalClosure defs t) i' <- reify defs !(evalClosure defs i) pure (TyCon t' i') @@ -380,75 +403,75 @@ Reflect NameType where export Reify Constant where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "I"), [(_, x)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "I"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (I x') - (NS _ (UN "I8"), [(_, x)]) + (UN (Basic "I8"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (I8 x') - (NS _ (UN "I16"), [(_, x)]) + (UN (Basic "I16"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (I16 x') - (NS _ (UN "I32"), [(_, x)]) + (UN (Basic "I32"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (I32 x') - (NS _ (UN "I64"), [(_, x)]) + (UN (Basic "I64"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (I64 x') - (NS _ (UN "BI"), [(_, x)]) + (UN (Basic "BI"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (BI x') - (NS _ (UN "B8"), [(_, x)]) + (UN (Basic "B8"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (B8 x') - (NS _ (UN "B16"), [(_, x)]) + (UN (Basic "B16"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (B16 x') - (NS _ (UN "B32"), [(_, x)]) + (UN (Basic "B32"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (B32 x') - (NS _ (UN "B64"), [(_, x)]) + (UN (Basic "B64"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (B64 x') - (NS _ (UN "Str"), [(_, x)]) + (UN (Basic "Str"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (Str x') - (NS _ (UN "Ch"), [(_, x)]) + (UN (Basic "Ch"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (Ch x') - (NS _ (UN "Db"), [(_, x)]) + (UN (Basic "Db"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (Db x') - (NS _ (UN "WorldVal"), []) + (UN (Basic "WorldVal"), []) => pure WorldVal - (NS _ (UN "IntType"), []) + (UN (Basic "IntType"), []) => pure IntType - (NS _ (UN "Int8Type"), []) + (UN (Basic "Int8Type"), []) => pure Int8Type - (NS _ (UN "Int16Type"), []) + (UN (Basic "Int16Type"), []) => pure Int16Type - (NS _ (UN "Int32Type"), []) + (UN (Basic "Int32Type"), []) => pure Int32Type - (NS _ (UN "Int64Type"), []) + (UN (Basic "Int64Type"), []) => pure Int64Type - (NS _ (UN "IntegerType"), []) + (UN (Basic "IntegerType"), []) => pure IntegerType - (NS _ (UN "Bits8Type"), []) + (UN (Basic "Bits8Type"), []) => pure Bits8Type - (NS _ (UN "Bits16Type"), []) + (UN (Basic "Bits16Type"), []) => pure Bits16Type - (NS _ (UN "Bits32Type"), []) + (UN (Basic "Bits32Type"), []) => pure Bits32Type - (NS _ (UN "Bits64Type"), []) + (UN (Basic "Bits64Type"), []) => pure Bits64Type - (NS _ (UN "StringType"), []) + (UN (Basic "StringType"), []) => pure StringType - (NS _ (UN "CharType"), []) + (UN (Basic "CharType"), []) => pure CharType - (NS _ (UN "DoubleType"), []) + (UN (Basic "DoubleType"), []) => pure DoubleType - (NS _ (UN "WorldType"), []) + (UN (Basic "WorldType"), []) => pure WorldType _ => cantReify val "Constant" reify defs val = cantReify val "Constant" @@ -528,10 +551,10 @@ Reflect Constant where export Reify Visibility where reify defs val@(NDCon _ n _ _ _) - = case !(full (gamma defs) n) of - NS _ (UN "Private") => pure Private - NS _ (UN "Export") => pure Export - NS _ (UN "Public") => pure Public + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "Private") => pure Private + UN (Basic "Export") => pure Export + UN (Basic "Public") => pure Public _ => cantReify val "Visibility" reify defs val = cantReify val "Visibility" @@ -544,10 +567,10 @@ Reflect Visibility where export Reify TotalReq where reify defs val@(NDCon _ n _ _ _) - = case !(full (gamma defs) n) of - NS _ (UN "Total") => pure Total - NS _ (UN "CoveringOnly") => pure CoveringOnly - NS _ (UN "PartialOK") => pure PartialOK + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "Total") => pure Total + UN (Basic "CoveringOnly") => pure CoveringOnly + UN (Basic "PartialOK") => pure PartialOK _ => cantReify val "TotalReq" reify defs val = cantReify val "TotalReq" @@ -560,10 +583,10 @@ Reflect TotalReq where export Reify RigCount where reify defs val@(NDCon _ n _ _ _) - = case !(full (gamma defs) n) of - NS _ (UN "M0") => pure erased - NS _ (UN "M1") => pure linear - NS _ (UN "MW") => pure top + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "M0") => pure erased + UN (Basic "M1") => pure linear + UN (Basic "MW") => pure top _ => cantReify val "Count" reify defs val = cantReify val "Count" @@ -578,11 +601,11 @@ Reflect RigCount where export Reify t => Reify (PiInfo t) where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "ImplicitArg"), _) => pure Implicit - (NS _ (UN "ExplicitArg"), _) => pure Explicit - (NS _ (UN "AutoImplicit"), _) => pure AutoImplicit - (NS _ (UN "DefImplicit"), [_, (_, t)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "ImplicitArg"), _) => pure Implicit + (UN (Basic "ExplicitArg"), _) => pure Explicit + (UN (Basic "AutoImplicit"), _) => pure AutoImplicit + (UN (Basic "DefImplicit"), [_, (_, t)]) => do t' <- reify defs !(evalClosure defs t) pure (DefImplicit t') _ => cantReify val "PiInfo" @@ -603,10 +626,10 @@ Reflect t => Reflect (PiInfo t) where export Reify LazyReason where reify defs val@(NDCon _ n _ _ _) - = case !(full (gamma defs) n) of - NS _ (UN "LInf") => pure LInf - NS _ (UN "LLazy") => pure LLazy - NS _ (UN "LUnknown") => pure LUnknown + = case dropAllNS !(full (gamma defs) n) of + UN (Basic "LInf") => pure LInf + UN (Basic "LLazy") => pure LLazy + UN (Basic "LUnknown") => pure LUnknown _ => cantReify val "LazyReason" reify defs val = cantReify val "LazyReason" @@ -619,8 +642,8 @@ Reflect LazyReason where export Reify VirtualIdent where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "Interactive"), []) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Interactive"), []) => pure Interactive _ => cantReify val "VirtualIdent" reify defs val = cantReify val "VirtualIdent" @@ -637,12 +660,12 @@ Reflect BuiltinType where export Reify BuiltinType where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "BuiltinNatural"), []) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "BuiltinNatural"), []) => pure BuiltinNatural - (NS _ (UN "NaturalToInteger"), []) + (UN (Basic "NaturalToInteger"), []) => pure NaturalToInteger - (NS _ (UN "IntegerToNatural"), []) + (UN (Basic "IntegerToNatural"), []) => pure IntegerToNatural _ => cantReify val "BuiltinType" reify defs val = cantReify val "BuiltinType" @@ -655,14 +678,14 @@ Reflect VirtualIdent where export Reify OriginDesc where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "PhysicalIdrSrc"), [(_, ident)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "PhysicalIdrSrc"), [(_, ident)]) => do ident' <- reify defs !(evalClosure defs ident) pure (PhysicalIdrSrc ident') - (NS _ (UN "PhysicalPkgSrc"), [(_, fname)]) + (UN (Basic "PhysicalPkgSrc"), [(_, fname)]) => do fname' <- reify defs !(evalClosure defs fname) pure (PhysicalPkgSrc fname') - (NS _ (UN "Virtual"), [(_, ident)]) + (UN (Basic "Virtual"), [(_, ident)]) => do ident' <- reify defs !(evalClosure defs ident) pure (Virtual ident') _ => cantReify val "OriginDesc" @@ -683,13 +706,13 @@ Reflect OriginDesc where export Reify FC where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "MkFC"), [(_, fn), (_, start), (_, end)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "MkFC"), [(_, fn), (_, start), (_, end)]) => do fn' <- reify defs !(evalClosure defs fn) start' <- reify defs !(evalClosure defs start) end' <- reify defs !(evalClosure defs end) pure (MkFC fn' start' end') - (NS _ (UN "EmptyFC"), _) => pure EmptyFC + (UN (Basic "EmptyFC"), _) => pure EmptyFC _ => cantReify val "FC" reify defs val = cantReify val "FC" diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 77f9117fb..d964d755c 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -78,7 +78,7 @@ data Constant export isConstantType : Name -> Maybe Constant -isConstantType (UN n) = case n of +isConstantType (UN (Basic n)) = case n of "Int" => Just IntType "Int8" => Just Int8Type "Int16" => Just Int16Type diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 53355994a..e9b544977 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -73,17 +73,20 @@ TTC FC where export TTC Name where + -- for efficiency reasons we do not encode UserName separately + -- hence the nested pattern matches on UN (Basic/Hole/Field) toBuf b (NS xs x) = do tag 0; toBuf b xs; toBuf b x - toBuf b (UN x) = do tag 1; toBuf b x + toBuf b (UN (Basic x)) = do tag 1; toBuf b x toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y - toBuf b (RF x) = do tag 5; toBuf b x + toBuf b (UN (Field x)) = do tag 5; toBuf b x toBuf b (Nested x y) = do tag 6; toBuf b x; toBuf b y toBuf b (CaseBlock x y) = do tag 7; toBuf b x; toBuf b y toBuf b (WithBlock x y) = do tag 8; toBuf b x; toBuf b y toBuf b (Resolved x) = throw (InternalError ("Can't write resolved name " ++ show x)) + toBuf b (UN Underscore) = tag 9 fromBuf b = case !getTag of @@ -91,7 +94,7 @@ TTC Name where x <- fromBuf b pure (NS xs x) 1 => do x <- fromBuf b - pure (UN x) + pure (UN $ Basic x) 2 => do x <- fromBuf b y <- fromBuf b pure (MN x y) @@ -102,7 +105,7 @@ TTC Name where y <- fromBuf b pure (DN x y) 5 => do x <- fromBuf b - pure (RF x) + pure (UN $ Field x) 6 => do x <- fromBuf b y <- fromBuf b pure (Nested x y) @@ -112,6 +115,7 @@ TTC Name where 8 => do x <- fromBuf b y <- fromBuf b pure (WithBlock x y) + 9 => pure (UN Underscore) _ => corrupt "Name" export diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index d29e348ca..803928e6f 100644 --- a/src/Core/Termination.idr +++ b/src/Core/Termination.idr @@ -385,8 +385,8 @@ mutual | Nothing => undefinedName fc fn_in let fn = fullname gdef log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn) - aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller")) - cond [(fn == NS builtinNS (UN "assert_total"), pure []) + aSmaller <- resolved (gamma defs) (NS builtinNS (UN $ Basic "assert_smaller")) + cond [(fn == NS builtinNS (UN $ Basic "assert_total"), pure []) ,(caseFn fn, do scs1 <- traverse (findSC defs env g pats) args mps <- getCasePats defs fn pats args diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 53be6d340..884990ddd 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -166,9 +166,8 @@ export genMVName : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> Name -> Core Name -genMVName (UN str) = genName str +genMVName (UN str) = genName (displayUserName str) genMVName (MN str _) = genName str -genMVName (RF str) = genName str genMVName n = do ust <- get UST put UST (record { nextName $= (+1) } ust) diff --git a/src/Core/Value.idr b/src/Core/Value.idr index 8ba5aaa61..20bbcc129 100644 --- a/src/Core/Value.idr +++ b/src/Core/Value.idr @@ -105,7 +105,7 @@ mutual export ntCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars -ntCon fc (UN "Type") tag Z [] = NType fc +ntCon fc (UN (Basic "Type")) tag Z [] = NType fc ntCon fc n tag Z [] = case isConstantType n of Just c => NPrimVal fc c Nothing => NTCon fc n tag Z [] diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 91b64ee81..f5bf2b00d 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -35,7 +35,6 @@ import TTImp.Utils import Libraries.Data.IMaybe import Libraries.Utils.Shunting -import Libraries.Utils.String import Control.Monad.State import Data.Maybe @@ -150,12 +149,12 @@ addNS _ n = n bindFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp bindFun fc ns ma f = let fc = virtualiseFC fc in - IApp fc (IApp fc (IVar fc (addNS ns $ UN ">>=")) ma) f + IApp fc (IApp fc (IVar fc (addNS ns $ UN $ Basic ">>=")) ma) f seqFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp seqFun fc ns ma mb = let fc = virtualiseFC fc in - IApp fc (IApp fc (IVar fc (addNS ns (UN ">>"))) ma) mb + IApp fc (IApp fc (IVar fc (addNS ns (UN $ Basic ">>"))) ma) mb bindBangs : List (Name, FC, RawImp) -> Maybe Namespace -> RawImp -> RawImp bindBangs [] ns tm = tm @@ -169,24 +168,24 @@ idiomise fc (IAlternative afc u alts) = IAlternative afc (mapAltType (idiomise afc) u) (idiomise afc <$> alts) idiomise fc (IApp afc f a) = let fc = virtualiseFC fc in - IApp fc (IApp fc (IVar fc (UN "<*>")) + IApp fc (IApp fc (IVar fc (UN $ Basic "<*>")) (idiomise afc f)) a idiomise fc fn = let fc = virtualiseFC fc in - IApp fc (IVar fc (UN "pure")) fn + IApp fc (IVar fc (UN $ Basic "pure")) fn pairname : Name -pairname = NS builtinNS (UN "Pair") +pairname = NS builtinNS (UN $ Basic "Pair") mkpairname : Name -mkpairname = NS builtinNS (UN "MkPair") +mkpairname = NS builtinNS (UN $ Basic "MkPair") dpairname : Name -dpairname = NS dpairNS (UN "DPair") +dpairname = NS dpairNS (UN $ Basic "DPair") mkdpairname : Name -mkdpairname = NS dpairNS (UN "MkDPair") +mkdpairname = NS dpairNS (UN $ Basic "MkDPair") data Bang : Type where @@ -204,7 +203,7 @@ mutual mn !(desugarB side ps argTy) !(desugarB side ps' retTy) desugarB side ps (PLam fc rig p pat@(PRef prefFC n@(UN nm)) argTy scope) - = if lowerFirst nm || nm == "_" + = if isPatternVariable nm then do whenJust (isConcreteFC prefFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)] pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p) @@ -270,8 +269,8 @@ mutual = do l' <- desugarB side ps l r' <- desugarB side ps r pure $ IAlternative fc FirstSuccess - [apply (IVar fc (UN "===")) [l', r'], - apply (IVar fc (UN "~=~")) [l', r']] + [apply (IVar fc (UN $ Basic "===")) [l', r'], + apply (IVar fc (UN $ Basic "~=~")) [l', r']] desugarB side ps (PBracketed fc e) = desugarB side ps e desugarB side ps (POp fc opFC op l r) = do ts <- toTokList (POp fc opFC op l r) @@ -330,7 +329,7 @@ mutual desugarB side ps (PHole fc br holename) = do when br $ do syn <- get Syn - put Syn (record { bracketholes $= ((UN holename) ::) } syn) + put Syn (record { bracketholes $= ((UN (Basic holename)) ::) } syn) pure $ IHole fc holename desugarB side ps (PType fc) = pure $ IType fc desugarB side ps (PAs fc nameFC vname pattern) @@ -405,37 +404,37 @@ mutual desugarB side ps (PDPair fc opFC l ty r) = throw (GenericMsg fc "Invalid dependent pair type") desugarB side ps (PUnit fc) - = pure $ IAlternative fc (UniqueDefault (IVar fc (UN "MkUnit"))) - [IVar fc (UN "Unit"), - IVar fc (UN "MkUnit")] + = pure $ IAlternative fc (UniqueDefault (IVar fc (UN $ Basic "MkUnit"))) + [IVar fc (UN $ Basic "Unit"), + IVar fc (UN $ Basic "MkUnit")] desugarB side ps (PIfThenElse fc x t e) = let fc = virtualiseFC fc in - pure $ ICase fc !(desugarB side ps x) (IVar fc (UN "Bool")) - [PatClause fc (IVar fc (UN "True")) !(desugar side ps t), - PatClause fc (IVar fc (UN "False")) !(desugar side ps e)] + pure $ ICase fc !(desugarB side ps x) (IVar fc (UN $ Basic "Bool")) + [PatClause fc (IVar fc (UN $ Basic "True")) !(desugar side ps t), + PatClause fc (IVar fc (UN $ Basic "False")) !(desugar side ps e)] desugarB side ps (PComprehension fc ret conds) = do let ns = mbNamespace !(get Bang) desugarB side ps (PDoBlock fc ns (map (guard ns) conds ++ [toPure ns ret])) where guard : Maybe Namespace -> PDo -> PDo guard ns (DoExp fc tm) - = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN "guard")) tm) + = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN $ Basic "guard")) tm) guard ns d = d toPure : Maybe Namespace -> PTerm -> PDo - toPure ns tm = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN "pure")) tm) + toPure ns tm = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN $ Basic "pure")) tm) desugarB side ps (PRewrite fc rule tm) = pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm) desugarB side ps (PRange fc start next end) = let fc = virtualiseFC fc in desugarB side ps $ case next of - Nothing => papply fc (PRef fc (UN "rangeFromTo")) [start,end] - Just n => papply fc (PRef fc (UN "rangeFromThenTo")) [start, n, end] + Nothing => papply fc (PRef fc (UN $ Basic "rangeFromTo")) [start,end] + Just n => papply fc (PRef fc (UN $ Basic "rangeFromThenTo")) [start, n, end] desugarB side ps (PRangeStream fc start next) = let fc = virtualiseFC fc in desugarB side ps $ case next of - Nothing => papply fc (PRef fc (UN "rangeFrom")) [start] - Just n => papply fc (PRef fc (UN "rangeFromThen")) [start, n] + Nothing => papply fc (PRef fc (UN $ Basic "rangeFrom")) [start] + Just n => papply fc (PRef fc (UN $ Basic "rangeFromThen")) [start, n] desugarB side ps (PUnifyLog fc lvl tm) = pure $ IUnifyLog fc lvl !(desugarB side ps tm) desugarB side ps (PPostfixApp fc rec projs) @@ -468,9 +467,9 @@ mutual {auto m : Ref MD Metadata} -> Side -> List Name -> (nilFC : FC) -> List (FC, PTerm) -> Core RawImp - expandList side ps nilFC [] = pure (IVar nilFC (UN "Nil")) + expandList side ps nilFC [] = pure (IVar nilFC (UN $ Basic "Nil")) expandList side ps nilFC ((consFC, x) :: xs) - = pure $ apply (IVar consFC (UN "::")) + = pure $ apply (IVar consFC (UN $ Basic "::")) [!(desugarB side ps x), !(expandList side ps nilFC xs)] expandSnocList @@ -480,9 +479,9 @@ mutual {auto u : Ref UST UState} -> {auto m : Ref MD Metadata} -> Side -> List Name -> (nilFC : FC) -> List (FC, PTerm) -> Core RawImp - expandSnocList side ps nilFC [] = pure (IVar nilFC (UN "Lin")) + expandSnocList side ps nilFC [] = pure (IVar nilFC (UN $ Basic "Lin")) expandSnocList side ps nilFC ((consFC, x) :: xs) - = pure $ apply (IVar consFC (UN ":<")) + = pure $ apply (IVar consFC (UN $ Basic ":<")) [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)] addFromString : {auto c : Ref Ctxt Defs} -> @@ -526,7 +525,7 @@ mutual concatStr a b = let aFC = virtualiseFC (getFC a) bFC = virtualiseFC (getFC b) - in IApp aFC (IApp bFC (IVar bFC (UN "++")) a) b + in IApp aFC (IApp bFC (IVar bFC (UN $ Basic "++")) a) b trimMultiline : FC -> Nat -> List (List PStr) -> Core (List PStr) trimMultiline fc indent lines @@ -647,13 +646,13 @@ mutual {auto u : Ref UST UState} -> {auto m : Ref MD Metadata} -> Side -> List Name -> Tree OpStr PTerm -> Core RawImp - desugarTree side ps (Infix loc eqFC (UN "=") l r) -- special case since '=' is special syntax + desugarTree side ps (Infix loc eqFC (UN $ Basic "=") l r) -- special case since '=' is special syntax = do l' <- desugarTree side ps l r' <- desugarTree side ps r pure (IAlternative loc FirstSuccess - [apply (IVar eqFC (UN "===")) [l', r'], - apply (IVar eqFC (UN "~=~")) [l', r']]) - desugarTree side ps (Infix loc _ (UN "$") l r) -- special case since '$' is special syntax + [apply (IVar eqFC (UN $ Basic "===")) [l', r'], + apply (IVar eqFC (UN $ Basic "~=~")) [l', r']]) + desugarTree side ps (Infix loc _ (UN $ Basic "$") l r) -- special case since '$' is special syntax = do l' <- desugarTree side ps l r' <- desugarTree side ps r pure (IApp loc l' r') @@ -668,7 +667,7 @@ mutual -- Note: In case of negated signed integer literals, we apply the -- negation directly. Otherwise, the literal might be -- truncated to 0 before being passed on to `negate`. - desugarTree side ps (Pre loc opFC (UN "-") $ Leaf $ PPrimVal fc c) + desugarTree side ps (Pre loc opFC (UN $ Basic "-") $ Leaf $ PPrimVal fc c) = let newFC = fromMaybe EmptyFC (mergeFC loc fc) continue = desugarTree side ps . Leaf . PPrimVal newFC in case c of @@ -682,11 +681,11 @@ mutual -- not a signed integer literal. proceed by desugaring -- and applying to `negate`. _ => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c) - pure (IApp loc (IVar opFC (UN "negate")) arg') + pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg') - desugarTree side ps (Pre loc opFC (UN "-") arg) + desugarTree side ps (Pre loc opFC (UN $ Basic "-") arg) = do arg' <- desugarTree side ps arg - pure (IApp loc (IVar opFC (UN "negate")) arg') + pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg') desugarTree side ps (Pre loc opFC op arg) = do arg' <- desugarTree side ps arg @@ -801,7 +800,7 @@ mutual ps !(desugar AnyExpr ps ty))) where toRF : Name -> Name - toRF (UN n) = RF n + toRF (UN (Basic n)) = UN (Field n) toRF n = n export @@ -995,17 +994,19 @@ mutual fname (MkField _ _ _ _ n _) = n mkConName : Name -> Name - mkConName (NS ns (UN n)) = NS ns (DN n (MN ("__mk" ++ n) 0)) + mkConName (NS ns (UN n)) + = let str = displayUserName n in + NS ns (DN str (MN ("__mk" ++ str) 0)) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0) mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp) mapDesugarPiInfo ps = traverse (desugar AnyExpr ps) - desugarDecl ps (PFixity fc Prefix prec (UN n)) + desugarDecl ps (PFixity fc Prefix prec (UN (Basic n))) = do syn <- get Syn put Syn (record { prefixes $= insert n prec } syn) pure [] - desugarDecl ps (PFixity fc fix prec (UN n)) + desugarDecl ps (PFixity fc fix prec (UN (Basic n))) = do syn <- get Syn put Syn (record { infixes $= insert n (fix, prec) } syn) pure [] @@ -1022,7 +1023,7 @@ mutual desugarDecl ps (PTransform fc n lhs rhs) = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs) rhs' <- desugar AnyExpr (bound ++ ps) rhs - pure [ITransform fc (UN n) blhs rhs'] + pure [ITransform fc (UN $ Basic n) blhs rhs'] desugarDecl ps (PRunElabDecl fc tm) = do tm' <- desugar AnyExpr ps tm pure [IRunElabDecl fc tm'] diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index 81171e996..1c326410e 100644 --- a/src/Idris/Doc/String.idr +++ b/src/Idris/Doc/String.idr @@ -120,8 +120,10 @@ prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm prettyName : Name -> Doc IdrisDocAnn prettyName n = - let root = nameRoot n in - if isOpName n then parens (pretty root) else pretty root + case userNameRoot n of + -- shouldn't happen: we only show UN anyways... + Nothing => pretty (nameRoot n) + Just un => if isOpUserName un then parens (pretty un) else pretty un prettyKindedName : Maybe String -> Doc IdrisDocAnn -> Doc IdrisDocAnn prettyKindedName Nothing nm = nm @@ -179,7 +181,7 @@ getDocsForName fc n config = do syn <- get Syn defs <- get Ctxt let extra = case nameRoot n of - "-" => [NS numNS (UN "negate")] + "-" => [NS numNS (UN $ Basic "negate")] _ => [] resolved <- lookupCtxtName n (gamma defs) let all@(_ :: _) = extra ++ map fst resolved @@ -237,7 +239,9 @@ getDocsForName fc n config getInfixDoc : Name -> Core (List (Doc IdrisDocAnn)) getInfixDoc n - = do let Just (fixity, assoc) = S.lookupName n (infixes !(get Syn)) + = do let Just (Basic n) = userNameRoot n + | _ => pure [] + let Just (fixity, assoc) = S.lookup n (infixes !(get Syn)) | Nothing => pure [] pure $ pure $ hsep [ pretty (show fixity) @@ -248,7 +252,9 @@ getDocsForName fc n config getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn)) getPrefixDoc n - = do let Just assoc = S.lookupName n (prefixes !(get Syn)) + = do let Just (Basic n) = userNameRoot n + | _ => pure [] + let Just assoc = S.lookup n (prefixes !(get Syn)) | Nothing => pure [] pure $ ["prefix operator, level" <++> pretty (show assoc)] diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 74770b3a5..f71672185 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -39,7 +39,7 @@ export mkImplName : FC -> Name -> List RawImp -> Name mkImplName fc n ps = DN (show n ++ " implementation at " ++ replaceSep (show fc)) - (UN ("__Impl_" ++ show n ++ "_" ++ + (UN $ Basic ("__Impl_" ++ show n ++ "_" ++ showSep "_" (map show ps))) bindConstraints : FC -> PiInfo RawImp -> @@ -64,7 +64,7 @@ addDefaults fc impName params allms defs body extendBody [] missing body where specialiseMeth : Name -> (Name, RawImp) - specialiseMeth n = (n, INamedApp fc (IVar fc n) (UN "__con") (IVar fc impName)) + specialiseMeth n = (n, INamedApp fc (IVar fc n) (UN $ Basic "__con") (IVar fc impName)) -- Given the list of missing names, if any are among the default definitions, -- add them to the body extendBody : List Name -> List Name -> List ImpDecl -> @@ -342,19 +342,19 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i mkLam argns (impsApply (applyTo (IVar EmptyFC n) argns) - (map (\n => (n, IVar vfc (UN (show n)))) imps)) + (map (\n => (n, IVar vfc (UN (Basic $ show n)))) imps)) where applyUpdate : (Name, RigCount, PiInfo RawImp) -> (Name, RigCount, PiInfo RawImp) - applyUpdate (UN n, c, p) - = maybe (UN n, c, p) (\n' => (UN n', c, p)) (lookup n upds) + applyUpdate (UN (Basic n), c, p) + = maybe (UN (Basic n), c, p) (\n' => (UN (Basic n'), c, p)) (lookup n upds) applyUpdate t = t methName : Name -> Name methName (NS _ n) = methName n methName n = DN (show n) - (UN (show n ++ "_" ++ show iname ++ "_" ++ + (UN $ Basic (show n ++ "_" ++ show iname ++ "_" ++ (if named then show impName_in else "") ++ showSep "_" (map show ps))) @@ -450,9 +450,8 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i -- top level method name to current implementation's method name methNameUpdate : (Name, Name, t) -> (Name, Name) methNameUpdate (UN mn, fn, _) = (UN mn, fn) - methNameUpdate (RF mn, fn, _) = (RF mn, fn) methNameUpdate (NS _ mn, fn, p) = methNameUpdate (mn, fn, p) - methNameUpdate (mn, fn, p) = (UN (nameRoot mn), fn) -- probably impossible + methNameUpdate (mn, fn, p) = (UN (Basic $ nameRoot mn), fn) -- probably impossible findMethName : List (Name, Name) -> FC -> Name -> Core Name @@ -510,7 +509,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i "Adding transform for " ++ show meth.name ++ " : " ++ show meth.type ++ "\n\tfor " ++ show iname ++ " in " ++ show ns let lhs = INamedApp vfc (IVar vfc meth.name) - (UN "__con") + (UN $ Basic "__con") (IVar vfc iname) let Just mname = lookup (dropNS meth.name) ns | Nothing => pure () @@ -518,7 +517,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i log "elab.implementation" 5 $ show lhs ++ " ==> " ++ show rhs handleUnify (processDecl [] nest env - (ITransform vfc (UN (show meth.name ++ " " ++ show iname)) lhs rhs)) + (ITransform vfc (UN $ Basic (show meth.name ++ " " ++ show iname)) lhs rhs)) (\err => log "elab.implementation" 5 $ "Can't add transform " ++ show lhs ++ " ==> " ++ show rhs ++ diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index eaa8dda23..733ed1d11 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -172,7 +172,7 @@ getMethDecl {vars} env nest params mnames (c, nm, ty) -- bind the auto implicit for the interface - put it first, as it may be needed -- in other method variables, including implicit variables bindIFace : FC -> RawImp -> RawImp -> RawImp -bindIFace fc ity sc = IPi fc top AutoImplicit (Just (UN "__con")) ity sc +bindIFace fc ity sc = IPi fc top AutoImplicit (Just (UN $ Basic "__con")) ity sc -- Get the top level function for implementing a method getMethToplevel : {vars : _} -> @@ -201,7 +201,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig let argns = getExplicitArgs 0 sig.type -- eta expand the RHS so that we put implicits in the right place let fnclause = PatClause vfc (INamedApp vfc (IVar sig.location cn) - (UN "__con") + (UN $ Basic "__con") conapp) (mkLam argns (apply (IVar EmptyFC (methName sig.name)) @@ -220,7 +220,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty) applyCon : Name -> (Name, RawImp) - applyCon n = let name = UN "__con" in + applyCon n = let name = UN (Basic "__con") in (n, INamedApp vfc (IVar vfc n) name (IVar vfc name)) getExplicitArgs : Int -> RawImp -> List Name @@ -235,12 +235,12 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig = ILam EmptyFC top Explicit (Just x) (Implicit vfc False) (mkLam xs tm) bindName : Name -> String - bindName (UN n) = "__bind_" ++ n + bindName (UN n) = "__bind_" ++ displayUserName n bindName (NS _ n) = bindName n bindName n = show n methName : Name -> Name - methName n = UN (bindName n) + methName n = UN (Basic $ bindName n) -- Get the function for chasing a constraint. This is one of the -- arguments to the record, appearing before the method arguments. @@ -257,7 +257,7 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co let fty = IPi fc top Explicit Nothing ity con ty_imp <- bindTypeNames fc [] (meths ++ vars) fty let hintname = DN ("Constraint " ++ show con) - (UN ("__" ++ show iname ++ "_" ++ show con)) + (UN (Basic $ "__" ++ show iname ++ "_" ++ show con)) let tydecl = IClaim fc top vis [Inline, Hint False] (MkImpTy EmptyFC EmptyFC hintname ty_imp) @@ -271,12 +271,12 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co pure (hintname, [tydecl, fndef]) where bindName : Name -> String - bindName (UN n) = "__bind_" ++ n + bindName (UN n) = "__bind_" ++ displayUserName n bindName (NS _ n) = bindName n bindName n = show n constName : Name -> Name - constName n = UN (bindName n) + constName n = UN (Basic $ bindName n) impsBind : RawImp -> List String -> RawImp impsBind fn [] = fn @@ -290,9 +290,11 @@ getDefault _ = Nothing mkCon : FC -> Name -> Name mkCon loc (NS ns (UN n)) - = NS ns (DN (n ++ " at " ++ show loc) (UN ("__mk" ++ n))) + = let str = displayUserName n in + NS ns (DN (str ++ " at " ++ show loc) (UN $ Basic ("__mk" ++ str))) mkCon loc n - = DN (show n ++ " at " ++ show loc) (UN ("__mk" ++ show n)) + = let str = show n in + DN (str ++ " at " ++ show loc) (UN $ Basic ("__mk" ++ str)) updateIfaceSyn : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -378,7 +380,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp) nameCons i [] = [] nameCons i ((_, ty) :: rest) - = (UN ("__con" ++ show i), ty) :: nameCons (i + 1) rest + = (UN (Basic $ "__con" ++ show i), ty) :: nameCons (i + 1) rest -- Elaborate the data declaration part of the interface elabAsData : (conName : Name) -> List Name -> @@ -476,8 +478,8 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body applyParams : RawImp -> List Name -> RawImp applyParams tm [] = tm - applyParams tm (UN n :: ns) - = applyParams (INamedApp vdfc tm (UN n) (IBindVar vdfc n)) ns + applyParams tm (UN (Basic n) :: ns) + = applyParams (INamedApp vdfc tm (UN (Basic n)) (IBindVar vdfc n)) ns applyParams tm (_ :: ns) = applyParams tm ns changeNameTerm : Name -> RawImp -> Core RawImp diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr index 742bab62c..7c15a36b2 100644 --- a/src/Idris/IDEMode/CaseSplit.idr +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -44,7 +44,7 @@ Updates = List (RawName, String) toStrUpdate : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> (Name, RawImp) -> Core Updates -toStrUpdate (UN n, term) +toStrUpdate (UN (Basic n), term) = do clause <- pterm (map defaultKindedName term) -- hack pure [(n, show (bracket clause))] where @@ -196,7 +196,7 @@ updateCase splits line col getIndent acc _ = acc fnName : Bool -> Name -> String -fnName lhs (UN n) +fnName lhs (UN (Basic n)) = if isIdentNormal n then n else if lhs then "(" ++ n ++ ")" else "op" diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index 3e579c9dc..93ff3926e 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -266,10 +266,6 @@ SExpable a => SExpable (Maybe a) where toSExp Nothing = SExpList [] toSExp (Just x) = toSExp x -export -sym : String -> Name -sym = UN - export version : Int -> Int -> SExp version maj min = toSExp (SymbolAtom "protocol-version", maj, min) diff --git a/src/Idris/IDEMode/Holes.idr b/src/Idris/IDEMode/Holes.idr index a4c0c894a..ffcf3f4c5 100644 --- a/src/Idris/IDEMode/Holes.idr +++ b/src/Idris/IDEMode/Holes.idr @@ -48,7 +48,7 @@ isHole def -- Bring these back into REPL.idr showName : Name -> Bool -showName (UN "_") = False +showName (UN Underscore) = False showName (MN _ _) = False showName _ = True diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 653cd7b05..a0fa770fb 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -167,40 +167,45 @@ process (LoadFile fname_in _) replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname process (NameAt name Nothing) = do defs <- get Ctxt - glob <- lookupCtxtName (UN name) (gamma defs) + glob <- lookupCtxtName (UN (mkUserName name)) (gamma defs) let dat = map (\(name, _, gdef) => (name, gdef.location)) glob pure (NameLocList dat) process (NameAt n (Just _)) = do todoCmd "name-at " pure $ REPL $ Edited $ DisplayEdit emptyDoc process (TypeOf n Nothing) - = replWrap $ Idris.REPL.process (Check (PRef replFC (UN n))) + = replWrap $ Idris.REPL.process (Check (PRef replFC (UN $ mkUserName n))) process (TypeOf n (Just (l, c))) - = replWrap $ Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n))) + = replWrap $ Idris.REPL.process + $ Editing (TypeAt (fromInteger l) (fromInteger c) (UN $ mkUserName n)) process (CaseSplit l c n) - = replWrap $ Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n))) + = replWrap $ Idris.REPL.process + $ Editing $ CaseSplit False (fromInteger l) (fromInteger c) + $ UN $ mkUserName n process (AddClause l n) - = replWrap $ Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process + $ Editing $ AddClause False (fromInteger l) + $ UN $ mkUserName n process (AddMissing l n) = do todoCmd "add-missing" pure $ REPL $ Edited $ DisplayEdit emptyDoc process (ExprSearch l n hs all) - = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) - (map UN hs))) + = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) + (UN $ Basic n) (map (UN . Basic) hs))) process ExprSearchNext = replWrap $ Idris.REPL.process (Editing ExprSearchNext) process (GenerateDef l n) - = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n) 0)) + = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN $ Basic n) 0)) process GenerateDefNext = replWrap $ Idris.REPL.process (Editing GenerateDefNext) process (MakeLemma l n) - = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN $ mkUserName n))) process (MakeCase l n) - = replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN $ mkUserName n))) process (MakeWith l n) - = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN $ mkUserName n))) process (DocsFor n modeOpt) - = replWrap $ Idris.REPL.process (Doc (PRef EmptyFC (UN n))) + = replWrap $ Idris.REPL.process (Doc (PRef EmptyFC (UN $ mkUserName n))) process (Apropos n) = do todoCmd "apropros" pure $ REPL $ Printed emptyDoc diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 8aec9fc49..dbc850408 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -331,7 +331,7 @@ build pkg opts Just exec => do let Just (mainNS, mainFile) = mainmod pkg | Nothing => throw (GenericMsg emptyFC "No main module given") - let mainName = NS (miAsNamespace mainNS) (UN "main") + let mainName = NS (miAsNamespace mainNS) (UN $ Basic "main") compileMain mainName mainFile exec runScript (postbuild pkg) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 3bdf01936..d3ca5dca4 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -219,17 +219,17 @@ mutual else fail "| not allowed here" where underscore : FC -> ArgType - underscore fc = NamedArg (UN "_") (PImplicit fc) + underscore fc = NamedArg (UN Underscore) (PImplicit fc) braceArgs : OriginDesc -> IndentInfo -> Rule (List ArgType) braceArgs fname indents = do start <- bounds (decoratedSymbol fname "{") list <- sepBy (decoratedSymbol fname ",") - $ do x <- bounds (decoratedSimpleBinderName fname) + $ do x <- bounds (UN . Basic <$> decoratedSimpleBinderName fname) let fc = boundToFC fname x - option (NamedArg (UN x.val) $ PRef fc (UN x.val)) + option (NamedArg x.val $ PRef fc x.val) $ do tm <- decoratedSymbol fname "=" *> typeExpr pdef fname indents - pure (NamedArg (UN x.val) tm) + pure (NamedArg x.val tm) matchAny <- option [] (if isCons list then do decoratedSymbol fname "," x <- bounds (decoratedSymbol fname "_") @@ -280,14 +280,14 @@ mutual pure $ let fc = boundToFC fname (mergeBounds l r) opFC = virtualiseFC fc -- already been highlighted: we don't care - in POp fc opFC (UN "=") l.val r.val + in POp fc opFC (UN $ Basic "=") l.val r.val else fail "= not allowed") <|> (do b <- bounds $ do continue indents op <- bounds iOperator e <- case op.val of - UN "$" => typeExpr q fname indents + UN (Basic "$") => typeExpr q fname indents _ => expr q fname indents pure (op, e) (op, r) <- pure b.val @@ -298,7 +298,7 @@ mutual dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm dpairType fname start indents - = do loc <- bounds (do x <- decoratedSimpleBinderName fname + = do loc <- bounds (do x <- UN . Basic <$> decoratedSimpleBinderName fname decoratedSymbol fname ":" ty <- typeExpr pdef fname indents pure (x, ty)) @@ -307,7 +307,7 @@ mutual rest <- bounds (nestedDpair fname loc indents <|> typeExpr pdef fname indents) pure (PDPair (boundToFC fname (mergeBounds start rest)) (boundToFC fname op) - (PRef (boundToFC fname loc) (UN x)) + (PRef (boundToFC fname loc) x) ty rest.val) @@ -494,13 +494,13 @@ mutual simplerExpr : OriginDesc -> IndentInfo -> Rule PTerm simplerExpr fname indents - = do b <- bounds (do x <- bounds (decoratedSimpleBinderName fname) + = do b <- bounds (do x <- bounds (UN . Basic <$> decoratedSimpleBinderName fname) decoratedSymbol fname "@" commit expr <- simpleExpr fname indents pure (x, expr)) (x, expr) <- pure b.val - pure (PAs (boundToFC fname b) (boundToFC fname x) (UN x.val) expr) + pure (PAs (boundToFC fname b) (boundToFC fname x) x.val expr) <|> atom fname <|> record_ fname indents <|> singlelineStr pdef fname indents @@ -586,8 +586,9 @@ mutual Rule (List (RigCount, WithBounds Name, PTerm)) pibindListName fname indents = do rig <- multiplicity fname - ns <- sepBy1 (decoratedSymbol fname ",") (bounds binderName) - let ns = forget $ map (map UN) ns + ns <- sepBy1 (decoratedSymbol fname ",") + (bounds $ UN <$> binderName) + let ns = forget ns decorateBoundedNames fname Bound ns decoratedSymbol fname ":" ty <- typeExpr pdef fname indents @@ -601,8 +602,9 @@ mutual pure (rig, map UN n, ty)) where -- _ gets treated specially here, it means "I don't care about the name" - binderName : Rule String - binderName = unqualifiedName <|> (symbol "_" $> "_") + binderName : Rule UserName + binderName = Basic <$> unqualifiedName + <|> symbol "_" $> Underscore pibindList : OriginDesc -> IndentInfo -> Rule (List (RigCount, WithBounds (Maybe Name), PTerm)) @@ -665,7 +667,7 @@ mutual ns <- sepBy1 (decoratedSymbol fname ",") (bounds (decoratedSimpleBinderName fname)) pure $ map (\n => ( erased {a=RigCount} - , map (Just . UN) n + , map (Just . UN . Basic) n , PImplicit (boundToFC fname n)) ) (forget ns) mustWorkBecause b.bounds "Cannot return a forall quantifier" @@ -806,8 +808,8 @@ mutual pure (upd path val) where fieldName : Name -> String - fieldName (UN s) = s - fieldName (RF s) = s + fieldName (UN (Basic s)) = s + fieldName (UN (Field s)) = s fieldName _ = "_impossible" -- this allows the dotted syntax .field @@ -844,14 +846,15 @@ mutual _ => fail "Not a namespaced 'do'" validPatternVar : Name -> EmptyRule () - validPatternVar (UN n) - = unless (lowerFirst n || n == "_") $ + validPatternVar (UN Underscore) = pure () + validPatternVar (UN (Basic n)) + = unless (lowerFirst n) $ fail "Not a pattern variable" validPatternVar _ = fail "Not a pattern variable" doAct : OriginDesc -> IndentInfo -> Rule (List PDo) doAct fname indents - = do b <- bounds (do n <- bounds (name <|> UN "_" <$ symbol "_") + = do b <- bounds (do n <- bounds (name <|> UN Underscore <$ symbol "_") -- If the name doesn't begin with a lower case letter, we should -- treat this as a pattern, so fail validPatternVar n.val @@ -1027,7 +1030,7 @@ mutual start <- bounds (decoratedSymbol fname "(") wval <- bracketedExpr fname start indents prf <- optional (decoratedKeyword fname "proof" - *> UN <$> decoratedSimpleBinderName fname) + *> UN . Basic <$> decoratedSimpleBinderName fname) ws <- mustWork $ nonEmptyBlockAfter col $ clause (S withArgs) (Just lhs) fname pure (prf, flags, wval, forget ws)) @@ -1343,7 +1346,7 @@ usingDecls fname indents (do n <- optional (do x <- unqualifiedName decoratedSymbol fname ":" - pure (UN x)) + pure (UN $ Basic x)) ty <- typeExpr pdef fname indents pure (n, ty)) decoratedSymbol fname ")" @@ -1579,10 +1582,10 @@ paramDecls fname indents oldParamDecls fname indents = do decoratedSymbol fname "(" ps <- sepBy (decoratedSymbol fname ",") - (do x <- decoratedSimpleBinderName fname + (do x <- UN . Basic <$> decoratedSimpleBinderName fname decoratedSymbol fname ":" ty <- typeExpr pdef fname indents - pure (UN x, top, Explicit, ty)) + pure (x, top, Explicit, ty)) decoratedSymbol fname ")" pure ps diff --git a/src/Idris/Parser/Let.idr b/src/Idris/Parser/Let.idr index 66b6bdcdf..a89c0e149 100644 --- a/src/Idris/Parser/Let.idr +++ b/src/Idris/Parser/Let.idr @@ -82,12 +82,12 @@ mkDoLets origin lets = letFactory buildDoLets : List (WithBounds LetBinder) -> List PDo buildDoLets [] = [] buildDoLets (b :: rest) = let fc = boundToFC origin b in case b.val of - (MkLetBinder rig (PRef fc' (UN n)) ty val []) => - (if lowerFirst n - then DoLet fc fc' (UN n) rig ty val - else DoLetPat fc (PRef fc' (UN n)) ty val [] + (MkLetBinder rig (PRef fc' (UN un)) ty val []) => + (if isPatternVariable un + then DoLet fc fc' (UN un) rig ty val + else DoLetPat fc (PRef fc' (UN un)) ty val [] ) :: buildDoLets rest (MkLetBinder rig (PImplicit fc') ty val []) => - DoLet fc fc' (UN "_") rig ty val :: buildDoLets rest + DoLet fc fc' (UN Underscore) rig ty val :: buildDoLets rest (MkLetBinder rig pat ty val alts) => DoLetPat fc pat ty val alts :: buildDoLets rest diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 914e9ffc8..bad3c2632 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -396,12 +396,12 @@ mutual where dePure : IPTerm -> IPTerm dePure tm@(PApp _ (PRef _ n) arg) - = if dropNS (rawName n) == UN "pure" then arg else tm + = if dropNS (rawName n) == UN (Basic "pure") then arg else tm dePure tm = tm deGuard : PDo' KindedName -> PDo' KindedName deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) - = if dropNS (rawName n) == UN "guard" then DoExp fc arg else tm + = if dropNS (rawName n) == UN (Basic "guard") then DoExp fc arg else tm deGuard tm = tm go d (PRewrite _ rule tm) = parenthesise (d > appPrec) $ group $ rewrite_ <++> go startPrec rule <+> line <+> in_ <++> go startPrec tm diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index c977060d5..b5fd46f57 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -543,7 +543,10 @@ getItDecls = do opts <- get ROpts case evalResultName opts of Nothing => pure [] - Just n => pure [ IClaim replFC top Private [] (MkImpTy replFC EmptyFC (UN "it") (Implicit replFC False)), IDef replFC (UN "it") [PatClause replFC (IVar replFC (UN "it")) (IVar replFC n)]] + Just n => + let it = UN $ Basic "it" in + pure [ IClaim replFC top Private [] (MkImpTy replFC EmptyFC it (Implicit replFC False)) + , IDef replFC it [PatClause replFC (IVar replFC it) (IVar replFC n)]] prepareExp : {auto c : Ref Ctxt Defs} -> @@ -553,9 +556,9 @@ prepareExp : {auto o : Ref ROpts REPLOpts} -> PTerm -> Core ClosedTerm prepareExp ctm - = do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm) + = do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN $ Basic "unsafePerformIO")) ctm) let ttimpWithIt = ILocal replFC !getItDecls ttimp - inidx <- resolveName (UN "[input]") + inidx <- resolveName (UN $ Basic "[input]") (tm, ty) <- elabTerm inidx InExpr [] (MkNested []) [] ttimpWithIt Nothing tm_erased <- linearCheck replFC linear True [] tm @@ -604,7 +607,7 @@ execDecls decls = do execDecl : PDecl -> Core () execDecl decl = do i <- desugarDecl [] decl - inidx <- resolveName (UN "[defs]") + inidx <- resolveName (UN $ Basic "[defs]") _ <- newRef EST (initEStateSub inidx [] SubRefl) processLocal [] (MkNested []) [] !getItDecls i @@ -675,13 +678,13 @@ inferAndElab : {auto c : Ref Ctxt Defs} -> inferAndElab emode itm = do ttimp <- desugar AnyExpr [] itm let ttimpWithIt = ILocal replFC !getItDecls ttimp - inidx <- resolveName (UN "[input]") + inidx <- resolveName (UN $ Basic "[input]") -- a TMP HACK to prioritise list syntax for List: hide -- foreign argument lists. TODO: once the new FFI is fully -- up and running we won't need this. Also, if we add -- 'with' disambiguation we can use that instead. - catch (do hide replFC (NS primIONS (UN "::")) - hide replFC (NS primIONS (UN "Nil"))) + catch (do hide replFC (NS primIONS (UN $ Basic "::")) + hide replFC (NS primIONS (UN $ Basic "Nil"))) (\err => pure ()) (tm , gty) <- elabTerm inidx emode [] (MkNested []) [] ttimpWithIt Nothing @@ -745,10 +748,10 @@ process (Eval itm) then do ity <- resugar [] !(norm defs [] ty) pure (Evaluated itm (Just ity)) else pure (Evaluated itm Nothing) -process (Check (PRef fc (UN "it"))) +process (Check (PRef fc (UN (Basic "it")))) = do opts <- get ROpts case evalResultName opts of - Nothing => throw (UndefinedName fc (UN "it")) + Nothing => throw (UndefinedName fc (UN $ Basic "it")) Just n => process (Check (PRef fc n)) process (Check (PRef fc fn)) = do defs <- get Ctxt diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 84af4e168..5c8de24d6 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -106,11 +106,11 @@ unbracket tm = tm ||| Attempt to extract a constant natural number extractNat : Nat -> IPTerm -> Maybe Nat extractNat acc tm = case tm of - PRef _ (MkKindedName _ _ (NS ns (UN n))) => + PRef _ (MkKindedName _ _ (NS ns (UN (Basic n)))) => do guard (n == "Z") guard (ns == typesNS || ns == preludeNS) pure acc - PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN n)))) k => case n of + PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of "S" => do guard (ns == typesNS || ns == preludeNS) extractNat (1 + acc) k "fromInteger" => extractNat acc k @@ -188,9 +188,9 @@ sugarName x = show x toPRef : FC -> KindedName -> Core IPTerm toPRef fc kn@(MkKindedName nt fn nm) = case nm of - MN n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN n))) + MN n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n))) PV n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ n))) - DN n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN n))) + DN n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n))) Nested _ n => toPRef fc (MkKindedName nt fn n) _ => pure (sugarApp (PRef fc kn)) @@ -218,11 +218,11 @@ mutual else toPTerm p ret where needsBind : Maybe Name -> Bool - needsBind (Just (UN t)) + needsBind (Just nm@(UN (Basic t))) = let ret = map rawName ret ns = findBindableNames False [] [] ret allNs = findAllNames [] ret in - ((UN t) `elem` allNs) && not (t `elem` (map Builtin.fst ns)) + (nm `elem` allNs) && not (t `elem` (map Builtin.fst ns)) needsBind _ = False toPTerm p (IPi fc rig pt n arg ret) = do arg' <- toPTerm appPrec arg @@ -231,7 +231,7 @@ mutual bracket p tyPrec (PPi fc rig pt' n arg' ret') toPTerm p (ILam fc rig pt mn arg sc) = do let n = case mn of - Nothing => UN "_" + Nothing => UN Underscore Just n' => n' imp <- showImplicits arg' <- if imp then toPTerm tyPrec arg @@ -262,8 +262,8 @@ mutual mkIf : IPTerm -> IPTerm mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [], MkPatClause _ (PRef _ fval) f []]) - = if dropNS (rawName tval) == UN "True" - && dropNS (rawName fval) == UN "False" + = if dropNS (rawName tval) == UN (Basic "True") + && dropNS (rawName fval) == UN (Basic "False") then PIfThenElse loc sc t f else tm mkIf tm = tm @@ -304,7 +304,9 @@ mutual toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c) toPTerm p (IHole fc str) = pure (PHole fc False str) toPTerm p (IType fc) = pure (PType fc) - toPTerm p (IBindVar fc v) = pure (PRef fc (MkKindedName (Just Bound) (UN v) (UN v))) + toPTerm p (IBindVar fc v) + = let nm = UN (Basic v) in + pure (PRef fc (MkKindedName (Just Bound) nm nm)) toPTerm p (IBindHere fc _ tm) = toPTerm p tm toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat)) toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat)) @@ -495,19 +497,19 @@ cleanPTerm ptm cleanName : Name -> Core Name cleanName nm = case nm of - MN n _ => pure (UN n) + MN n _ => pure (UN $ mkUserName n) -- this may be "_" PV n _ => pure n - DN n _ => pure (UN n) + DN n _ => pure (UN $ mkUserName n) -- this may be "_" NS _ n => cleanName n Nested _ n => cleanName n - RF n => pure (RF n) - _ => UN <$> prettyName nm + UN n => pure (UN n) + _ => UN . mkUserName <$> prettyName nm cleanKindedName : KindedName -> Core KindedName cleanKindedName (MkKindedName nt fn nm) = MkKindedName nt fn <$> cleanName nm cleanBinderName : PiInfo IPTerm -> Name -> Core (Maybe Name) - cleanBinderName AutoImplicit (UN "__con") = pure Nothing + cleanBinderName AutoImplicit (UN (Basic "__con")) = pure Nothing cleanBinderName _ nm = Just <$> cleanName nm cleanNode : IPTerm -> Core IPTerm diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index bbcf46184..488c21877 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -451,11 +451,11 @@ postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest) = do ignore $ postOptions res rest pure False postOptions res (OutputFile outfile :: rest) - = do ignore $ compileExp (PRef EmptyFC (UN "main")) outfile + = do ignore $ compileExp (PRef EmptyFC (UN $ Basic "main")) outfile ignore $ postOptions res rest pure False postOptions res (ExecFn str :: rest) - = do ignore $ execExp (PRef EmptyFC (UN str)) + = do ignore $ execExp (PRef EmptyFC (UN $ Basic str)) ignore $ postOptions res rest pure False postOptions res (CheckOnly :: rest) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index cb0c7c9ff..77f96802c 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -321,17 +321,22 @@ mutual directiveList : List Directive directiveList = - [ (Hide (UN "")), (Logging Nothing), (LazyOn False) + [ (Hide ph), (Logging Nothing), (LazyOn False) , (UnboundImplicits False), (AmbigDepth 0) - , (PairNames (UN "") (UN "") (UN "")), (RewriteName (UN "") (UN "")) - , (PrimInteger (UN "")), (PrimString (UN "")), (PrimChar (UN "")) - , (PrimDouble (UN "")), (CGAction "" ""), (Names (UN "") []) - , (StartExpr (PRef EmptyFC (UN ""))), (Overloadable (UN "")) + , (PairNames ph ph ph), (RewriteName ph ph) + , (PrimInteger ph), (PrimString ph), (PrimChar ph) + , (PrimDouble ph), (CGAction "" ""), (Names ph []) + , (StartExpr (PRef EmptyFC ph)), (Overloadable ph) , (Extension ElabReflection), (DefaultTotality PartialOK) , (PrefixRecordProjections True), (AutoImplicitDepth 0) , (NFMetavarThreshold 0), (SearchTimeout 0) ] + where + -- placeholder + ph : Name + ph = UN $ Basic "" + isPragma : Directive -> Bool isPragma (CGAction _ _) = False isPragma _ = True @@ -773,12 +778,12 @@ parameters {0 nm : Type} (toName : nm -> Name) where dePure : PTerm' nm -> PTerm' nm dePure tm@(PApp _ (PRef _ n) arg) - = if dropNS (toName n) == UN "pure" then arg else tm + = if dropNS (toName n) == UN (Basic "pure") then arg else tm dePure tm = tm deGuard : PDo' nm -> PDo' nm deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) - = if dropNS (toName n) == UN "guard" then DoExp fc arg else tm + = if dropNS (toName n) == UN (Basic "guard") then DoExp fc arg else tm deGuard tm = tm showPTermPrec d (PRewrite _ rule tm) = "rewrite " ++ showPTermPrec d rule ++ " in " ++ showPTermPrec d tm @@ -987,7 +992,7 @@ initSyntax initDocStrings [] [] - (IVar EmptyFC (UN "main")) + (IVar EmptyFC (UN $ Basic "main")) where diff --git a/src/Libraries/Data/ANameMap.idr b/src/Libraries/Data/ANameMap.idr index 4067bb411..5e29a04fb 100644 --- a/src/Libraries/Data/ANameMap.idr +++ b/src/Libraries/Data/ANameMap.idr @@ -5,7 +5,7 @@ import Core.Name import Data.List import Libraries.Data.NameMap -import Libraries.Data.StringMap +import Libraries.Data.UserNameMap %default total @@ -16,7 +16,7 @@ record ANameMap a where exactNames : NameMap a -- for looking up by name root or partially qualified (so possibly -- ambiguous) names. This doesn't store machine generated names. - hierarchy : StringMap (List (Name, a)) + hierarchy : UserNameMap (List (Name, a)) export empty : ANameMap a @@ -39,7 +39,7 @@ lookupName n dict Just ns => filter (matches n . fst) ns addToHier : Name -> a -> - StringMap (List (Name, a)) -> StringMap (List (Name, a)) + UserNameMap (List (Name, a)) -> UserNameMap (List (Name, a)) addToHier n val hier -- Only add user defined names. Machine generated names can only be -- found with the exactNames diff --git a/src/Libraries/Data/StringMap.idr b/src/Libraries/Data/StringMap.idr index 3d7fff119..6ef6e46c1 100644 --- a/src/Libraries/Data/StringMap.idr +++ b/src/Libraries/Data/StringMap.idr @@ -2,8 +2,6 @@ module Libraries.Data.StringMap -- Hand specialised map, for efficiency... -import Core.Name - %default total Key : Type @@ -219,12 +217,6 @@ lookup : String -> StringMap v -> Maybe v lookup _ Empty = Nothing lookup k (M _ t) = treeLookup k t -export -lookupName : (n : Name) -> (dict : StringMap v) -> Maybe v -lookupName n dict = case userNameRoot n of - Nothing => Nothing - Just str => lookup str dict - export insert : String -> v -> StringMap v -> StringMap v insert k v Empty = M Z (Leaf k v) diff --git a/src/Libraries/Data/UserNameMap.idr b/src/Libraries/Data/UserNameMap.idr new file mode 100644 index 000000000..e6ad1820f --- /dev/null +++ b/src/Libraries/Data/UserNameMap.idr @@ -0,0 +1,326 @@ +module Libraries.Data.UserNameMap + +-- Hand specialised map, for efficiency... + +import Core.Name + +%default total + +Key : Type +Key = UserName + +-- TODO: write split + +private +data Tree : Nat -> Type -> Type where + Leaf : Key -> v -> Tree Z v + Branch2 : Tree n v -> Key -> Tree n v -> Tree (S n) v + Branch3 : Tree n v -> Key -> Tree n v -> Key -> Tree n v -> Tree (S n) v + +branch4 : + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> + Tree (S (S n)) v +branch4 a b c d e f g = + Branch2 (Branch2 a b c) d (Branch2 e f g) + +branch5 : + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> + Tree (S (S n)) v +branch5 a b c d e f g h i = + Branch2 (Branch2 a b c) d (Branch3 e f g h i) + +branch6 : + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> + Tree (S (S n)) v +branch6 a b c d e f g h i j k = + Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k) + +branch7 : + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> Key -> + Tree n v -> + Tree (S (S n)) v +branch7 a b c d e f g h i j k l m = + Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m) + +merge1 : Tree n v -> Key -> Tree (S n) v -> Key -> Tree (S n) v -> Tree (S (S n)) v +merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i +merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k +merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k +merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m + +merge2 : Tree (S n) v -> Key -> Tree n v -> Key -> Tree (S n) v -> Tree (S (S n)) v +merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i +merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k +merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k +merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m + +merge3 : Tree (S n) v -> Key -> Tree (S n) v -> Key -> Tree n v -> Tree (S (S n)) v +merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i +merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k +merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k +merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m + +treeLookup : Key -> Tree n v -> Maybe v +treeLookup k (Leaf k' v) = + if k == k' then + Just v + else + Nothing +treeLookup k (Branch2 t1 k' t2) = + if k <= k' then + treeLookup k t1 + else + treeLookup k t2 +treeLookup k (Branch3 t1 k1 t2 k2 t3) = + if k <= k1 then + treeLookup k t1 + else if k <= k2 then + treeLookup k t2 + else + treeLookup k t3 + +treeInsert' : Key -> v -> Tree n v -> Either (Tree n v) (Tree n v, Key, Tree n v) +treeInsert' k v (Leaf k' v') = + case compare k k' of + LT => Right (Leaf k v, k, Leaf k' v') + EQ => Left (Leaf k v) + GT => Right (Leaf k' v', k', Leaf k v) +treeInsert' k v (Branch2 t1 k' t2) = + if k <= k' then + case treeInsert' k v t1 of + Left t1' => Left (Branch2 t1' k' t2) + Right (a, b, c) => Left (Branch3 a b c k' t2) + else + case treeInsert' k v t2 of + Left t2' => Left (Branch2 t1 k' t2') + Right (a, b, c) => Left (Branch3 t1 k' a b c) +treeInsert' k v (Branch3 t1 k1 t2 k2 t3) = + if k <= k1 then + case treeInsert' k v t1 of + Left t1' => Left (Branch3 t1' k1 t2 k2 t3) + Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3) + else + if k <= k2 then + case treeInsert' k v t2 of + Left t2' => Left (Branch3 t1 k1 t2' k2 t3) + Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3) + else + case treeInsert' k v t3 of + Left t3' => Left (Branch3 t1 k1 t2 k2 t3') + Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c) + +treeInsert : Key -> v -> Tree n v -> Either (Tree n v) (Tree (S n) v) +treeInsert k v t = + case treeInsert' k v t of + Left t' => Left t' + Right (a, b, c) => Right (Branch2 a b c) + +delType : Nat -> Type -> Type +delType Z v = () +delType (S n) v = Tree n v + +treeDelete : {n : _} -> Key -> Tree n v -> Either (Tree n v) (delType n v) +treeDelete k (Leaf k' v) = + if k == k' then + Right () + else + Left (Leaf k' v) +treeDelete {n=S Z} k (Branch2 t1 k' t2) = + if k <= k' then + case treeDelete k t1 of + Left t1' => Left (Branch2 t1' k' t2) + Right () => Right t2 + else + case treeDelete k t2 of + Left t2' => Left (Branch2 t1 k' t2') + Right () => Right t1 +treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) = + if k <= k1 then + case treeDelete k t1 of + Left t1' => Left (Branch3 t1' k1 t2 k2 t3) + Right () => Left (Branch2 t2 k2 t3) + else if k <= k2 then + case treeDelete k t2 of + Left t2' => Left (Branch3 t1 k1 t2' k2 t3) + Right () => Left (Branch2 t1 k1 t3) + else + case treeDelete k t3 of + Left t3' => Left (Branch3 t1 k1 t2 k2 t3') + Right () => Left (Branch2 t1 k1 t2) +treeDelete {n=S (S _)} k (Branch2 t1 k' t2) = + if k <= k' then + case treeDelete k t1 of + Left t1' => Left (Branch2 t1' k' t2) + Right t1' => + case t2 of + Branch2 a b c => Right (Branch3 t1' k' a b c) + Branch3 a b c d e => Left (branch4 t1' k' a b c d e) + else + case treeDelete k t2 of + Left t2' => Left (Branch2 t1 k' t2') + Right t2' => + case t1 of + Branch2 a b c => Right (Branch3 a b c k' t2') + Branch3 a b c d e => Left (branch4 a b c d e k' t2') +treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) = + if k <= k1 then + case treeDelete k t1 of + Left t1' => Left (Branch3 t1' k1 t2 k2 t3) + Right t1' => Left (merge1 t1' k1 t2 k2 t3) + else if k <= k2 then + case treeDelete k t2 of + Left t2' => Left (Branch3 t1 k1 t2' k2 t3) + Right t2' => Left (merge2 t1 k1 t2' k2 t3) + else + case treeDelete k t3 of + Left t3' => Left (Branch3 t1 k1 t2 k2 t3') + Right t3' => Left (merge3 t1 k1 t2 k2 t3') + +treeToList : Tree n v -> List (Key, v) +treeToList = treeToList' (:: []) + where + treeToList' : forall n . ((Key, v) -> List (Key, v)) -> Tree n v -> List (Key, v) + treeToList' cont (Leaf k v) = cont (k, v) + treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1 + treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1 + +export +data UserNameMap : Type -> Type where + Empty : UserNameMap v + M : (n : Nat) -> Tree n v -> UserNameMap v + +export +empty : UserNameMap v +empty = Empty + +export +singleton : UserName -> v -> UserNameMap v +singleton k v = M Z (Leaf k v) + +export +lookup : UserName -> UserNameMap v -> Maybe v +lookup _ Empty = Nothing +lookup k (M _ t) = treeLookup k t + +export +lookupName : (n : Name) -> (dict : UserNameMap v) -> Maybe v +lookupName n dict = case userNameRoot n of + Nothing => Nothing + Just un => lookup un dict + +export +insert : UserName -> v -> UserNameMap v -> UserNameMap v +insert k v Empty = M Z (Leaf k v) +insert k v (M _ t) = + case treeInsert k v t of + Left t' => (M _ t') + Right t' => (M _ t') + +export +insertFrom : List (UserName, v) -> UserNameMap v -> UserNameMap v +insertFrom = flip $ foldl $ flip $ uncurry insert + +export +delete : UserName -> UserNameMap v -> UserNameMap v +delete _ Empty = Empty +delete k (M Z t) = + case treeDelete k t of + Left t' => (M _ t') + Right () => Empty +delete k (M (S _) t) = + case treeDelete k t of + Left t' => (M _ t') + Right t' => (M _ t') + +export +fromList : List (UserName, v) -> UserNameMap v +fromList l = foldl (flip (uncurry insert)) empty l + +export +toList : UserNameMap v -> List (UserName, v) +toList Empty = [] +toList (M _ t) = treeToList t + +||| Gets the Keys of the map. +export +keys : UserNameMap v -> List UserName +keys = map fst . UserNameMap.toList + +||| Gets the values of the map. Could contain duplicates. +export +values : UserNameMap v -> List v +values = map snd . UserNameMap.toList + +treeMap : (a -> b) -> Tree n a -> Tree n b +treeMap f (Leaf k v) = Leaf k (f v) +treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2) +treeMap f (Branch3 t1 k1 t2 k2 t3) + = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3) + +export +implementation Functor UserNameMap where + map _ Empty = Empty + map f (M n t) = M _ (treeMap f t) + +||| Merge two maps. When encountering duplicate keys, using a function to combine the values. +||| Uses the ordering of the first map given. +export +mergeWith : (v -> v -> v) -> UserNameMap v -> UserNameMap v -> UserNameMap v +mergeWith f x y = insertFrom inserted x where + inserted : List (Key, v) + inserted = do + (k, v) <- UserNameMap.toList y + let v' = (maybe id f $ lookup k x) v + pure (k, v') + +||| Merge two maps using the Semigroup (and by extension, Monoid) operation. +||| Uses mergeWith internally, so the ordering of the left map is kept. +export +merge : Semigroup v => UserNameMap v -> UserNameMap v -> UserNameMap v +merge = mergeWith (<+>) + +||| Left-biased merge, also keeps the ordering specified by the left map. +export +mergeLeft : UserNameMap v -> UserNameMap v -> UserNameMap v +mergeLeft x y = mergeWith const x y + +export +adjust : UserName -> (v -> v) -> UserNameMap v -> UserNameMap v +adjust k f m = + case lookup k m of + Nothing => m + Just v => insert k (f v) m + +export +Show v => Show (UserNameMap v) where + show m = show $ map (\(k,v) => show k ++ "->" ++ show v) $ UserNameMap.toList m + +-- TODO: is this the right variant of merge to use for this? I think it is, but +-- I could also see the advantages of using `mergeLeft`. The current approach is +-- strictly more powerful I believe, because `mergeLeft` can be emulated with +-- the `First` monoid. However, this does require more code to do the same +-- thing. +export +Semigroup v => Semigroup (UserNameMap v) where + (<+>) = merge + +export +(Semigroup v) => Monoid (UserNameMap v) where + neutral = empty diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 0b7e36def..2458c9567 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -245,16 +245,18 @@ isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~") export ||| Test whether a user name begins with an operator symbol. -isOpName : Name -> Bool -isOpName n = fromMaybe False $ do - -- NB: we can't use userNameRoot because that'll prefix `RF` - -- names with a `.` which means that record fields will systematically - -- be declared to be operators. - guard (isUserName n) - let n = nameRoot n +isOpUserName : UserName -> Bool +isOpUserName (Basic n) = fromMaybe False $ do c <- fst <$> strUncons n guard (isOpChar c) pure True +isOpUserName (Field _) = False +isOpUserName Underscore = False + +export +||| Test whether a name begins with an operator symbol. +isOpName : Name -> Bool +isOpName = maybe False isOpUserName . userNameRoot validSymbol : Lexer validSymbol = some (pred isOpChar) diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 00f3a7a49..571f17d31 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -41,7 +41,7 @@ constant CharLit c => Ch <$> getCharLit c DoubleLit d => Just (Db d) IntegerLit i => Just (BI i) - Ident s => isConstantType (UN s) >>= + Ident s => isConstantType (UN $ Basic s) >>= \case WorldType => Nothing c => Just c _ => Nothing @@ -140,7 +140,7 @@ aDotIdent = terminal "Expected dot+identifier" $ export postfixProj : Rule Name -postfixProj = RF <$> aDotIdent +postfixProj = UN . Field <$> aDotIdent export symbol : String -> Rule () @@ -188,7 +188,7 @@ operatorCandidate : Rule Name operatorCandidate = terminal "Expected operator" $ \case - Symbol s => Just (UN s) + Symbol s => Just (UN $ Basic s) -- TODO: have an operator construct? _ => Nothing export @@ -199,7 +199,7 @@ operator Symbol s => if s `elem` reservedSymbols then Nothing - else Just (UN s) + else Just (UN $ Basic s) -- TODO: have an operator construct? _ => Nothing identPart : Rule String @@ -296,7 +296,7 @@ nameWithCapital b = opNonNS <|> do let id = snd <$> nsx identWithCapital b id isNotReservedName id - pure $ uncurry mkNamespacedName nsx.val + pure $ uncurry mkNamespacedName (map Basic nsx.val) opNS : WithBounds (Maybe Namespace, String) -> Rule Name opNS nsx = do @@ -325,7 +325,7 @@ capitalisedIdent = do export dataConstructorName : Rule Name -dataConstructorName = opNonNS <|> UN <$> capitalisedIdent +dataConstructorName = opNonNS <|> (UN . Basic) <$> capitalisedIdent export %inline dataTypeName : Rule Name diff --git a/src/TTImp/BindImplicits.idr b/src/TTImp/BindImplicits.idr index 989390acd..760857ecd 100644 --- a/src/TTImp/BindImplicits.idr +++ b/src/TTImp/BindImplicits.idr @@ -19,19 +19,20 @@ export renameIBinds : (renames : List String) -> (used : List String) -> RawImp -> State (List (String, String)) RawImp -renameIBinds rs us (IPi fc c p (Just (UN n)) ty sc) +renameIBinds rs us (IPi fc c p (Just un@(UN (Basic n))) ty sc) = if n `elem` rs then let n' = getUnique (rs ++ us) n - sc' = substNames (map UN (filter (/= n) us)) - [(UN n, IVar fc (UN n'))] sc in + un' = UN (Basic n') + sc' = substNames (map (UN . Basic) (filter (/= n) us)) + [(un, IVar fc un')] sc in do scr <- renameIBinds rs (n' :: us) sc' ty' <- renameIBinds rs us ty upds <- get put ((n, n') :: upds) - pure $ IPi fc c p (Just (UN n')) ty' scr + pure $ IPi fc c p (Just un') ty' scr else do scr <- renameIBinds rs us sc ty' <- renameIBinds rs us ty - pure $ IPi fc c p (Just (UN n)) ty' scr + pure $ IPi fc c p (Just un) ty' scr renameIBinds rs us (IPi fc c p n ty sc) = pure $ IPi fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc) renameIBinds rs us (ILam fc c p n ty sc) @@ -73,18 +74,18 @@ renameIBinds rs us tm = pure $ tm export doBind : List (String, String) -> RawImp -> RawImp doBind [] tm = tm -doBind ns (IVar fc (UN n)) - = maybe (IVar fc (UN n)) - (\n' => IBindVar fc n') +doBind ns (IVar fc nm@(UN (Basic n))) + = maybe (IVar fc nm) + (IBindVar fc) (lookup n ns) doBind ns (IPi fc rig p mn aty retty) = let ns' = case mn of - Just (UN n) => filter (\x => fst x /= n) ns + Just (UN (Basic n)) => filter (\x => fst x /= n) ns _ => ns in IPi fc rig p mn (doBind ns' aty) (doBind ns' retty) doBind ns (ILam fc rig p mn aty sc) = let ns' = case mn of - Just (UN n) => filter (\x => fst x /= n) ns + Just (UN (Basic n)) => filter (\x => fst x /= n) ns _ => ns in ILam fc rig p mn (doBind ns' aty) (doBind ns' sc) doBind ns (IApp fc fn av) @@ -120,7 +121,7 @@ bindNames arg tm = if !isUnboundImplicits then do let ns = nub (findBindableNames arg [] [] tm) log "elab.bindnames" 10 $ "Found names :" ++ show ns - pure (map UN (map snd ns), doBind ns tm) + pure (map (UN . Basic) (map snd ns), doBind ns tm) else pure ([], tm) -- if the name is part of the using decls, add the relevant binder for it: @@ -190,4 +191,5 @@ piBindNames loc env tm piBind : List String -> RawImp -> RawImp piBind [] ty = ty piBind (n :: ns) ty - = IPi loc erased Implicit (Just (UN n)) (Implicit loc False) (piBind ns ty) + = IPi loc erased Implicit (Just (UN $ Basic n)) (Implicit loc False) + $ piBind ns ty diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 0098825b8..71a898bc2 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -18,7 +18,7 @@ import TTImp.TTImp import Data.List import Data.String -import Libraries.Data.StringMap +import Libraries.Data.UserNameMap %default covering @@ -31,7 +31,7 @@ expandAmbigName : {vars : _} -> RawImp -> Maybe (Glued vars) -> Core RawImp expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp = do est <- get EST - if UN n `elem` lhsPatVars est + if UN (Basic n) `elem` lhsPatVars est then pure $ IMustUnify fc NonLinearVar orig else pure $ orig expandAmbigName mode nest env orig args (IVar fc x) exp @@ -68,7 +68,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp (uniqType primNs x args) (map (mkAlt primApp est) nalts) where - lookupUN : Maybe String -> StringMap a -> Maybe a + lookupUN : Maybe UserName -> UserNameMap a -> Maybe a lookupUN Nothing _ = Nothing lookupUN (Just n) sm = lookup n sm diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index a61044a1b..e4a6abc8c 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -536,14 +536,14 @@ mutual export findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp - findBindAllExpPattern = lookup (UN "_") + findBindAllExpPattern = lookup (UN Underscore) isImplicitAs : RawImp -> Bool isImplicitAs (IAs _ _ UseLeft _ (Implicit _ _)) = True isImplicitAs _ = False isBindAllExpPattern : Name -> Bool - isBindAllExpPattern (UN "_") = True + isBindAllExpPattern (UN Underscore) = True isBindAllExpPattern _ = False -- Check an application of 'fntm', with type 'fnty' to the given list @@ -598,7 +598,7 @@ mutual then -- We are done checkExp rig elabinfo env fc tm (glueBack defs env ty) expty else -- Some user defined binding is present while we are out of explicit arguments, that's an error - throw (InvalidArgs fc env (map (const (UN "")) autoargs ++ map fst namedargs) tm) + throw (InvalidArgs fc env (map (const (UN $ Basic "")) autoargs ++ map fst namedargs) tm) -- Function type is delayed, so force the term and continue checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs autoargs namedargs kr expty = checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty @@ -710,7 +710,7 @@ mutual = do defs <- get Ctxt if all isImplicitAs (autoargs ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs)) then checkExp rig elabinfo env fc tm (glueBack defs env ty) expty - else throw (InvalidArgs fc env (map (const (UN "")) autoargs ++ map fst namedargs) tm) + else throw (InvalidArgs fc env (map (const (UN $ Basic "")) autoargs ++ map fst namedargs) tm) ||| Entrypoint for checkAppWith: run the elaboration first and, if we're ||| on the LHS and the result is an under-applied constructor then insist diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 8c717f005..987eafb6b 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -288,7 +288,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected -- so that it applies to the right original variable getBindName : Int -> Name -> List Name -> (Name, Name) getBindName idx n@(UN un) vs - = if n `elem` vs then (n, MN un idx) else (n, n) + = if n `elem` vs then (n, MN (displayUserName un) idx) else (n, n) getBindName idx n vs = if n `elem` vs then (n, MN "_cn" idx) else (n, n) @@ -327,7 +327,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected -- Names used in the pattern we're matching on, so don't bind them -- in the generated case block usedIn : RawImp -> List Name - usedIn (IBindVar _ n) = [UN n] + usedIn (IBindVar _ n) = [UN $ Basic n] usedIn (IApp _ f a) = usedIn f ++ usedIn a usedIn (IAs _ _ _ n a) = n :: usedIn a usedIn (IAlternative _ _ alts) = concatMap usedIn alts diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 281061fd1..5e997f5fa 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -20,7 +20,7 @@ import Data.Either import Libraries.Data.IntMap import Data.List import Libraries.Data.NameMap -import Libraries.Data.StringMap +import Libraries.Data.UserNameMap %default covering @@ -143,7 +143,7 @@ record EState (vars : List Name) where linearUsed : List (Var vars) saveHoles : NameMap () -- things we'll need to save to TTC, even if solved - unambiguousNames : StringMap (Name, Int, GlobalDef) + unambiguousNames : UserNameMap (Name, Int, GlobalDef) -- Mapping from userNameRoot to fully resolved names. -- For names in this mapping, we don't run disambiguation. -- Used in with-expressions. @@ -547,7 +547,7 @@ successful allowCons ((tm, elab) :: elabs) defs <- branch catch (do -- Run the elaborator logC "elab" 5 $ - do tm' <- maybe (pure (UN "__")) + do tm' <- maybe (pure (UN $ Basic "__")) toFullNames tm pure ("Running " ++ show tm') res <- elab @@ -567,7 +567,7 @@ successful allowCons ((tm, elab) :: elabs) put MD md put Ctxt defs logC "elab" 5 $ - do tm' <- maybe (pure (UN "__")) + do tm' <- maybe (pure (UN $ Basic "__")) toFullNames tm pure ("Success " ++ show tm' ++ " (" ++ show ncons' ++ " - " diff --git a/src/TTImp/Elab/Hole.idr b/src/TTImp/Elab/Hole.idr index 693e897ec..b6320fdbe 100644 --- a/src/TTImp/Elab/Hole.idr +++ b/src/TTImp/Elab/Hole.idr @@ -35,7 +35,7 @@ checkHole : {vars : _} -> {auto e : Ref EST (EState vars)} -> RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> - FC -> String -> Maybe (Glued vars) -> + FC -> UserName -> Maybe (Glued vars) -> Core (Term vars, Glued vars) checkHole rig elabinfo nest env fc n_in (Just gexpty) = do nm <- inCurrentNS (UN n_in) @@ -58,7 +58,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty) saveHole nm pure (metaval, gexpty) checkHole rig elabinfo nest env fc n_in exp - = do nmty <- genName ("type_of_" ++ n_in) + = do nmty <- genName ("type_of_" ++ show n_in) let env' = letToLam env ty <- metaVar fc erased env' nmty (TType fc) nm <- inCurrentNS (UN n_in) diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr index cf4d22761..1cfe09ae6 100644 --- a/src/TTImp/Elab/ImplicitBind.idr +++ b/src/TTImp/Elab/ImplicitBind.idr @@ -401,7 +401,7 @@ checkBindVar : {vars : _} -> {auto e : Ref EST (EState vars)} -> RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> - FC -> String -> -- string is base of the pattern name + FC -> UserName -> -- username is base of the pattern name Maybe (Glued vars) -> Core (Term vars, Glued vars) checkBindVar rig elabinfo nest env fc str topexp diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index 439f8c3ac..f8a5e0197 100644 --- a/src/TTImp/Elab/Record.idr +++ b/src/TTImp/Elab/Record.idr @@ -44,7 +44,7 @@ applyImp f ((Just n, arg) :: xs) toLHS' : FC -> Rec -> (Maybe Name, RawImp) toLHS' loc (Field mn@(Just _) n _) - = (mn, IAs loc EmptyFC UseRight (UN n) (Implicit loc True)) + = (mn, IAs loc EmptyFC UseRight (UN $ Basic n) (Implicit loc True)) toLHS' loc (Field mn n _) = (mn, IBindVar EmptyFC n) toLHS' loc (Constr mn con args) = let args' = map (toLHS' loc . snd) args in @@ -129,7 +129,7 @@ findPath loc (p :: ps) full (Just tyn) val (Field mn n v) = do fldn <- genFieldName p args' <- mkArgs ps -- If it's an implicit argument, leave it as _ by default - let arg = maybe (IVar EmptyFC (UN fldn)) + let arg = maybe (IVar EmptyFC (UN $ Basic fldn)) (const (Implicit loc False)) imp pure ((p, Field imp fldn arg) :: args') @@ -154,7 +154,8 @@ getSides loc (ISetField path val) tyn orig rec -- then set the path on the rhs to 'val' = findPath loc path path (Just tyn) (const val) rec getSides loc (ISetFieldApp path val) tyn orig rec - = findPath loc path path (Just tyn) (\n => apply val [IVar EmptyFC (UN n)]) rec + = findPath loc path path (Just tyn) + (\n => apply val [IVar EmptyFC (UN $ Basic n)]) rec getAllSides : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -184,7 +185,7 @@ recUpdate rigc elabinfo iloc nest env flds rec grecty | Nothing => throw (RecordTypeNeeded iloc env) fldn <- genFieldName "__fld" sides <- getAllSides iloc flds rectyn rec - (Field Nothing fldn (IVar vloc (UN fldn))) + (Field Nothing fldn (IVar vloc (UN $ Basic fldn))) pure $ ICase vloc rec (Implicit vloc False) [mkClause sides] where vloc : FC diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 6b6f125a3..b494a6627 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -35,7 +35,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp = do defs <- get Ctxt fnm <- toFullNames nm case fnm of - NS ns (UN n) + NS ns (UN (Basic n)) => if ns == reflectionNS then elabCon defs n (map snd args) else failWith defs $ "bad reflection namespace " ++ show ns @@ -90,7 +90,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp elabCon defs "Check" [exp, ttimp] = do exp' <- evalClosure defs exp ttimp' <- evalClosure defs ttimp - tidx <- resolveName (UN "[elaborator script]") + tidx <- resolveName (UN $ Basic "[elaborator script]") e <- newRef EST (initEState tidx env) (checktm, _) <- runDelays (const True) $ check top (initElabInfo InExpr) nest env !(reify defs ttimp') @@ -190,7 +190,7 @@ checkRunElab rig elabinfo nest env fc script exp defs <- get Ctxt unless (isExtension ElabReflection defs) $ throw (GenericMsg fc "%language ElabReflection not enabled") - let n = NS reflectionNS (UN "Elab") + let n = NS reflectionNS (UN $ Basic "Elab") let ttn = reflectiontt "TT" elabtt <- appCon fc defs n [expected] (stm, sty) <- runDelays (const True) $ diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index e5529d8b8..e562671ac 100644 --- a/src/TTImp/Elab/Term.idr +++ b/src/TTImp/Elab/Term.idr @@ -1,6 +1,6 @@ module TTImp.Elab.Term -import Libraries.Data.StringMap +import Libraries.Data.UserNameMap import Core.Context import Core.Core @@ -133,7 +133,7 @@ checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp AutoImplicit => genVarName "conArg" (DefImplicit _) => genVarName "defArg" checkPi rig elabinfo nest env fc r p n argTy retTy exp -checkTerm rig elabinfo nest env (IPi fc r p (Just (UN "_")) argTy retTy) exp +checkTerm rig elabinfo nest env (IPi fc r p (Just (UN Underscore)) argTy retTy) exp = checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp checkTerm rig elabinfo nest env (IPi fc r p (Just n) argTy retTy) exp = checkPi rig elabinfo nest env fc r p n argTy retTy exp @@ -182,7 +182,7 @@ checkTerm rig elabinfo nest env (ICoerced fc tm) exp checkTerm rig elabinfo nest env (IBindHere fc binder sc) exp = checkBindHere rig elabinfo nest env fc binder sc exp checkTerm rig elabinfo nest env (IBindVar fc n) exp - = checkBindVar rig elabinfo nest env fc n exp + = checkBindVar rig elabinfo nest env fc (Basic n) exp checkTerm rig elabinfo nest env (IAs fc nameFC side n_in tm) exp = checkAs rig elabinfo nest env fc nameFC side n_in tm exp checkTerm rig elabinfo nest env (IMustUnify fc reason tm) exp @@ -210,7 +210,7 @@ checkTerm rig elabinfo nest env (IType fc) exp = checkExp rig elabinfo env fc (TType fc) (gType fc) exp checkTerm rig elabinfo nest env (IHole fc str) exp - = checkHole rig elabinfo nest env fc str exp + = checkHole rig elabinfo nest env fc (Basic str) exp checkTerm rig elabinfo nest env (IUnifyLog fc lvl tm) exp = withLogLevel lvl $ check rig elabinfo nest env tm exp checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty) @@ -249,7 +249,7 @@ checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp pure result where - resolveNames : FC -> List Name -> Core (StringMap (Name, Int, GlobalDef)) + resolveNames : FC -> List Name -> Core (UserNameMap (Name, Int, GlobalDef)) resolveNames fc [] = pure empty resolveNames fc (n :: ns) = case userNameRoot n of diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index 587ef3acf..84395c00f 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -122,7 +122,7 @@ unique : List String -> List String -> Int -> List Name -> String unique [] supply suff usedns = unique supply supply (suff + 1) usedns unique (str :: next) supply suff usedns = let var = mkVarN str suff in - if UN var `elem` usedns + if UN (Basic var) `elem` usedns then unique next supply suff usedns else var where @@ -154,7 +154,7 @@ getArgName defs x bound allvars ty else lookupName n ts notBound : String -> Bool - notBound x = not $ UN x `elem` bound + notBound x = not $ UN (Basic x) `elem` bound findNames : NF vars -> Core (List String) findNames (NBind _ x (Pi _ _ _ _) _) @@ -166,7 +166,7 @@ getArgName defs x bound allvars ty findNames ty = pure (filter notBound defaultNames) getName : Name -> List String -> List Name -> String - getName (UN n) defs used = unique (n :: defs) (n :: defs) 0 used + getName (UN (Basic n)) defs used = unique (n :: defs) (n :: defs) 0 used getName _ defs used = unique defs defs 0 used export @@ -179,7 +179,7 @@ getArgNames defs bound allvars env (NBind fc x (Pi _ _ p ty) sc) Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))] _ => pure [] sc' <- sc defs (toClosure defaultOpts env (Erased fc False)) - pure $ ns ++ !(getArgNames defs bound (map UN ns ++ allvars) env sc') + pure $ ns ++ !(getArgNames defs bound (map (UN . Basic) ns ++ allvars) env sc') getArgNames defs bound allvars env val = pure [] export diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 8db591df8..13f72e8e2 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -364,7 +364,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty all (\r => nameRoot (recname r) ++ "_rhs") (recData opts) hn <- uniqueName defs (map nameRoot vars) base - (idx, tm) <- newMeta fc rig env (UN hn) ty + (idx, tm) <- newMeta fc rig env (UN $ Basic hn) ty (Hole (length env) (holeInit False)) False one (tm, []) @@ -739,7 +739,7 @@ searchType {vars} fc rig opts env topty Z (Bind bfc n b@(Pi fc' c info ty) sc) getSuccessful fc rig opts False env ty topty [searchLocal fc rig opts env (Bind bfc n b sc) topty, (do defs <- get Ctxt - let n' = UN !(getArgName defs n [] vars !(nf defs env ty)) + let n' = UN $ Basic !(getArgName defs n [] vars !(nf defs env ty)) let env' : Env Term (n' :: _) = b :: env let sc' = renameTop n' sc log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc' diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index 492d1aace..dfad2f792 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -28,7 +28,7 @@ import Data.List %default covering fnName : Bool -> Name -> String -fnName lhs (UN n) +fnName lhs (UN (Basic n)) = if isIdentNormal n then n else if lhs then "(" ++ n ++ ")" else "op" @@ -89,7 +89,7 @@ expandClause loc opts n c splittableNames : RawImp -> List Name splittableNames (IApp _ f (IBindVar _ n)) - = splittableNames f ++ [UN n] + = splittableNames f ++ [UN $ Basic n] splittableNames (IApp _ f _) = splittableNames f splittableNames (IAutoApp _ f _) @@ -114,7 +114,7 @@ trySplit loc lhsraw lhs rhs n valid _ = Nothing fixNames : RawImp -> RawImp - fixNames (IVar loc' (UN n)) = IBindVar loc' n + fixNames (IVar loc' (UN (Basic n))) = IBindVar loc' n fixNames (IVar loc' (MN _ _)) = Implicit loc' True fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a) fixNames (IAutoApp loc' f a) = IAutoApp loc' (fixNames f) (fixNames a) @@ -127,7 +127,7 @@ trySplit loc lhsraw lhs rhs n Nothing => IVar loc' n Just tm => fixNames tm updateLHS ups (IBindVar loc' n) - = case lookup (UN n) ups of + = case lookup (UN (Basic n)) ups of Nothing => IBindVar loc' n Just tm => fixNames tm updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a) diff --git a/src/TTImp/Interactive/MakeLemma.idr b/src/TTImp/Interactive/MakeLemma.idr index fadf454f9..023475619 100644 --- a/src/TTImp/Interactive/MakeLemma.idr +++ b/src/TTImp/Interactive/MakeLemma.idr @@ -47,7 +47,7 @@ getArgs : {vars : _} -> getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc) = do defs <- get Ctxt ty' <- map (map rawName) $ unelab env !(normalise defs env ty) - let x' = UN !(uniqueName defs (map nameRoot vars) (nameRoot x)) + let x' = UN $ Basic !(uniqueName defs (map nameRoot vars) (nameRoot x)) (sc', ty) <- getArgs (b :: env) k (renameTop x' sc) -- Don't need to use the name if it's not used in the scope type let mn = if c == top diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 18afa1f32..dfe6890da 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -180,15 +180,15 @@ mutual implicitArg fname indents = do start <- location symbol "{" - x <- unqualifiedName + x <- UN . Basic <$> unqualifiedName (do symbol "=" commit tm <- expr fname indents symbol "}" - pure (Just (UN x), tm)) + pure (Just x, tm)) <|> (do symbol "}" end <- location - pure (Just (UN x), IVar (MkFC fname start end) (UN x))) + pure (Just x, IVar (MkFC fname start end) x)) <|> do symbol "@{" commit tm <- expr fname indents @@ -198,12 +198,12 @@ mutual as : OriginDesc -> IndentInfo -> Rule RawImp as fname indents = do start <- location - x <- unqualifiedName + x <- UN . Basic <$> unqualifiedName nameEnd <- location symbol "@" pat <- simpleExpr fname indents end <- location - pure (IAs (MkFC fname start end) (MkFC fname start nameEnd) UseRight (UN x) pat) + pure (IAs (MkFC fname start end) (MkFC fname start nameEnd) UseRight x pat) simpleExpr : OriginDesc -> IndentInfo -> Rule RawImp simpleExpr fname indents @@ -247,7 +247,7 @@ mutual (do symbol ":" appExpr fname indents) rig <- getMult rigc - pure (rig, UN n, ty)) + pure (rig, UN (Basic n), ty)) pibindListName : OriginDesc -> FilePos -> IndentInfo -> @@ -259,7 +259,7 @@ mutual ty <- expr fname indents atEnd indents rig <- getMult rigc - pure (map (\n => (rig, UN n, ty)) (forget ns)) + pure (map (\n => (rig, UN (Basic n), ty)) (forget ns)) <|> forget <$> sepBy1 (symbol ",") (do rigc <- multiplicity n <- name @@ -297,7 +297,10 @@ mutual ns <- sepBy1 (symbol ",") unqualifiedName nend <- location let nfc = MkFC fname nstart nend - let binders = map (\n => (erased {a=RigCount}, Just (UN n), Implicit nfc False)) (forget ns) + let binders = map (\n => ( erased {a=RigCount} + , Just (UN $ Basic n) + , Implicit nfc False)) + (forget ns) symbol "." scope <- typeExpr fname indents end <- location @@ -628,7 +631,7 @@ fieldDecl fname indents ty <- expr fname indents end <- location pure (map (\n => MkIField (MkFC fname start end) - linear p (UN n) ty) (forget ns)) + linear p (UN $ Basic n) ty) (forget ns)) recordDecl : OriginDesc -> IndentInfo -> Rule ImpDecl recordDecl fname indents diff --git a/src/TTImp/PartialEval.idr b/src/TTImp/PartialEval.idr index 56c84f0fc..891139d16 100644 --- a/src/TTImp/PartialEval.idr +++ b/src/TTImp/PartialEval.idr @@ -142,11 +142,11 @@ getSpecPats fc pename fn stk fnty args sargs pats mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app (a :: as) ((_, Dynamic) :: ds) = do defs <- get Ctxt sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) - mkRHSargs sc' (IApp fc app (IVar fc (UN a))) as ds + mkRHSargs sc' (IApp fc app (IVar fc (UN $ Basic a))) as ds mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app (a :: as) ((_, Dynamic) :: ds) = do defs <- get Ctxt sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) - mkRHSargs sc' (INamedApp fc app x (IVar fc (UN a))) as ds + mkRHSargs sc' (INamedApp fc app x (IVar fc (UN $ Basic a))) as ds mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app as ((_, Static tm) :: ds) = do defs <- get Ctxt sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) @@ -160,7 +160,7 @@ getSpecPats fc pename fn stk fnty args sargs pats -- Type will depend on the value here (we assume a variadic function) but -- the argument names are still needed mkRHSargs ty app (a :: as) ((_, Dynamic) :: ds) - = mkRHSargs ty (IApp fc app (IVar fc (UN a))) as ds + = mkRHSargs ty (IApp fc app (IVar fc (UN $ Basic a))) as ds mkRHSargs _ app _ _ = pure app @@ -293,7 +293,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk getAllRefs : NameMap Bool -> List ArgMode -> NameMap Bool getAllRefs ns (Dynamic :: xs) = getAllRefs ns xs getAllRefs ns (Static t :: xs) - = addRefs False (UN "_") (getAllRefs ns xs) t + = addRefs False (UN Underscore) (getAllRefs ns xs) t getAllRefs ns [] = ns updateApp : Name -> RawImp -> RawImp @@ -364,7 +364,7 @@ specialise {vars} fc env gdef fn stk let nhash = hash (mapMaybe getStatic (map snd sargs)) `hashWithSalt` fn -- add function name to hash to avoid namespace clashes let pename = NS partialEvalNS - (UN ("PE_" ++ nameRoot fnfull ++ "_" ++ asHex nhash)) + (UN $ Basic ("PE_" ++ nameRoot fnfull ++ "_" ++ asHex nhash)) defs <- get Ctxt case lookup pename (peFailures defs) of Nothing => Just <$> mkSpecDef fc gdef pename sargs fn stk diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 09b97f544..9645dffcc 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -589,8 +589,8 @@ checkClause {vars} mult vis totreq hashit n opts nest env Nothing => [] Just _ => let fc = emptyFC in - let refl = IVar fc (NS builtinNS (UN "Refl")) in - [(mprf, INamedApp fc refl (UN "x") wval_raw)] + let refl = IVar fc (NS builtinNS (UN $ Basic "Refl")) in + [(mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)] let rhs_in = gapply (IVar vfc wname) $ map (\ nm => (Nothing, IVar vfc nm)) envns @@ -650,7 +650,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env bindWithArgs {xs} wvalTy (Just (name, wval)) wvalEnv = do defs <- get Ctxt - let eqName = NS builtinNS (UN "Equal") + let eqName = NS builtinNS (UN $ Basic "Equal") Just (TCon t ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs) | _ => throw (InternalError "Cannot find builtin Equal") let eqTyCon = Ref vfc (TyCon t ar) !(toResolvedNames eqName) @@ -830,7 +830,7 @@ mkRunTime fc n mkCrash : {vars : _} -> String -> Term vars mkCrash msg - = apply fc (Ref fc Func (NS builtinNS (UN "idris_crash"))) + = apply fc (Ref fc Func (NS builtinNS (UN $ Basic "idris_crash"))) [Erased fc False, PrimVal fc (Str msg)] matchAny : Term vars -> Term vars @@ -954,7 +954,7 @@ processDef opts nest env fc n_in cs_in defs <- get Ctxt put Ctxt (record { toCompileCase $= (n ::) } defs) - atotal <- toResolvedNames (NS builtinNS (UN "assert_total")) + atotal <- toResolvedNames (NS builtinNS (UN $ Basic "assert_total")) when (not (InCase `elem` opts)) $ do calcRefs False atotal (Resolved nidx) sc <- calculateSizeChange fc n diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 8b0a03208..1644ec23e 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -136,8 +136,8 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields upds (b :: tyenv) sc else do let fldNameStr = nameRoot n - rfNameNS <- inCurrentNS (RF fldNameStr) - unNameNS <- inCurrentNS (UN fldNameStr) + rfNameNS <- inCurrentNS (UN $ Field fldNameStr) + unNameNS <- inCurrentNS (UN $ Basic fldNameStr) let nestDrop = map (\ (n, (_, ns, _)) => (n, length ns)) @@ -173,9 +173,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields let lhs = IApp bfc (IVar bfc rfNameNS) (if imp == Explicit then lhs_exp - else INamedApp bfc lhs_exp (UN fldNameStr) + else INamedApp bfc lhs_exp (UN $ Basic fldNameStr) (IBindVar bfc fldNameStr)) - let rhs = IVar EmptyFC (UN fldNameStr) + let rhs = IVar EmptyFC (UN $ Basic fldNameStr) log "declare.record.projection" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs processDecl [] nest env (IDef bfc rfNameNS [PatClause bfc lhs rhs]) diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr index bdf8cb096..072164446 100644 --- a/src/TTImp/ProcessRunElab.idr +++ b/src/TTImp/ProcessRunElab.idr @@ -28,8 +28,8 @@ processRunElab eopts nest env fc tm = do defs <- get Ctxt unless (isExtension ElabReflection defs) $ throw (GenericMsg fc "%language ElabReflection not enabled") - tidx <- resolveName (UN "[elaborator script]") - let n = NS reflectionNS (UN "Elab") + tidx <- resolveName (UN $ Basic "[elaborator script]") + let n = NS reflectionNS (UN $ Basic "Elab") unit <- getCon fc defs (builtin "Unit") exp <- appCon fc defs n [unit] diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 065c0e83c..d751a0ec7 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -91,7 +91,7 @@ processFnOpt fc _ ndef (SpecArgs ns) then collectDDeps sc' else do aty <- quote empty [] nty -- Get names depended on by nty - let deps = keys (getRefs (UN "_") aty) + let deps = keys (getRefs (UN Underscore) aty) rest <- collectDDeps sc' pure (rest ++ deps) collectDDeps _ = pure [] @@ -184,7 +184,7 @@ getFnString : {auto c : Ref Ctxt Defs} -> RawImp -> Core String getFnString (IPrimVal _ (Str st)) = pure st getFnString tm - = do inidx <- resolveName (UN "[foreign]") + = do inidx <- resolveName (UN $ Basic "[foreign]") let fc = getFC tm let gstr = gnf [] (PrimVal fc StringType) etm <- checkTerm inidx InExpr [] (MkNested []) [] tm gstr diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index da16f56ad..5c2b68b1b 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -14,12 +14,12 @@ import TTImp.TTImp export Reify BindMode where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "PI"), [(_, c)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "PI"), [(_, c)]) => do c' <- reify defs !(evalClosure defs c) pure (PI c') - (NS _ (UN "PATTERN"), _) => pure PATTERN - (NS _ (UN "NONE"), _) => pure NONE + (UN (Basic "PATTERN"), _) => pure PATTERN + (UN (Basic "NONE"), _) => pure NONE _ => cantReify val "BindMode" reify deva val = cantReify val "BindMode" @@ -36,9 +36,9 @@ Reflect BindMode where export Reify UseSide where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "UseLeft"), _) => pure UseLeft - (NS _ (UN "UseRight"), _) => pure UseRight + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "UseLeft"), _) => pure UseLeft + (UN (Basic "UseRight"), _) => pure UseRight _ => cantReify val "UseSide" reify defs val = cantReify val "UseSide" @@ -52,14 +52,14 @@ Reflect UseSide where export Reify DotReason where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "NonLinearVar"), _) => pure NonLinearVar - (NS _ (UN "VarApplied"), _) => pure VarApplied - (NS _ (UN "NotConstructor"), _) => pure NotConstructor - (NS _ (UN "ErasedArg"), _) => pure ErasedArg - (NS _ (UN "UserDotted"), _) => pure UserDotted - (NS _ (UN "UnknownDot"), _) => pure UnknownDot - (NS _ (UN "UnderAppliedCon"), _) => pure UnderAppliedCon + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "NonLinearVar"), _) => pure NonLinearVar + (UN (Basic "VarApplied"), _) => pure VarApplied + (UN (Basic "NotConstructor"), _) => pure NotConstructor + (UN (Basic "ErasedArg"), _) => pure ErasedArg + (UN (Basic "UserDotted"), _) => pure UserDotted + (UN (Basic "UnknownDot"), _) => pure UnknownDot + (UN (Basic "UnderAppliedCon"), _) => pure UnderAppliedCon _ => cantReify val "DotReason" reify defs val = cantReify val "DotReason" @@ -85,12 +85,12 @@ mutual export Reify RawImp where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "IVar"), [fc, n]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "IVar"), [fc, n]) => do fc' <- reify defs !(evalClosure defs fc) n' <- reify defs !(evalClosure defs n) pure (IVar fc' n') - (NS _ (UN "IPi"), [fc, c, p, mn, aty, rty]) + (UN (Basic "IPi"), [fc, c, p, mn, aty, rty]) => do fc' <- reify defs !(evalClosure defs fc) c' <- reify defs !(evalClosure defs c) p' <- reify defs !(evalClosure defs p) @@ -98,7 +98,7 @@ mutual aty' <- reify defs !(evalClosure defs aty) rty' <- reify defs !(evalClosure defs rty) pure (IPi fc' c' p' mn' aty' rty') - (NS _ (UN "ILam"), [fc, c, p, mn, aty, lty]) + (UN (Basic "ILam"), [fc, c, p, mn, aty, lty]) => do fc' <- reify defs !(evalClosure defs fc) c' <- reify defs !(evalClosure defs c) p' <- reify defs !(evalClosure defs p) @@ -106,7 +106,7 @@ mutual aty' <- reify defs !(evalClosure defs aty) lty' <- reify defs !(evalClosure defs lty) pure (ILam fc' c' p' mn' aty' lty') - (NS _ (UN "ILet"), [fc, lhsFC, c, n, ty, val, sc]) + (UN (Basic "ILet"), [fc, lhsFC, c, n, ty, val, sc]) => do fc' <- reify defs !(evalClosure defs fc) lhsFC' <- reify defs !(evalClosure defs lhsFC) c' <- reify defs !(evalClosure defs c) @@ -115,123 +115,123 @@ mutual val' <- reify defs !(evalClosure defs val) sc' <- reify defs !(evalClosure defs sc) pure (ILet fc' lhsFC' c' n' ty' val' sc') - (NS _ (UN "ICase"), [fc, sc, ty, cs]) + (UN (Basic "ICase"), [fc, sc, ty, cs]) => do fc' <- reify defs !(evalClosure defs fc) sc' <- reify defs !(evalClosure defs sc) ty' <- reify defs !(evalClosure defs ty) cs' <- reify defs !(evalClosure defs cs) pure (ICase fc' sc' ty' cs') - (NS _ (UN "ILocal"), [fc, ds, sc]) + (UN (Basic "ILocal"), [fc, ds, sc]) => do fc' <- reify defs !(evalClosure defs fc) ds' <- reify defs !(evalClosure defs ds) sc' <- reify defs !(evalClosure defs sc) pure (ILocal fc' ds' sc') - (NS _ (UN "IUpdate"), [fc, ds, sc]) + (UN (Basic "IUpdate"), [fc, ds, sc]) => do fc' <- reify defs !(evalClosure defs fc) ds' <- reify defs !(evalClosure defs ds) sc' <- reify defs !(evalClosure defs sc) pure (IUpdate fc' ds' sc') - (NS _ (UN "IApp"), [fc, f, a]) + (UN (Basic "IApp"), [fc, f, a]) => do fc' <- reify defs !(evalClosure defs fc) f' <- reify defs !(evalClosure defs f) a' <- reify defs !(evalClosure defs a) pure (IApp fc' f' a') - (NS _ (UN "INamedApp"), [fc, f, m, a]) + (UN (Basic "INamedApp"), [fc, f, m, a]) => do fc' <- reify defs !(evalClosure defs fc) f' <- reify defs !(evalClosure defs f) m' <- reify defs !(evalClosure defs m) a' <- reify defs !(evalClosure defs a) pure (INamedApp fc' f' m' a') - (NS _ (UN "IAutoApp"), [fc, f, a]) + (UN (Basic "IAutoApp"), [fc, f, a]) => do fc' <- reify defs !(evalClosure defs fc) f' <- reify defs !(evalClosure defs f) a' <- reify defs !(evalClosure defs a) pure (IAutoApp fc' f' a') - (NS _ (UN "IWithApp"), [fc, f, a]) + (UN (Basic "IWithApp"), [fc, f, a]) => do fc' <- reify defs !(evalClosure defs fc) f' <- reify defs !(evalClosure defs f) a' <- reify defs !(evalClosure defs a) pure (IWithApp fc' f' a') - (NS _ (UN "ISearch"), [fc, d]) + (UN (Basic "ISearch"), [fc, d]) => do fc' <- reify defs !(evalClosure defs fc) d' <- reify defs !(evalClosure defs d) pure (ISearch fc' d') - (NS _ (UN "IAlternative"), [fc, t, as]) + (UN (Basic "IAlternative"), [fc, t, as]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) as' <- reify defs !(evalClosure defs as) pure (IAlternative fc' t' as') - (NS _ (UN "IRewrite"), [fc, t, sc]) + (UN (Basic "IRewrite"), [fc, t, sc]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) sc' <- reify defs !(evalClosure defs sc) pure (IRewrite fc' t' sc') - (NS _ (UN "IBindHere"), [fc, t, sc]) + (UN (Basic "IBindHere"), [fc, t, sc]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) sc' <- reify defs !(evalClosure defs sc) pure (IBindHere fc' t' sc') - (NS _ (UN "IBindVar"), [fc, n]) + (UN (Basic "IBindVar"), [fc, n]) => do fc' <- reify defs !(evalClosure defs fc) n' <- reify defs !(evalClosure defs n) pure (IBindVar fc' n') - (NS _ (UN "IAs"), [fc, nameFC, s, n, t]) + (UN (Basic "IAs"), [fc, nameFC, s, n, t]) => do fc' <- reify defs !(evalClosure defs fc) nameFC' <- reify defs !(evalClosure defs nameFC) s' <- reify defs !(evalClosure defs s) n' <- reify defs !(evalClosure defs n) t' <- reify defs !(evalClosure defs t) pure (IAs fc' nameFC' s' n' t') - (NS _ (UN "IMustUnify"), [fc, r, t]) + (UN (Basic "IMustUnify"), [fc, r, t]) => do fc' <- reify defs !(evalClosure defs fc) r' <- reify defs !(evalClosure defs r) t' <- reify defs !(evalClosure defs t) pure (IMustUnify fc' r' t') - (NS _ (UN "IDelayed"), [fc, r, t]) + (UN (Basic "IDelayed"), [fc, r, t]) => do fc' <- reify defs !(evalClosure defs fc) r' <- reify defs !(evalClosure defs r) t' <- reify defs !(evalClosure defs t) pure (IDelayed fc' r' t') - (NS _ (UN "IDelay"), [fc, t]) + (UN (Basic "IDelay"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IDelay fc' t') - (NS _ (UN "IForce"), [fc, t]) + (UN (Basic "IForce"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IForce fc' t') - (NS _ (UN "IQuote"), [fc, t]) + (UN (Basic "IQuote"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IQuote fc' t') - (NS _ (UN "IQuoteName"), [fc, t]) + (UN (Basic "IQuoteName"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IQuoteName fc' t') - (NS _ (UN "IQuoteDecl"), [fc, t]) + (UN (Basic "IQuoteDecl"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IQuoteDecl fc' t') - (NS _ (UN "IUnquote"), [fc, t]) + (UN (Basic "IUnquote"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IUnquote fc' t') - (NS _ (UN "IPrimVal"), [fc, t]) + (UN (Basic "IPrimVal"), [fc, t]) => do fc' <- reify defs !(evalClosure defs fc) t' <- reify defs !(evalClosure defs t) pure (IPrimVal fc' t') - (NS _ (UN "IType"), [fc]) + (UN (Basic "IType"), [fc]) => do fc' <- reify defs !(evalClosure defs fc) pure (IType fc') - (NS _ (UN "IHole"), [fc, n]) + (UN (Basic "IHole"), [fc, n]) => do fc' <- reify defs !(evalClosure defs fc) n' <- reify defs !(evalClosure defs n) pure (IHole fc' n') - (NS _ (UN "Implicit"), [fc, n]) + (UN (Basic "Implicit"), [fc, n]) => do fc' <- reify defs !(evalClosure defs fc) n' <- reify defs !(evalClosure defs n) pure (Implicit fc' n') - (NS _ (UN "IWithUnambigNames"), [fc, ns, t]) + (UN (Basic "IWithUnambigNames"), [fc, ns, t]) => do fc' <- reify defs !(evalClosure defs fc) ns' <- reify defs !(evalClosure defs ns) t' <- reify defs !(evalClosure defs t) @@ -242,12 +242,12 @@ mutual export Reify IFieldUpdate where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "ISetField"), [(_, x), (_, y)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "ISetField"), [(_, x), (_, y)]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) pure (ISetField x' y') - (NS _ (UN "ISetFieldApp"), [(_, x), (_, y)]) + (UN (Basic "ISetFieldApp"), [(_, x), (_, y)]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) pure (ISetFieldApp x' y') @@ -257,12 +257,12 @@ mutual export Reify AltType where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "FirstSuccess"), _) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "FirstSuccess"), _) => pure FirstSuccess - (NS _ (UN "Unique"), _) + (UN (Basic "Unique"), _) => pure Unique - (NS _ (UN "UniqueDefault"), [(_, x)]) + (UN (Basic "UniqueDefault"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (UniqueDefault x') _ => cantReify val "AltType" @@ -271,25 +271,25 @@ mutual export Reify FnOpt where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "Inline"), _) => pure Inline - (NS _ (UN "TCInline"), _) => pure TCInline - (NS _ (UN "Hint"), [(_, x)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "Inline"), _) => pure Inline + (UN (Basic "TCInline"), _) => pure TCInline + (UN (Basic "Hint"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (Hint x') - (NS _ (UN "GlobalHint"), [(_, x)]) + (UN (Basic "GlobalHint"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (GlobalHint x') - (NS _ (UN "ExternFn"), _) => pure ExternFn - (NS _ (UN "ForeignFn"), [(_, x)]) + (UN (Basic "ExternFn"), _) => pure ExternFn + (UN (Basic "ForeignFn"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (ForeignFn x') - (NS _ (UN "Invertible"), _) => pure Invertible - (NS _ (UN "Totality"), [(_, x)]) + (UN (Basic "Invertible"), _) => pure Invertible + (UN (Basic "Totality"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (Totality x') - (NS _ (UN "Macro"), _) => pure Macro - (NS _ (UN "SpecArgs"), [(_, x)]) + (UN (Basic "Macro"), _) => pure Macro + (UN (Basic "SpecArgs"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (SpecArgs x') _ => cantReify val "FnOpt" @@ -298,8 +298,8 @@ mutual export Reify ImpTy where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "MkTy"), [w, x, y, z]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "MkTy"), [w, x, y, z]) => do w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) @@ -311,29 +311,29 @@ mutual export Reify DataOpt where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), args) of - (NS _ (UN "SearchBy"), [(_, x)]) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "SearchBy"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) pure (SearchBy x') - (NS _ (UN "NoHints"), _) => pure NoHints - (NS _ (UN "UniqueSearch"), _) => pure UniqueSearch - (NS _ (UN "External"), _) => pure External - (NS _ (UN "NoNewtype"), _) => pure NoNewtype + (UN (Basic "NoHints"), _) => pure NoHints + (UN (Basic "UniqueSearch"), _) => pure UniqueSearch + (UN (Basic "External"), _) => pure External + (UN (Basic "NoNewtype"), _) => pure NoNewtype _ => cantReify val "DataOpt" reify defs val = cantReify val "DataOpt" export Reify ImpData where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "MkData"), [v,w,x,y,z]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "MkData"), [v,w,x,y,z]) => do v' <- reify defs !(evalClosure defs v) w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (MkImpData v' w' x' y' z') - (NS _ (UN "MkLater"), [x,y,z]) + (UN (Basic "MkLater"), [x,y,z]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) @@ -344,8 +344,8 @@ mutual export Reify IField where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "MkIField"), [v,w,x,y,z]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "MkIField"), [v,w,x,y,z]) => do v' <- reify defs !(evalClosure defs v) w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) @@ -358,8 +358,8 @@ mutual export Reify ImpRecord where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "MkRecord"), [v,w,x,y,z]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "MkRecord"), [v,w,x,y,z]) => do v' <- reify defs !(evalClosure defs v) w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) @@ -372,8 +372,8 @@ mutual export Reify WithFlag where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "Syntactic"), []) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "Syntactic"), []) => pure Syntactic _ => cantReify val "WithFlag" reify defs val = cantReify val "WithFlag" @@ -381,13 +381,13 @@ mutual export Reify ImpClause where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "PatClause"), [x,y,z]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "PatClause"), [x,y,z]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (PatClause x' y' z') - (NS _ (UN "WithClause"), [u,v,w,x,y,z]) + (UN (Basic "WithClause"), [u,v,w,x,y,z]) => do u' <- reify defs !(evalClosure defs u) v' <- reify defs !(evalClosure defs v) w' <- reify defs !(evalClosure defs w) @@ -395,7 +395,7 @@ mutual y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (WithClause u' v' w' x' y' z') - (NS _ (UN "ImpossibleClause"), [x,y]) + (UN (Basic "ImpossibleClause"), [x,y]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) pure (ImpossibleClause x' y') @@ -405,47 +405,47 @@ mutual export Reify ImpDecl where reify defs val@(NDCon _ n _ _ args) - = case (!(full (gamma defs) n), map snd args) of - (NS _ (UN "IClaim"), [v,w,x,y,z]) + = case (dropAllNS !(full (gamma defs) n), map snd args) of + (UN (Basic "IClaim"), [v,w,x,y,z]) => do v' <- reify defs !(evalClosure defs v) w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (IClaim v' w' x' y' z') - (NS _ (UN "IData"), [x,y,z]) + (UN (Basic "IData"), [x,y,z]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (IData x' y' z') - (NS _ (UN "IDef"), [x,y,z]) + (UN (Basic "IDef"), [x,y,z]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (IDef x' y' z') - (NS _ (UN "IParameters"), [x,y,z]) + (UN (Basic "IParameters"), [x,y,z]) => do x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (IParameters x' y' z') - (NS _ (UN "IRecord"), [w, x,y,z]) + (UN (Basic "IRecord"), [w, x,y,z]) => do w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (IRecord w' x' y' z') - (NS _ (UN "INamespace"), [w,x,y]) + (UN (Basic "INamespace"), [w,x,y]) => do w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) pure (INamespace w' x' y') - (NS _ (UN "ITransform"), [w,x,y,z]) + (UN (Basic "ITransform"), [w,x,y,z]) => do w' <- reify defs !(evalClosure defs w) x' <- reify defs !(evalClosure defs x) y' <- reify defs !(evalClosure defs y) z' <- reify defs !(evalClosure defs z) pure (ITransform w' x' y' z') - (NS _ (UN "ILog"), [x]) + (UN (Basic "ILog"), [x]) => do x' <- reify defs !(evalClosure defs x) pure (ILog x') _ => cantReify val "Decl" diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 881236f92..d66b3e5d1 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -500,7 +500,7 @@ findIBinds (INamedApp _ fn _ av) = findIBinds fn ++ findIBinds av findIBinds (IWithApp fc fn av) = findIBinds fn ++ findIBinds av -findIBinds (IAs fc _ _ (UN n) pat) +findIBinds (IAs fc _ _ (UN (Basic n)) pat) = n :: findIBinds pat findIBinds (IAs fc _ _ n pat) = findIBinds pat @@ -522,7 +522,7 @@ findIBinds tm = [] export findImplicits : RawImp' nm -> List String -findImplicits (IPi fc rig p (Just (UN mn)) aty retty) +findImplicits (IPi fc rig p (Just (UN (Basic mn))) aty retty) = mn :: findImplicits aty ++ findImplicits retty findImplicits (IPi fc rig p mn aty retty) = findImplicits aty ++ findImplicits retty @@ -563,7 +563,7 @@ implicitsAs : {auto c : Ref Ctxt Defs} -> implicitsAs n defs ns tm = do let implicits = findIBinds tm log "declare.def.lhs.implicits" 30 $ "Found implicits: " ++ show implicits - setAs (map Just (ns ++ map UN implicits)) [] tm + setAs (map Just (ns ++ map (UN . Basic) implicits)) [] tm where -- Takes the function application expression which is the lhs of a clause -- and decomposes it into the underlying function symbol and the variables @@ -635,7 +635,7 @@ implicitsAs n defs ns tm = do body <- sc defs (toClosure defaultOpts [] (Erased fc False)) case es of -- Explicits were skipped, therefore all explicits are given anyway - Just (UN "_") :: _ => findImps ns es [] body + Just (UN Underscore) :: _ => findImps ns es [] body -- Explicits weren't skipped, so we need to check _ => case updateNs x es of Nothing => pure [] -- explicit wasn't given @@ -659,9 +659,9 @@ implicitsAs n defs ns tm impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp impAs loc' [] tm = tm - impAs loc' ((UN n, AutoImplicit) :: ns) tm + impAs loc' ((nm@(UN (Basic n)), AutoImplicit) :: ns) tm = impAs loc' ns $ - INamedApp loc' tm (UN n) (IBindVar loc' n) + INamedApp loc' tm nm (IBindVar loc' n) impAs loc' ((n, Implicit) :: ns) tm = impAs loc' ns $ @@ -694,7 +694,6 @@ definedInBlock ns decls = UN _ => NS ns n MN _ _ => NS ns n DN _ _ => NS ns n - RF _ => NS ns n _ => n defName : Namespace -> ImpDecl -> List Name @@ -711,7 +710,7 @@ definedInBlock ns decls = fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns toRF : Name -> Name - toRF (UN n) = RF n + toRF (UN (Basic n)) = UN (Field n) toRF n = n fnsUN : List Name diff --git a/src/TTImp/Unelab.idr b/src/TTImp/Unelab.idr index b66cef03e..2c06905c3 100644 --- a/src/TTImp/Unelab.idr +++ b/src/TTImp/Unelab.idr @@ -309,7 +309,7 @@ mutual let nm = if used 0 sctm || isNoSugar umode then Just x else if rig /= top || isDefImp p - then Just (UN "_") + then Just (UN Underscore) else Nothing pure (IPi fc rig p' nm ty' sc, gType fc) where diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index d9259cc7e..83e756941 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -60,8 +60,8 @@ findBindableNames : (arg : Bool) -> List Name -> (used : List String) -> findBindableNamesQuot : List Name -> (used : List String) -> RawImp -> List (String, String) -findBindableNames True env used (IVar fc (UN n)) - = if not (UN n `elem` env) && lowerFirst n +findBindableNames True env used (IVar fc nm@(UN (Basic n))) + = if not (nm `elem` env) && lowerFirst n then [(n, getUnique used n)] else [] findBindableNames arg env used (IPi fc rig p mn aty retty) @@ -84,7 +84,7 @@ findBindableNames arg env used (IAutoApp fc fn av) = findBindableNames False env used fn ++ findBindableNames True env used av findBindableNames arg env used (IWithApp fc fn av) = findBindableNames False env used fn ++ findBindableNames True env used av -findBindableNames arg env used (IAs fc _ _ (UN n) pat) +findBindableNames arg env used (IAs fc _ _ (UN (Basic n)) pat) = (n, getUnique used n) :: findBindableNames arg env used pat findBindableNames arg env used (IAs fc _ _ n pat) = findBindableNames arg env used pat @@ -184,7 +184,7 @@ findUniqueBindableNames fc arg env used t do defs <- get Ctxt let ctxt = gamma defs ns <- map catMaybes $ for assoc $ \ (n, _) => do - ns <- lookupCtxtName (UN n) ctxt + ns <- lookupCtxtName (UN (Basic n)) ctxt let ns = flip mapMaybe ns $ \(n, _, d) => case definition d of -- do not warn about holes: `?a` is not actually @@ -255,7 +255,7 @@ findIBindVars (IAutoApp fc fn av) findIBindVars (IWithApp fc fn av) = findIBindVars fn ++ findIBindVars av findIBindVars (IBindVar fc v) - = [UN v] + = [UN (Basic v)] findIBindVars (IDelayed fc r t) = findIBindVars t findIBindVars (IDelay fc t) @@ -279,8 +279,8 @@ mutual _ => IVar fc n else IVar fc n substNames' True bound ps (IBindVar fc n) - = if not (UN n `elem` bound) - then case lookup (UN n) ps of + = if not (UN (Basic n) `elem` bound) + then case lookup (UN $ Basic n) ps of Just t => t _ => IBindVar fc n else IBindVar fc n @@ -331,13 +331,13 @@ mutual substNamesClause' : Bool -> List Name -> List (Name, RawImp) -> ImpClause -> ImpClause substNamesClause' bvar bound ps (PatClause fc lhs rhs) - = let bound' = map UN (map snd (findBindableNames True bound [] lhs)) + = let bound' = map (UN . Basic) (map snd (findBindableNames True bound [] lhs)) ++ findIBindVars lhs ++ bound in PatClause fc (substNames' bvar [] [] lhs) (substNames' bvar bound' ps rhs) substNamesClause' bvar bound ps (WithClause fc lhs wval prf flags cs) - = let bound' = map UN (map snd (findBindableNames True bound [] lhs)) + = let bound' = map (UN . Basic) (map snd (findBindableNames True bound [] lhs)) ++ findIBindVars lhs ++ bound in WithClause fc (substNames' bvar [] [] lhs) @@ -483,7 +483,7 @@ uniqueName defs used n where usedName : Core Bool usedName - = pure $ case !(lookupTyName (UN n) (gamma defs)) of + = pure $ case !(lookupTyName (UN $ Basic n) (gamma defs)) of [] => n `elem` used _ => True diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr index 818e1941b..a9b5e3131 100644 --- a/src/TTImp/WithClause.idr +++ b/src/TTImp/WithClause.idr @@ -96,10 +96,10 @@ mutual -- one of them is okay getMatch lhs (IAlternative fc _ as) (IAlternative _ _ as') = matchAny fc lhs (zip as as') - getMatch lhs (IAs _ _ _ (UN n) p) (IAs _ fc _ (UN n') p') + getMatch lhs (IAs _ _ _ (UN (Basic n)) p) (IAs _ fc _ (UN (Basic n')) p') = do ms <- getMatch lhs p p' mergeMatches lhs ((n, IBindVar fc n') :: ms) - getMatch lhs (IAs _ _ _ (UN n) p) p' + getMatch lhs (IAs _ _ _ (UN (Basic n)) p) p' = do ms <- getMatch lhs p p' mergeMatches lhs ((n, p') :: ms) getMatch lhs (IAs _ _ _ _ p) p' = getMatch lhs p p' @@ -151,7 +151,7 @@ getArgMatch : FC -> (side : ElabMode) -> (search : Bool) -> (arg : Maybe (PiInfo RawImp, Name)) -> RawImp getArgMatch ploc mode search warg ms Nothing = warg getArgMatch ploc mode True warg ms (Just (AutoImplicit, nm)) - = case (isUN nm >>= \ n => lookup n ms) of + = case (isUN nm >>= \ un => isBasic un >>= \ n => lookup n ms) of Just tm => tm Nothing => let arg = ISearch ploc 500 in @@ -159,7 +159,7 @@ getArgMatch ploc mode True warg ms (Just (AutoImplicit, nm)) then IAs ploc ploc UseLeft nm arg else arg getArgMatch ploc mode search warg ms (Just (_, nm)) - = case (isUN nm >>= \ n => lookup n ms) of + = case (isUN nm >>= \ un => isBasic un >>= \ n => lookup n ms) of Just tm => tm Nothing => let arg = Implicit ploc True in diff --git a/tests/idris2/docs002/expected b/tests/idris2/docs002/expected index a99f4e5a1..5664cccf9 100644 --- a/tests/idris2/docs002/expected +++ b/tests/idris2/docs002/expected @@ -7,6 +7,8 @@ a : SimpleRec -> Int b : SimpleRec -> String hello : Int -> Int world : Nat -> Nat +.a : SimpleRec -> Int +.b : SimpleRec -> String Doc> Doc.NS.NestedNS.Foo : Type A type of Foo @@ -17,6 +19,6 @@ Doc> record Doc.SimpleRec : Type Totality: total Constructor: MkSimpleRec : Int -> String -> SimpleRec Projections: - a : SimpleRec -> Int - b : SimpleRec -> String + .a : SimpleRec -> Int + .b : SimpleRec -> String Doc> Bye for now! diff --git a/tests/idris2/docs003/expected b/tests/idris2/docs003/expected index 2aa8533a0..a4c15b1f2 100644 --- a/tests/idris2/docs003/expected +++ b/tests/idris2/docs003/expected @@ -3,17 +3,17 @@ RecordDoc> RecordDoc> record RecordDoc.A : Type -> Type Totality: total Constructor: __mkA : _ - Projection: anA : A a -> a + Projection: .anA : A a -> a RecordDoc> record RecordDoc.Tuple : Type -> Type -> Type Totality: total Constructor: __mkTuple : _ Projections: - proj1 : Tuple a b -> a - proj2 : Tuple a b -> b + .proj1 : Tuple a b -> a + .proj2 : Tuple a b -> b RecordDoc> record RecordDoc.Singleton : a -> Type Totality: total Constructor: __mkSingleton : _ Projections: - equal : (rec : Singleton v) -> value rec = v - value : Singleton v -> a + .equal : (rec : Singleton v) -> value rec = v + .value : Singleton v -> a RecordDoc> Bye for now! diff --git a/tests/idris2/reflection001/expected b/tests/idris2/reflection001/expected index 9cec0d04d..e31116e6d 100644 --- a/tests/idris2/reflection001/expected +++ b/tests/idris2/reflection001/expected @@ -33,9 +33,9 @@ quote:37:1--37:21 37 | %runElab noExtension ^^^^^^^^^^^^^^^^^^^^ -Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN "+")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (BI 4))) -Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN "+")) (IVar (MkFC (Virtual Interactive) (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC (Virtual Interactive) (0, 14) (0, 19)) (UN "False")) -Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (UN "xfn") (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN "*")) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) IntType)) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994))))) -Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (UN "xfn") (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN "*")) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994))) -Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")] +Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN (Basic "+"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (BI 4))) +Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN (Basic "+"))) (IVar (MkFC (Virtual Interactive) (0, 6) (0, 10)) (UN (Basic "True")))) (IVar (MkFC (Virtual Interactive) (0, 14) (0, 19)) (UN (Basic "False"))) +Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (UN (Basic "xfn")) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN (Basic "xfn"))) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN (Basic "the"))) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) IntType)) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994))))) +Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (UN (Basic "xfn")) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN (Basic "xfn"))) (IPrimVal EmptyFC (I 99994))) +Main> [UN (Basic "names"), NS (MkNS ["Prelude"]) (UN (Basic "+"))] Main> Bye for now! diff --git a/tests/idris2/reflection004/refdecl.idr b/tests/idris2/reflection004/refdecl.idr index c27910a45..2ea8a6481 100644 --- a/tests/idris2/reflection004/refdecl.idr +++ b/tests/idris2/reflection004/refdecl.idr @@ -20,9 +20,10 @@ axes (S (S (S (S (S _))))) {lte} = absurd lte mkPoint : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl mkPoint n = let type = "Point" ++ show n ++ "D" in + let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in IRecord emptyFC Nothing Public - (MkRecord emptyFC (NS (MkNS ["Main"]) (UN type)) [] (NS (MkNS ["Main"]) (UN ("Mk" ++ type))) - (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (RF axis) `(Double)) (axes n))) + (MkRecord emptyFC (mkMainUN type) [] (mkMainUN ("Mk" ++ type)) + (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n))) logDecls : TTImp -> Elab (Int -> Int) logDecls v diff --git a/tests/idris2/reg033/DerivingEq.idr b/tests/idris2/reg033/DerivingEq.idr index 413bd7fb7..9a83569e7 100644 --- a/tests/idris2/reg033/DerivingEq.idr +++ b/tests/idris2/reg033/DerivingEq.idr @@ -21,7 +21,7 @@ genEq typeName = do let and : TTImp -> TTImp -> TTImp and x y = `(~(x) && ~(y)) compareEq : String -> String -> TTImp - compareEq x y = `(~(IVar pos $ UN x) == ~(IVar pos $ UN y)) + compareEq x y = `(~(IVar pos $ UN (Basic x)) == ~(IVar pos $ UN (Basic y))) makeClause : Name -> Elab Clause makeClause constr = do [(_, ty)] <- getType constr