idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Code Issues Projects Releases Wiki Activity

[ refactor ] introduce UserName for (UN/RF) (#1926)

Browse Source 
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.
This commit is contained in:
G. Allais 2021-09-15 13:20:58 +01:00 committed by GitHub
parent 7baf698f66
commit 32e26c5bd1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
78 changed files with 1152 additions and 680 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2api.ipkg
View File

@ -147,6 +147,7 @@ modules =
Libraries.Data.String.Iterator, Libraries.Data.String.Iterator,
Libraries.Data.StringMap, Libraries.Data.StringMap,
Libraries.Data.StringTrie, Libraries.Data.StringTrie,
Libraries.Data.UserNameMap,
Libraries.Data.Version, Libraries.Data.Version,
Libraries.System.Directory.Tree, Libraries.System.Directory.Tree,

20
libs/base/Language/Reflection/TT.idr
View File

@ -97,22 +97,32 @@ data Constant
| WorldType | WorldType
public export 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 | MN String Int -- machine generated name
| NS Namespace Name -- name in a namespace
| DN String Name -- a name and how to display it | DN String Name -- a name and how to display it
| RF String -- record field name
| Nested (Int, Int) Name -- nested function name | Nested (Int, Int) Name -- nested function name
| CaseBlock String Int -- case block nested in (resolved) name | CaseBlock String Int -- case block nested in (resolved) name
| WithBlock String Int -- with 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 export
Show Name where Show Name where
show (NS ns n) = 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 (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (DN str y) = str show (DN str y) = str
show (RF n) = "." ++ n
show (Nested (outer, idx) inner) show (Nested (outer, idx) inner)
= show outer ++ ":" ++ show idx ++ ":" ++ show inner = show outer ++ ":" ++ show idx ++ ":" ++ show inner
show (CaseBlock outer i) = "case block in " ++ show outer show (CaseBlock outer i) = "case block in " ++ show outer

8
src/Compiler/Common.idr
View File

@ -199,10 +199,10 @@ replaceEntry (i, Just (ns, b))
natHackNames : List Name natHackNames : List Name
natHackNames natHackNames
= [UN "prim__add_Integer", = [UN (Basic "prim__add_Integer"),
UN "prim__sub_Integer", UN (Basic "prim__sub_Integer"),
UN "prim__mul_Integer", UN (Basic "prim__mul_Integer"),
NS typesNS (UN "prim__integerToNat")] NS typesNS (UN $ Basic "prim__integerToNat")]
-- Hmm, these dump functions are all very similar aren't they... -- Hmm, these dump functions are all very similar aren't they...
dumpCases : String -> List (Name,FC,NamedDef) -> Core () dumpCases : String -> List (Name,FC,NamedDef) -> Core ()

61
src/Compiler/CompileExpr.idr
View File

@ -181,33 +181,33 @@ magic ms e = go ms e where
%inline %inline
magic__integerToNat : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars magic__integerToNat : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
magic__integerToNat fc fc' [k] 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 -> forall vars. Vect 2 (CExp vars) -> CExp vars
magic__natMinus fc fc' [m,n] magic__natMinus fc fc' [m,n]
= magic__integerToNat fc fc' = 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 -- 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! -- 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 -> forall vars. Vect 1 (CExp vars) -> CExp vars
magic__natUnsuc fc fc' [m] 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 -- TODO: next release remove this and use %builtin pragma
natHack : List Magic natHack : List Magic
natHack = natHack =
[ MagicCRef (NS typesNS (UN "natToInteger")) 1 (\ _, _, [k] => k) [ MagicCRef (NS typesNS (UN $ Basic "natToInteger")) 1 (\ _, _, [k] => k)
, MagicCRef (NS typesNS (UN "integerToNat")) 1 magic__integerToNat , MagicCRef (NS typesNS (UN $ Basic "integerToNat")) 1 magic__integerToNat
, MagicCRef (NS typesNS (UN "plus")) 2 , MagicCRef (NS typesNS (UN $ Basic "plus")) 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n]) (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__add_Integer")) [m, n])
, MagicCRef (NS typesNS (UN "mult")) 2 , MagicCRef (NS typesNS (UN $ Basic "mult")) 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n]) (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__mul_Integer")) [m, n])
, MagicCRef (NS typesNS (UN "minus")) 2 magic__natMinus , MagicCRef (NS typesNS (UN $ Basic "minus")) 2 magic__natMinus
, MagicCRef (NS typesNS (UN "equalNat")) 2 , MagicCRef (NS typesNS (UN $ Basic "equalNat")) 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__eq_Integer")) [m, n]) (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__eq_Integer")) [m, n])
, MagicCRef (NS typesNS (UN "compareNat")) 2 , MagicCRef (NS typesNS (UN $ Basic "compareNat")) 2
(\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN "compareInteger"))) [m, n]) (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN $ Basic "compareInteger"))) [m, n])
] ]
-- get all transformation from %builtin pragmas -- get all transformation from %builtin pragmas
@ -321,8 +321,9 @@ mutual
(CLet fc x True !(toCExp m n val) sc') (CLet fc x True !(toCExp m n val) sc')
rig rig
toCExpTm m n (Bind fc x (Pi _ c e ty) sc) toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
= pure $ CCon fc (UN "->") TYCON Nothing [!(toCExp m n ty), = pure $ CCon fc (UN (Basic "->")) TYCON Nothing
CLam fc x !(toCExp m n sc)] [ !(toCExp m n ty)
, CLam fc x !(toCExp m n sc)]
toCExpTm m n (Bind fc x b tm) = pure $ CErased fc 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... -- We'd expect this to have been dealt with in toCExp, but for completeness...
toCExpTm m n (App fc tm arg) toCExpTm m n (App fc tm arg)
@ -339,9 +340,9 @@ mutual
= let t = constTag c in = let t = constTag c in
if t == 0 if t == 0
then pure $ CPrimVal fc c 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 (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 : _} -> toCExp : {vars : _} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
@ -576,15 +577,15 @@ getFieldArgs defs cl
getNArgs : {auto c : Ref Ctxt Defs} -> getNArgs : {auto c : Ref Ctxt Defs} ->
Defs -> Name -> List (Closure []) -> Core NArgs Defs -> Name -> List (Closure []) -> Core NArgs
getNArgs defs (NS _ (UN "IORes")) [arg] = pure $ NIORes arg getNArgs defs (NS _ (UN $ Basic "IORes")) [arg] = pure $ NIORes arg
getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr getNArgs defs (NS _ (UN $ Basic "Ptr")) [arg] = pure NPtr
getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr getNArgs defs (NS _ (UN $ Basic "AnyPtr")) [] = pure NPtr
getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr getNArgs defs (NS _ (UN $ Basic "GCPtr")) [arg] = pure NGCPtr
getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr getNArgs defs (NS _ (UN $ Basic "GCAnyPtr")) [] = pure NGCPtr
getNArgs defs (NS _ (UN "Buffer")) [] = pure NBuffer getNArgs defs (NS _ (UN $ Basic "Buffer")) [] = pure NBuffer
getNArgs defs (NS _ (UN "ForeignObj")) [] = pure NForeignObj getNArgs defs (NS _ (UN $ Basic "ForeignObj")) [] = pure NForeignObj
getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit
getNArgs defs (NS _ (UN "Struct")) [n, args] getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]
= do NPrimVal _ (Str n') <- evalClosure defs n = do NPrimVal _ (Str n') <- evalClosure defs n
| nf => throw (GenericMsg (getLoc nf) "Unknown name for struct") | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct")
pure (Struct n' !(getFieldArgs defs args)) pure (Struct n' !(getFieldArgs defs args))
@ -641,9 +642,9 @@ nfToCFType _ s (NTCon fc n_in _ _ args)
carg <- nfToCFType fc s narg carg <- nfToCFType fc s narg
pure (CFIORes carg) pure (CFIORes carg)
nfToCFType _ s (NType _) nfToCFType _ s (NType _)
= pure (CFUser (UN "Type") []) = pure (CFUser (UN (Basic "Type")) [])
nfToCFType _ s (NErased _ _) nfToCFType _ s (NErased _ _)
= pure (CFUser (UN "__") []) = pure (CFUser (UN (Basic "__")) [])
nfToCFType fc s t nfToCFType fc s t
= do defs <- get Ctxt = do defs <- get Ctxt
ty <- quote defs [] t ty <- quote defs [] t
@ -766,7 +767,7 @@ compileExp : {auto c : Ref Ctxt Defs} ->
compileExp tm compileExp tm
= do m <- builtinMagic = do m <- builtinMagic
s <- newRef NextSucc 0 s <- newRef NextSucc 0
exp <- toCExp m (UN "main") tm exp <- toCExp m (UN $ Basic "main") tm
pure exp pure exp
||| Given a name, look up an expression, and compile it to a CExp in the environment ||| Given a name, look up an expression, and compile it to a CExp in the environment

51
src/Compiler/ES/Codegen.idr
View File

@ -83,13 +83,17 @@ keywordSafe s = s
-- JS Name -- 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 : Name -> String
jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n 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 (MN n i) = jsIdent n ++ "_" ++ show i
jsName (PV n d) = "pat__" ++ jsName n jsName (PV n d) = "pat__" ++ jsName n
jsName (DN _ n) = 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 (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
jsName (WithBlock x y) = "with__" ++ 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. -- implementations for external primitive functions.
jsPrim : {auto c : Ref ESs ESSt} -> Name -> List Doc -> Core Doc jsPrim : {auto c : Ref ESs ESSt} -> Name -> List Doc -> Core Doc
jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ hcat ["({value:", v, "})"] jsPrim nm docs = case (dropAllNS nm, docs) of
jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ hcat ["(", r, ".value)"] (UN (Basic "prim__newIORef"), [_,v,_]) => pure $ hcat ["({value:", v, "})"]
jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ hcat ["(", r, ".value=", v, ")"] (UN (Basic "prim__readIORef"), [_,r,_]) => pure $ hcat ["(", r, ".value)"]
jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ hcat ["(Array(", s, ").fill(", v, "))"] (UN (Basic "prim__writeIORef"), [_,r,v,_]) => pure $ hcat ["(", r, ".value=", v, ")"]
jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ hcat ["(", x, "[", p, "])"] (UN (Basic "prim__newArray"), [_,s,v,_]) => pure $ hcat ["(Array(", s, ").fill(", v, "))"]
jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ hcat ["(", x, "[", p, "]=", v, ")"] (UN (Basic "prim__arrayGet"), [_,x,p,_]) => pure $ hcat ["(", x, "[", p, "])"]
jsPrim (NS _ (UN "void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" (UN (Basic "prim__arraySet"), [_,x,p,v,_]) => pure $ hcat ["(", x, "[", p, "]=", v, ")"]
jsPrim (NS _ (UN "prim__void")) [_, _] = pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'" (UN (Basic "void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
jsPrim (NS _ (UN "prim__codegen")) [] = do (UN (Basic "prim__void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
(UN (Basic "prim__codegen"), []) => do
(cg :: _) <- ccTypes <$> get ESs (cg :: _) <- ccTypes <$> get ESs
| _ => pure "\"javascript\"" | _ => pure "\"javascript\""
pure . Text $ jsString cg pure . Text $ jsString cg
-- fix #1839: Only support `prim__os` in Node backend but not in browsers -- fix #1839: Only support `prim__os` in Node backend but not in browsers
jsPrim (NS _ (UN "prim__os")) [] = do (UN (Basic "prim__os"), []) => do
tys <- ccTypes <$> get ESs tys <- ccTypes <$> get ESs
case searchForeign tys ["node"] of case searchForeign tys ["node"] of
Right _ => do Right _ => do
addToPreamble "prim__os" $ addToPreamble "prim__os" $
"const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++ "const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++
"(require('os').platform()));" "(require('os').platform()));"
pure $ Text $ esName "sysos" pure $ Text $ esName "sysos"
Left _ => Left _ =>
throw $ InternalError $ "prim not implemented: prim__os" 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 -- Codegen
@ -696,7 +701,7 @@ foreign _ = pure []
-- name of the toplevel tail call loop from the -- name of the toplevel tail call loop from the
-- preamble. -- preamble.
tailRec : Name tailRec : Name
tailRec = UN "__tailRec" tailRec = UN $ Basic "__tailRec"
||| Compiles the given `ClosedTerm` for the list of supported ||| Compiles the given `ClosedTerm` for the list of supported
||| backends to JS code. ||| backends to JS code.

2
src/Compiler/Inline.idr
View File

@ -151,7 +151,7 @@ mutual
-- whether they're safe to inline, but until then this gives such a huge -- 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. -- boost by removing unnecessary lambdas that we'll keep the special case.
eval rec env stk (CRef fc n) 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) => (True, act :: cont :: world :: stk) =>
do xn <- genName "act" do xn <- genName "act"
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world]) sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])

2
src/Compiler/Interpreter/VMCode.idr
View File

@ -120,7 +120,7 @@ callPrim stk fn args = case the (Either Object (Vect ar Constant)) $ traverse ge
getConst o = Left o getConst o = Left o
NS_UN : Namespace -> String -> Name 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 : Ref State InterpState => Stack -> Vect h Object -> Core a
argError stk obj = interpError stk $ "Unexpected arguments: " ++ foldMap ((" " ++) . showType) obj argError stk obj = interpError stk $ "Unexpected arguments: " ++ foldMap ((" " ++) . showType) obj

2
src/Compiler/LambdaLift.idr
View File

@ -148,7 +148,7 @@ genName
where where
mkName : Name -> Int -> Name mkName : Name -> Int -> Name
mkName (NS ns b) i = NS ns (mkName b i) 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 (DN _ n) i = mkName n i
mkName (CaseBlock outer inner) i = MN ("case block in " ++ outer ++ " (" ++ show inner ++ ")") 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 mkName (WithBlock outer inner) i = MN ("with block in " ++ outer ++ " (" ++ show inner ++ ")") i

41
src/Compiler/RefC/RefC.idr
View File

@ -63,14 +63,19 @@ showcCleanString (c ::cs) = (showcCleanStringChar c) . showcCleanString cs
cCleanString : String -> String cCleanString : String -> String
cCleanString cs = showcCleanString (unpack cs) "" cCleanString cs = showcCleanString (unpack cs) ""
export
cUserName : UserName -> String
cUserName (Basic n) = cCleanString n
cUserName (Field n) = "rec__" ++ cCleanString n
cUserName Underscore = cCleanString "_"
export export
cName : Name -> String cName : Name -> String
cName (NS ns n) = cCleanString (showNSWithSep "_" ns) ++ "_" ++ cName n 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 (MN n i) = cCleanString n ++ "_" ++ cCleanString (show i)
cName (PV n d) = "pat__" ++ cName n cName (PV n d) = "pat__" ++ cName n
cName (DN _ n) = cName n cName (DN _ n) = cName n
cName (RF n) = "rec__" ++ cCleanString n
cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y) cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
cName (WithBlock x y) = "with__" ++ 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 ||| Match on a user given name to get the scheme primitive
toPrim : Name -> ExtPrim toPrim : Name -> ExtPrim
toPrim pn@(NS _ n) toPrim pn@(NS _ n)
= cond [(n == UN "prim__newIORef", NewIORef), = cond [(n == UN (Basic "prim__newIORef"), NewIORef),
(n == UN "prim__readIORef", ReadIORef), (n == UN (Basic "prim__readIORef"), ReadIORef),
(n == UN "prim__writeIORef", WriteIORef), (n == UN (Basic "prim__writeIORef"), WriteIORef),
(n == UN "prim__newArray", NewArray), (n == UN (Basic "prim__newArray"), NewArray),
(n == UN "prim__arrayGet", ArrayGet), (n == UN (Basic "prim__arrayGet"), ArrayGet),
(n == UN "prim__arraySet", ArraySet), (n == UN (Basic "prim__arraySet"), ArraySet),
(n == UN "prim__getField", GetField), (n == UN (Basic "prim__getField"), GetField),
(n == UN "prim__setField", SetField), (n == UN (Basic "prim__setField"), SetField),
(n == UN "void", VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
(n == UN "prim__void", VoidElim), (n == UN (Basic "prim__void"), VoidElim),
(n == UN "prim__os", SysOS), (n == UN (Basic "prim__os"), SysOS),
(n == UN "prim__codegen", SysCodegen), (n == UN (Basic "prim__codegen"), SysCodegen),
(n == UN "prim__onCollect", OnCollect), (n == UN (Basic "prim__onCollect"), OnCollect),
(n == UN "prim__onCollectAny", OnCollectAny) (n == UN (Basic "prim__onCollectAny"), OnCollectAny)
] ]
(Unknown pn) (Unknown pn)
toPrim pn = assert_total $ idris_crash ("INTERNAL ERROR: Unknown primitive: " ++ cName 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 else CLangC
let isStandardFFI = Prelude.elem lang ["RefC", "C"] let isStandardFFI = Prelude.elem lang ["RefC", "C"]
let fctName = if isStandardFFI let fctName = if isStandardFFI
then UN fctForeignName then UN $ Basic $ fctForeignName
else UN $ lang ++ "_" ++ fctForeignName else UN $ Basic $ lang ++ "_" ++ fctForeignName
if isStandardFFI if isStandardFFI
then case extLibOpts of then case extLibOpts of
[lib, header] => addHeader header [lib, header] => addHeader header

2
src/Compiler/Scheme/Chez.idr
View File

@ -128,7 +128,7 @@ chezString cs = strCons '"' (showChezString (unpack cs) "\"")
mutual mutual
handleRet : String -> String -> String 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 handleRet _ op = mkWorld op
getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp)) getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))

41
src/Compiler/Scheme/Common.idr
View File

@ -28,15 +28,20 @@ schString s = concatMap okchar (unpack s)
then cast c then cast c
else "C-" ++ show (cast {to=Int} 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 export
schName : Name -> String 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 (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schName n
schName (UN n) = "u--" ++ schString n
schName (MN n i) = schString n ++ "-" ++ show i schName (MN n i) = schString n ++ "-" ++ show i
schName (PV n d) = "pat--" ++ schName n schName (PV n d) = "pat--" ++ schName n
schName (DN _ n) = 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 (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
schName (WithBlock x y) = "with--" ++ 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 ||| Match on a user given name to get the scheme primitive
toPrim : Name -> ExtPrim toPrim : Name -> ExtPrim
toPrim pn@(NS _ n) toPrim pn@(NS _ n)
= cond [(n == UN "prim__newIORef", NewIORef), = cond [(n == UN (Basic "prim__newIORef"), NewIORef),
(n == UN "prim__readIORef", ReadIORef), (n == UN (Basic "prim__readIORef"), ReadIORef),
(n == UN "prim__writeIORef", WriteIORef), (n == UN (Basic "prim__writeIORef"), WriteIORef),
(n == UN "prim__newArray", NewArray), (n == UN (Basic "prim__newArray"), NewArray),
(n == UN "prim__arrayGet", ArrayGet), (n == UN (Basic "prim__arrayGet"), ArrayGet),
(n == UN "prim__arraySet", ArraySet), (n == UN (Basic "prim__arraySet"), ArraySet),
(n == UN "prim__getField", GetField), (n == UN (Basic "prim__getField"), GetField),
(n == UN "prim__setField", SetField), (n == UN (Basic "prim__setField"), SetField),
(n == UN "void", VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
(n == UN "prim__void", VoidElim), (n == UN (Basic "prim__void"), VoidElim),
(n == UN "prim__os", SysOS), (n == UN (Basic "prim__os"), SysOS),
(n == UN "prim__codegen", SysCodegen), (n == UN (Basic "prim__codegen"), SysCodegen),
(n == UN "prim__onCollect", OnCollect), (n == UN (Basic "prim__onCollect"), OnCollect),
(n == UN "prim__onCollectAny", OnCollectAny), (n == UN (Basic "prim__onCollectAny"), OnCollectAny),
(n == UN "prim__makeFuture", MakeFuture) (n == UN (Basic "prim__makeFuture"), MakeFuture)
] ]
(Unknown pn) (Unknown pn)
toPrim pn = Unknown pn toPrim pn = Unknown pn

2
src/Compiler/Scheme/Gambit.idr
View File

@ -75,7 +75,7 @@ gambitString cs = strCons '"' (showGambitString (unpack cs) "\"")
mutual mutual
handleRet : String -> String -> String 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 handleRet _ op = mkWorld op
getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp)) getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))

2
src/Compiler/Scheme/Racket.idr
View File

@ -173,7 +173,7 @@ rktToC CFChar op = "(char->integer " ++ op ++ ")"
rktToC _ op = op rktToC _ op = op
handleRet : CFType -> String -> String 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) handleRet ret op = mkWorld (cToRkt ret op)
cCall : {auto f : Ref Done (List String) } -> cCall : {auto f : Ref Done (List String) } ->

8
src/Core/CaseBuilder.idr
View File

@ -507,7 +507,7 @@ groupCons fc fn pvars cs
-- The type of 'ConGroup' ensures that we refer to the arguments by -- The type of 'ConGroup' ensures that we refer to the arguments by
-- the same name in each of the clauses -- the same name in each of the clauses
addConG {vars'} {todo'} n tag pargs pats pid rhs [] 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))) $ 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 $ NBind fc (MN "_" 1) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NErased fc False)))
(\d, a => pure $ NType fc)) (\d, a => pure $ NType fc))
@ -626,7 +626,7 @@ groupCons fc fn pvars cs
then addConG n 0 pargs pats pid rhs acc then addConG n 0 pargs pats pid rhs acc
else throw (CaseCompile cfc fn (NotFullyApplied n)) else throw (CaseCompile cfc fn (NotFullyApplied n))
addGroup (PArrow _ _ s t) pprf pats pid rhs acc 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 -- Go inside the delay; we'll flag the case as needing to force its
-- scrutinee (need to check in 'caseGroups below) -- scrutinee (need to check in 'caseGroups below)
addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc 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) mkPat args orig (PrimVal fc c)
= pure $ if constTag c == 0 = pure $ if constTag c == 0
then PConst fc c then PConst fc c
else PTyCon fc (UN (show c)) 0 [] else PTyCon fc (UN (Basic $ show c)) 0 []
mkPat args orig (TType fc) = pure $ PTyCon fc (UN "Type") 0 [] mkPat args orig (TType fc) = pure $ PTyCon fc (UN $ Basic "Type") 0 []
mkPat args orig tm mkPat args orig tm
= do log "compile.casetree" 10 $ = do log "compile.casetree" 10 $
"Catchall: marking " ++ show tm ++ " as unmatchable" "Catchall: marking " ++ show tm ++ " as unmatchable"

2
src/Core/CompileExpr.idr
View File

@ -265,7 +265,7 @@ elem n [] = False
elem n (x :: xs) = n == x || elem n xs elem n (x :: xs) = n == x || elem n xs
tryNext : Name -> Name 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 (MN n i) = MN n (1 + i)
tryNext n = MN (nameRoot n) 0 tryNext n = MN (nameRoot n) 0

14
src/Core/Context.idr
View File

@ -22,6 +22,7 @@ import Data.Maybe
import Data.Nat import Data.Nat
import Libraries.Data.NameMap import Libraries.Data.NameMap
import Libraries.Data.StringMap import Libraries.Data.StringMap
import Libraries.Data.UserNameMap
import Libraries.Text.Distance.Levenshtein import Libraries.Text.Distance.Levenshtein
import System import System
@ -73,7 +74,7 @@ initCtxt : Core Context
initCtxt = initCtxtS initSize initCtxt = initCtxtS initSize
addPossible : Name -> Int -> addPossible : Name -> Int ->
StringMap (List PossibleName) -> StringMap (List PossibleName) UserNameMap (List PossibleName) -> UserNameMap (List PossibleName)
addPossible n i ps addPossible n i ps
= case userNameRoot n of = case userNameRoot n of
Nothing => ps Nothing => ps
@ -83,7 +84,7 @@ addPossible n i ps
Just nis => insert nr (Direct n i :: nis) ps Just nis => insert nr (Direct n i :: nis) ps
addAlias : Name -> Name -> Int -> addAlias : Name -> Name -> Int ->
StringMap (List PossibleName) -> StringMap (List PossibleName) UserNameMap (List PossibleName) -> UserNameMap (List PossibleName)
addAlias alias full i ps addAlias alias full i ps
= case userNameRoot alias of = case userNameRoot alias of
Nothing => ps Nothing => ps
@ -819,12 +820,12 @@ getFieldNames ctxt recNS
-- Find similar looking names in the context -- Find similar looking names in the context
export export
getSimilarNames : {auto c : Ref Ctxt Defs} -> Name -> Core (List String) 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 [] Nothing => pure []
Just str => if length str <= 1 then pure [] else Just str => if length str <= 1 then pure [] else
let threshold : Nat := max 1 (assert_total (divNat (length str) 3)) let threshold : Nat := max 1 (assert_total (divNat (length str) 3))
test : Name -> IO (Maybe Nat) := \ nm => do test : Name -> IO (Maybe Nat) := \ nm => do
let (Just str') = userNameRoot nm let (Just str') = show <$> userNameRoot nm
| _ => pure Nothing | _ => pure Nothing
dist <- Levenshtein.compute str str' dist <- Levenshtein.compute str str'
pure (dist <$ guard (dist <= threshold)) 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 : Namespace -> Name -> Visibility -> Bool
reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace
reducibleIn nspace (NS ns (UN n)) Private = 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 reducibleIn nspace n _ = True
export export
@ -1713,9 +1712,6 @@ inCurrentNS n@(MN _ _)
inCurrentNS n@(DN _ _) inCurrentNS n@(DN _ _)
= do defs <- get Ctxt = do defs <- get Ctxt
pure (NS (currentNS defs) n) pure (NS (currentNS defs) n)
inCurrentNS n@(RF _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n = pure n inCurrentNS n = pure n
export export

6
src/Core/Context/Context.idr
View File

@ -18,7 +18,7 @@ import Data.Nat
import Libraries.Data.IntMap import Libraries.Data.IntMap
import Libraries.Data.IOArray import Libraries.Data.IOArray
import Libraries.Data.NameMap import Libraries.Data.NameMap
import Libraries.Data.StringMap import Libraries.Data.UserNameMap
import Libraries.Utils.Binary import Libraries.Utils.Binary
public export public export
@ -357,8 +357,8 @@ record Context where
nextEntry : Int nextEntry : Int
-- Map from full name to its position in the context -- Map from full name to its position in the context
resolvedAs : NameMap Int resolvedAs : NameMap Int
-- Map from strings to all the possible names in all namespaces -- Map from usernames to all the possible names in all namespaces
possibles : StringMap (List PossibleName) possibles : UserNameMap (List PossibleName)
-- Reference to the actual content, indexed by Int -- Reference to the actual content, indexed by Int
content : Ref Arr (IOArray ContextEntry) content : Ref Arr (IOArray ContextEntry)
-- Branching depth, in a backtracking elaborator. 0 is top level; at lower -- Branching depth, in a backtracking elaborator. 0 is top level; at lower

2
src/Core/Env.idr
View File

@ -266,7 +266,7 @@ uniqifyEnv env = uenv [] env
where where
next : Name -> Name next : Name -> Name
next (MN n i) = MN n (i + 1) 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 (NS ns n) = NS ns (next n)
next n = MN (show n) 0 next n = MN (show n) 0

143
src/Core/Name.idr
View File

@ -6,28 +6,44 @@ import Data.Maybe
import Decidable.Equality import Decidable.Equality
import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.String
import public Core.Name.Namespace import public Core.Name.Namespace
%default total %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: ||| Name helps us track a name's structure as well as its origin:
||| was it user-provided or machine-manufactured? For what reason? ||| was it user-provided or machine-manufactured? For what reason?
public export public export
data Name : Type where data Name : Type where
NS : Namespace -> Name -> Name -- in a namespace 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 MN : String -> Int -> Name -- machine generated name
PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
DN : String -> Name -> Name -- a name and how to display it 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 Nested : (Int, Int) -> Name -> Name -- nested function name
CaseBlock : String -> Int -> Name -- case block nested in (resolved) name CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
WithBlock : String -> Int -> Name -- with block nested in (resolved) name WithBlock : String -> Int -> Name -- with block nested in (resolved) name
Resolved : Int -> Name -- resolved, index into context Resolved : Int -> Name -- resolved, index into context
export export
mkNamespacedName : Maybe Namespace -> String -> Name mkNamespacedName : Maybe Namespace -> UserName -> Name
mkNamespacedName Nothing nm = UN nm mkNamespacedName Nothing nm = UN nm
mkNamespacedName (Just ns) nm = NS ns (UN nm) mkNamespacedName (Just ns) nm = NS ns (UN nm)
@ -55,19 +71,24 @@ asName old new (NS ns n)
asName _ _ n = n asName _ _ n = n
export export
userNameRoot : Name -> Maybe String userNameRoot : Name -> Maybe UserName
userNameRoot (NS _ n) = userNameRoot n userNameRoot (NS _ n) = userNameRoot n
userNameRoot (UN n) = Just n userNameRoot (UN n) = Just n
userNameRoot (DN _ n) = userNameRoot n userNameRoot (DN _ n) = userNameRoot n
userNameRoot (RF n) = Just ("." ++ n) -- TMP HACK
userNameRoot _ = Nothing userNameRoot _ = Nothing
export export
isUnderscoreName : Name -> Bool isUnderscoreName : Name -> Bool
isUnderscoreName (UN "_") = True isUnderscoreName (UN Underscore) = True
isUnderscoreName (MN "_" _) = True isUnderscoreName (MN "_" _) = True
isUnderscoreName _ = False isUnderscoreName _ = False
export
isPatternVariable : UserName -> Bool
isPatternVariable (Basic nm) = lowerFirst nm
isPatternVariable (Field _) = False
isPatternVariable Underscore = True
export export
isUserName : Name -> Bool isUserName : Name -> Bool
isUserName (PV _ _) = False isUserName (PV _ _) = False
@ -85,7 +106,6 @@ isSourceName (UN _) = True
isSourceName (MN _ _) = False isSourceName (MN _ _) = False
isSourceName (PV n _) = isSourceName n isSourceName (PV n _) = isSourceName n
isSourceName (DN _ n) = isSourceName n isSourceName (DN _ n) = isSourceName n
isSourceName (RF _) = True
isSourceName (Nested _ n) = isSourceName n isSourceName (Nested _ n) = isSourceName n
isSourceName (CaseBlock _ _) = False isSourceName (CaseBlock _ _) = False
isSourceName (WithBlock _ _) = False isSourceName (WithBlock _ _) = False
@ -94,22 +114,32 @@ isSourceName (Resolved _) = False
export export
isRF : Name -> Maybe (Namespace, String) isRF : Name -> Maybe (Namespace, String)
isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n) isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n)
isRF (RF n) = Just (emptyNS, n) isRF (UN (Field n)) = Just (emptyNS, n)
isRF _ = Nothing isRF _ = Nothing
export export
isUN : Name -> Maybe String isUN : Name -> Maybe UserName
isUN (UN str) = Just str isUN (UN un) = Just un
isUN _ = Nothing 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 export
nameRoot : Name -> String nameRoot : Name -> String
nameRoot (NS _ n) = nameRoot n nameRoot (NS _ n) = nameRoot n
nameRoot (UN n) = n nameRoot (UN n) = displayUserName n
nameRoot (MN n _) = n nameRoot (MN n _) = n
nameRoot (PV n _) = nameRoot n nameRoot (PV n _) = nameRoot n
nameRoot (DN _ n) = nameRoot n nameRoot (DN _ n) = nameRoot n
nameRoot (RF n) = n
nameRoot (Nested _ inner) = nameRoot inner nameRoot (Nested _ inner) = nameRoot inner
nameRoot (CaseBlock n _) = "$" ++ show n nameRoot (CaseBlock n _) = "$" ++ show n
nameRoot (WithBlock n _) = "$" ++ show n nameRoot (WithBlock n _) = "$" ++ show n
@ -118,11 +148,10 @@ nameRoot (Resolved i) = "$" ++ show i
export export
displayName : Name -> (Maybe Namespace, String) displayName : Name -> (Maybe Namespace, String)
displayName (NS ns n) = mapFst (pure . maybe ns (ns <.>)) $ displayName n 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 (MN n _) = (Nothing, n)
displayName (PV n _) = displayName n displayName (PV n _) = displayName n
displayName (DN n _) = (Nothing, n) displayName (DN n _) = (Nothing, n)
displayName (RF n) = (Nothing, n)
displayName (Nested _ n) = displayName n displayName (Nested _ n) = displayName n
displayName (CaseBlock outer _) = (Nothing, "case block in " ++ show outer) displayName (CaseBlock outer _) = (Nothing, "case block in " ++ show outer)
displayName (WithBlock outer _) = (Nothing, "with 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 export
isUnsafeBuiltin : Name -> Bool isUnsafeBuiltin : Name -> Bool
isUnsafeBuiltin nm = case splitNS nm of isUnsafeBuiltin nm = case splitNS nm of
(ns, UN str) => (ns == builtinNS || ns == emptyNS) (ns, UN (Basic str)) =>
&& any {t = List} id (ns == builtinNS || ns == emptyNS)
[ "assert_" `isPrefixOf` str && any {t = List} id
, str `elem` [ "prim__believe_me", "believe_me" [ "assert_" `isPrefixOf` str
, "prim__crash", "idris_crash" , str `elem` [ "prim__believe_me", "believe_me"
] , "prim__crash", "idris_crash"
] ]
]
_ => False _ => False
export
Show UserName where
show (Basic n) = n
show (Field n) = "." ++ n
show Underscore = "_"
export export
Show Name where 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 (NS ns n) = show ns ++ "." ++ show n
show (UN x) = x show (UN x) = show x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}" show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}" show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
show (DN str n) = str show (DN str n) = str
show (RF n) = "." ++ n
show (Nested (outer, idx) inner) show (Nested (outer, idx) inner)
= show outer ++ ":" ++ show idx ++ ":" ++ show inner = show outer ++ ":" ++ show idx ++ ":" ++ show inner
show (CaseBlock outer i) = "case block in " ++ outer show (CaseBlock outer i) = "case block in " ++ outer
show (WithBlock outer i) = "with block in " ++ outer show (WithBlock outer i) = "with block in " ++ outer
show (Resolved x) = "$resolved" ++ show x 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 export
[Raw] Show Name where [Raw] Show Name where
show (NS ns n) = "NS " ++ show ns ++ " (" ++ show n ++ ")" 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 (MN x y) = "MN (" ++ show x ++ ") " ++ show y
show (PV n d) = "PV (" ++ show n ++ ") " ++ show d show (PV n d) = "PV (" ++ show n ++ ") " ++ show d
show (DN str n) = "DN " ++ str ++ " (" ++ show n ++ ")" show (DN str n) = "DN " ++ str ++ " (" ++ show n ++ ")"
show (RF n) = "RF " ++ n
show (Nested ij n) = "Nested " ++ show ij ++ " (" ++ show n ++ ")" show (Nested ij n) = "Nested " ++ show ij ++ " (" ++ show n ++ ")"
show (CaseBlock str i) = "CaseBlock " ++ str ++ " " ++ show i show (CaseBlock str i) = "CaseBlock " ++ str ++ " " ++ show i
show (WithBlock str i) = "CaseBlock " ++ str ++ " " ++ show i show (WithBlock str i) = "CaseBlock " ++ str ++ " " ++ show i
show (Resolved i) = "Resolved " ++ 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 export
Pretty Name where 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 (NS ns n) = pretty ns <+> dot <+> pretty n
pretty (UN x) = pretty x pretty (UN x) = pretty x
pretty (MN x y) = braces (pretty x <+> colon <+> pretty y) pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d) pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
pretty (DN str _) = pretty str pretty (DN str _) = pretty str
pretty (RF n) = "." <+> pretty n
pretty (Nested (outer, idx) inner) pretty (Nested (outer, idx) inner)
= pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner
pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
pretty (Resolved x) = pretty "$resolved" <+> pretty x 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 export
Eq Name where Eq Name where
(==) (NS ns n) (NS ns' n') = n == n' && ns == ns' (==) (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' (==) (MN x y) (MN x' y') = y == y' && x == x'
(==) (PV x y) (PV x' y') = x == x' && y == y' (==) (PV x y) (PV x' y') = x == x' && y == y'
(==) (DN _ n) (DN _ n') = n == n' (==) (DN _ n) (DN _ n') = n == n'
(==) (RF n) (RF n') = n == n'
(==) (Nested x y) (Nested x' y') = x == x' && y == y' (==) (Nested x y) (Nested x' y') = x == x' && y == y'
(==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x' (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
(==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x' (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
(==) (Resolved x) (Resolved x') = x == x' (==) (Resolved x) (Resolved x') = x == x'
(==) _ _ = False (==) _ _ = 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 : Name -> Int
nameTag (NS _ _) = 0 nameTag (NS _ _) = 0
nameTag (UN _) = 1 nameTag (UN _) = 1
nameTag (MN _ _) = 2 nameTag (MN _ _) = 2
nameTag (PV _ _) = 3 nameTag (PV _ _) = 3
nameTag (DN _ _) = 4 nameTag (DN _ _) = 4
nameTag (RF _) = 5
nameTag (Nested _ _) = 6 nameTag (Nested _ _) = 6
nameTag (CaseBlock _ _) = 7 nameTag (CaseBlock _ _) = 7
nameTag (WithBlock _ _) = 8 nameTag (WithBlock _ _) = 8
@ -252,7 +315,6 @@ Ord Name where
GT => GT GT => GT
LT => LT LT => LT
compare (DN _ n) (DN _ n') = compare n n' compare (DN _ n) (DN _ n') = compare n n'
compare (RF n) (RF n') = compare n n'
compare (Nested x y) (Nested x' y') compare (Nested x y) (Nested x' y')
= case compare y y' of = case compare y y' of
EQ => compare x x' EQ => compare x x'
@ -273,6 +335,18 @@ Ord Name where
compare x y = compare (nameTag x) (nameTag y) 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 export
nameEq : (x : Name) -> (y : Name) -> Maybe (x = y) nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)
nameEq (NS xs x) (NS ys y) with (decEq xs ys) 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 x) (NS ys y) | (Yes Refl) | Nothing = Nothing
nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl
nameEq (NS xs x) (NS ys y) | (No contra) = Nothing nameEq (NS xs x) (NS ys y) | (No contra) = Nothing
nameEq (UN x) (UN y) with (decEq x y) nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y)
nameEq (UN y) (UN y) | (Yes Refl) = Just Refl
nameEq (UN x) (UN y) | (No contra) = Nothing
nameEq (MN x t) (MN x' t') with (decEq x x') 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) with (decEq t t')
nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl 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) | (Just Refl) = Just Refl
nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
nameEq (DN x t) (DN y t') | (No p) = 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') with (decEq x x')
nameEq (Nested x y) (Nested x' y') | (No p) = Nothing nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y') nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')

10
src/Core/Normalise/Eval.idr
View File

@ -137,7 +137,7 @@ parameters (defs : Defs, topopts : EvalOpts)
= do tm' <- eval env locs tm [] = do tm' <- eval env locs tm []
case tm' of case tm' of
NDelay fc r _ arg => 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) _ => pure (NForce fc r tm' stk)
eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c
eval env locs (Erased fc i) stk = pure $ NErased fc i 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 [] = do tm' <- applyToStack env cont tm []
case tm' of case tm' of
NDelay fc r _ arg => 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)) _ => pure (NForce fc r tm' (args ++ stk))
applyToStack env cont nf@(NPrimVal fc _) _ = pure nf applyToStack env cont nf@(NPrimVal fc _) _ = pure nf
applyToStack env cont nf@(NErased 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 -- Primitive type matching, in typecase
tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase nm tag args sc) 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 = 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 then evalTree env loc opts fc stk sc
else pure NoMatch else pure NoMatch
_ => pure NoMatch _ => pure NoMatch
-- Type of type matching, in typecase -- 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 = evalTree env loc opts fc stk sc
-- Arrow matching, in typecase -- Arrow matching, in typecase
tryAlt {more} 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] = evalConAlt {more} env loc opts fc stk [s,t]
[aty, [aty,
MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)] MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]

16
src/Core/Primitives.idr
View File

@ -603,17 +603,21 @@ cmpTy t = constTy t t IntType
doubleTy : ClosedTerm doubleTy : ClosedTerm
doubleTy = predTy DoubleType DoubleType 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 : ClosedTerm
believeMeTy believeMeTy
= Bind emptyFC (UN "a") (Pi emptyFC erased Explicit (TType emptyFC)) $ = pi "a" erased Explicit (TType emptyFC) $
Bind emptyFC (UN "b") (Pi emptyFC erased Explicit (TType emptyFC)) $ pi "b" erased Explicit (TType emptyFC) $
Bind emptyFC (UN "x") (Pi emptyFC top Explicit (Local emptyFC Nothing _ (Later First))) $ pi "x" top Explicit (Local emptyFC Nothing _ (Later First)) $
Local emptyFC Nothing _ (Later First) Local emptyFC Nothing _ (Later First)
crashTy : ClosedTerm crashTy : ClosedTerm
crashTy crashTy
= Bind emptyFC (UN "a") (Pi emptyFC erased Explicit (TType emptyFC)) $ = pi "a" erased Explicit (TType emptyFC) $
Bind emptyFC (UN "msg") (Pi emptyFC top Explicit (PrimVal emptyFC StringType)) $ pi "msg" top Explicit (PrimVal emptyFC StringType) $
Local emptyFC Nothing _ (Later First) Local emptyFC Nothing _ (Later First)
castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars) castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
@ -682,7 +686,7 @@ getOp BelieveMe = believeMe
getOp _ = const Nothing getOp _ = const Nothing
prim : String -> Name prim : String -> Name
prim str = UN $ "prim__" ++ str prim str = UN $ Basic $ "prim__" ++ str
export export
opName : {0 arity : Nat} -> PrimFn arity -> Name opName : {0 arity : Nat} -> PrimFn arity -> Name

243
src/Core/Reflect.idr
View File

@ -41,31 +41,31 @@ appCon fc defs n args
export export
preludetypes : String -> Name preludetypes : String -> Name
preludetypes n = NS typesNS (UN n) preludetypes n = NS typesNS (UN $ Basic n)
export export
basics : String -> Name basics : String -> Name
basics n = NS basicsNS (UN n) basics n = NS basicsNS (UN $ Basic n)
export export
builtin : String -> Name builtin : String -> Name
builtin n = NS builtinNS (UN n) builtin n = NS builtinNS (UN $ Basic n)
export export
primio : String -> Name primio : String -> Name
primio n = NS primIONS (UN n) primio n = NS primIONS (UN $ Basic n)
export export
reflection : String -> Name reflection : String -> Name
reflection n = NS reflectionNS (UN n) reflection n = NS reflectionNS (UN $ Basic n)
export export
reflectiontt : String -> Name reflectiontt : String -> Name
reflectiontt n = NS reflectionTTNS (UN n) reflectiontt n = NS reflectionTTNS (UN $ Basic n)
export export
reflectionttimp : String -> Name reflectionttimp : String -> Name
reflectionttimp n = NS reflectionTTImpNS (UN n) reflectionttimp n = NS reflectionTTImpNS (UN $ Basic n)
export export
cantReify : NF vars -> String -> Core a cantReify : NF vars -> String -> Core a
@ -133,9 +133,9 @@ Reflect Double where
export export
Reify Bool where Reify Bool where
reify defs val@(NDCon _ n _ _ _) reify defs val@(NDCon _ n _ _ _)
= case !(full (gamma defs) n) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "True") => pure True UN (Basic "True") => pure True
NS _ (UN "False") => pure False UN (Basic "False") => pure False
_ => cantReify val "Bool" _ => cantReify val "Bool"
reify defs val = cantReify val "Bool" reify defs val = cantReify val "Bool"
@ -147,9 +147,9 @@ Reflect Bool where
export export
Reify Nat where Reify Nat where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "Z"), _) => pure Z (UN (Basic "Z"), _) => pure Z
(NS _ (UN "S"), [(_, k)]) (UN (Basic "S"), [(_, k)])
=> do k' <- reify defs !(evalClosure defs k) => do k' <- reify defs !(evalClosure defs k)
pure (S k') pure (S k')
_ => cantReify val "Nat" _ => cantReify val "Nat"
@ -165,9 +165,9 @@ Reflect Nat where
export export
Reify a => Reify (List a) where Reify a => Reify (List a) where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "Nil"), _) => pure [] (UN (Basic "Nil"), _) => pure []
(NS _ (UN "::"), [_, (_, x), (_, xs)]) (UN (Basic "::"), [_, (_, x), (_, xs)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
xs' <- reify defs !(evalClosure defs xs) xs' <- reify defs !(evalClosure defs xs)
pure (x' :: xs') pure (x' :: xs')
@ -185,8 +185,8 @@ Reflect a => Reflect (List a) where
export export
Reify a => Reify (List1 a) where Reify a => Reify (List1 a) where
reify defs val@(NDCon _ n _ _ [_, (_, x), (_, xs)]) reify defs val@(NDCon _ n _ _ [_, (_, x), (_, xs)])
= case !(full (gamma defs) n) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN ":::") UN (Basic ":::")
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
xs' <- reify defs !(evalClosure defs xs) xs' <- reify defs !(evalClosure defs xs)
pure (x' ::: xs') pure (x' ::: xs')
@ -198,14 +198,15 @@ Reflect a => Reflect (List1 a) where
reflect fc defs lhs env xxs reflect fc defs lhs env xxs
= do x' <- reflect fc defs lhs env (head xxs) = do x' <- reflect fc defs lhs env (head xxs)
xs' <- reflect fc defs lhs env (tail 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 export
Reify a => Reify (Maybe a) where Reify a => Reify (Maybe a) where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "Nothing"), _) => pure Nothing (UN (Basic "Nothing"), _) => pure Nothing
(NS _ (UN "Just"), [_, (_, x)]) (UN (Basic "Just"), [_, (_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Just x') pure (Just x')
_ => cantReify val "Maybe" _ => cantReify val "Maybe"
@ -221,8 +222,8 @@ Reflect a => Reflect (Maybe a) where
export export
(Reify a, Reify b) => Reify (a, b) where (Reify a, Reify b) => Reify (a, b) where
reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)]) reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)])
= case (!(full (gamma defs) n)) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "MkPair") UN (Basic "MkPair")
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (x', y') pure (x', y')
@ -239,8 +240,8 @@ export
export export
Reify Namespace where Reify Namespace where
reify defs val@(NDCon _ n _ _ [(_, ns)]) reify defs val@(NDCon _ n _ _ [(_, ns)])
= case (!(full (gamma defs) n)) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "MkNS") UN (Basic "MkNS")
=> do ns' <- reify defs !(evalClosure defs ns) => do ns' <- reify defs !(evalClosure defs ns)
pure (unsafeFoldNamespace ns') pure (unsafeFoldNamespace ns')
_ => cantReify val "Namespace" _ => cantReify val "Namespace"
@ -255,8 +256,8 @@ Reflect Namespace where
export export
Reify ModuleIdent where Reify ModuleIdent where
reify defs val@(NDCon _ n _ _ [(_, ns)]) reify defs val@(NDCon _ n _ _ [(_, ns)])
= case (!(full (gamma defs) n)) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "MkMI") UN (Basic "MkMI")
=> do ns' <- reify defs !(evalClosure defs ns) => do ns' <- reify defs !(evalClosure defs ns)
pure (unsafeFoldModuleIdent ns') pure (unsafeFoldModuleIdent ns')
_ => cantReify val "ModuleIdent" _ => cantReify val "ModuleIdent"
@ -268,37 +269,62 @@ Reflect ModuleIdent where
= do ns' <- reflect fc defs lhs env (unsafeUnfoldModuleIdent ns) = do ns' <- reflect fc defs lhs env (unsafeUnfoldModuleIdent ns)
appCon fc defs (reflectiontt "MkMI") [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 export
Reify Name where Reify Name where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "UN"), [(_, str)]) (UN (Basic "UN"), [(_, str)])
=> do str' <- reify defs !(evalClosure defs str) => do str' <- reify defs !(evalClosure defs str)
pure (UN str') pure (UN str')
(NS _ (UN "MN"), [(_, str), (_, i)]) (UN (Basic "MN"), [(_, str), (_, i)])
=> do str' <- reify defs !(evalClosure defs str) => do str' <- reify defs !(evalClosure defs str)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (MN str' i') pure (MN str' i')
(NS _ (UN "NS"), [(_, ns), (_, n)]) (UN (Basic "NS"), [(_, ns), (_, n)])
=> do ns' <- reify defs !(evalClosure defs ns) => do ns' <- reify defs !(evalClosure defs ns)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (NS ns' n') pure (NS ns' n')
(NS _ (UN "DN"), [(_, str), (_, n)]) (UN (Basic "DN"), [(_, str), (_, n)])
=> do str' <- reify defs !(evalClosure defs str) => do str' <- reify defs !(evalClosure defs str)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (DN str' n') pure (DN str' n')
(NS _ (UN "RF"), [(_, str)]) (UN (Basic "Nested"), [(_, ix), (_, n)])
=> do str' <- reify defs !(evalClosure defs str)
pure (RF str')
(NS _ (UN "Nested"), [(_, ix), (_, n)])
=> do ix' <- reify defs !(evalClosure defs ix) => do ix' <- reify defs !(evalClosure defs ix)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (Nested ix' n') pure (Nested ix' n')
(NS _ (UN "CaseBlock"), [(_, outer), (_, i)]) (UN (Basic "CaseBlock"), [(_, outer), (_, i)])
=> do outer' <- reify defs !(evalClosure defs outer) => do outer' <- reify defs !(evalClosure defs outer)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (CaseBlock outer' i') pure (CaseBlock outer' i')
(NS _ (UN "WithBlock"), [(_, outer), (_, i)]) (UN (Basic "WithBlock"), [(_, outer), (_, i)])
=> do outer' <- reify defs !(evalClosure defs outer) => do outer' <- reify defs !(evalClosure defs outer)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (WithBlock outer' i') pure (WithBlock outer' i')
@ -324,9 +350,6 @@ Reflect Name where
= do str' <- reflect fc defs lhs env str = do str' <- reflect fc defs lhs env str
n' <- reflect fc defs lhs env n n' <- reflect fc defs lhs env n
appCon fc defs (reflectiontt "DN") [str', 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) reflect fc defs lhs env (Nested ix n)
= do ix' <- reflect fc defs lhs env ix = do ix' <- reflect fc defs lhs env ix
n' <- reflect fc defs lhs env n n' <- reflect fc defs lhs env n
@ -350,14 +373,14 @@ Reflect Name where
export export
Reify NameType where Reify NameType where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "Bound"), _) => pure Bound (UN (Basic "Bound"), _) => pure Bound
(NS _ (UN "Func"), _) => pure Func (UN (Basic "Func"), _) => pure Func
(NS _ (UN "DataCon"), [(_, t), (_, i)]) (UN (Basic "DataCon"), [(_, t), (_, i)])
=> do t' <- reify defs !(evalClosure defs t) => do t' <- reify defs !(evalClosure defs t)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (DataCon t' i') pure (DataCon t' i')
(NS _ (UN "TyCon"), [(_, t),(_, i)]) (UN (Basic "TyCon"), [(_, t),(_, i)])
=> do t' <- reify defs !(evalClosure defs t) => do t' <- reify defs !(evalClosure defs t)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (TyCon t' i') pure (TyCon t' i')
@ -380,75 +403,75 @@ Reflect NameType where
export export
Reify Constant where Reify Constant where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "I"), [(_, x)]) (UN (Basic "I"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (I x') pure (I x')
(NS _ (UN "I8"), [(_, x)]) (UN (Basic "I8"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (I8 x') pure (I8 x')
(NS _ (UN "I16"), [(_, x)]) (UN (Basic "I16"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (I16 x') pure (I16 x')
(NS _ (UN "I32"), [(_, x)]) (UN (Basic "I32"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (I32 x') pure (I32 x')
(NS _ (UN "I64"), [(_, x)]) (UN (Basic "I64"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (I64 x') pure (I64 x')
(NS _ (UN "BI"), [(_, x)]) (UN (Basic "BI"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (BI x') pure (BI x')
(NS _ (UN "B8"), [(_, x)]) (UN (Basic "B8"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (B8 x') pure (B8 x')
(NS _ (UN "B16"), [(_, x)]) (UN (Basic "B16"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (B16 x') pure (B16 x')
(NS _ (UN "B32"), [(_, x)]) (UN (Basic "B32"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (B32 x') pure (B32 x')
(NS _ (UN "B64"), [(_, x)]) (UN (Basic "B64"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (B64 x') pure (B64 x')
(NS _ (UN "Str"), [(_, x)]) (UN (Basic "Str"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Str x') pure (Str x')
(NS _ (UN "Ch"), [(_, x)]) (UN (Basic "Ch"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Ch x') pure (Ch x')
(NS _ (UN "Db"), [(_, x)]) (UN (Basic "Db"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Db x') pure (Db x')
(NS _ (UN "WorldVal"), []) (UN (Basic "WorldVal"), [])
=> pure WorldVal => pure WorldVal
(NS _ (UN "IntType"), []) (UN (Basic "IntType"), [])
=> pure IntType => pure IntType
(NS _ (UN "Int8Type"), []) (UN (Basic "Int8Type"), [])
=> pure Int8Type => pure Int8Type
(NS _ (UN "Int16Type"), []) (UN (Basic "Int16Type"), [])
=> pure Int16Type => pure Int16Type
(NS _ (UN "Int32Type"), []) (UN (Basic "Int32Type"), [])
=> pure Int32Type => pure Int32Type
(NS _ (UN "Int64Type"), []) (UN (Basic "Int64Type"), [])
=> pure Int64Type => pure Int64Type
(NS _ (UN "IntegerType"), []) (UN (Basic "IntegerType"), [])
=> pure IntegerType => pure IntegerType
(NS _ (UN "Bits8Type"), []) (UN (Basic "Bits8Type"), [])
=> pure Bits8Type => pure Bits8Type
(NS _ (UN "Bits16Type"), []) (UN (Basic "Bits16Type"), [])
=> pure Bits16Type => pure Bits16Type
(NS _ (UN "Bits32Type"), []) (UN (Basic "Bits32Type"), [])
=> pure Bits32Type => pure Bits32Type
(NS _ (UN "Bits64Type"), []) (UN (Basic "Bits64Type"), [])
=> pure Bits64Type => pure Bits64Type
(NS _ (UN "StringType"), []) (UN (Basic "StringType"), [])
=> pure StringType => pure StringType
(NS _ (UN "CharType"), []) (UN (Basic "CharType"), [])
=> pure CharType => pure CharType
(NS _ (UN "DoubleType"), []) (UN (Basic "DoubleType"), [])
=> pure DoubleType => pure DoubleType
(NS _ (UN "WorldType"), []) (UN (Basic "WorldType"), [])
=> pure WorldType => pure WorldType
_ => cantReify val "Constant" _ => cantReify val "Constant"
reify defs val = cantReify val "Constant" reify defs val = cantReify val "Constant"
@ -528,10 +551,10 @@ Reflect Constant where
export export
Reify Visibility where Reify Visibility where
reify defs val@(NDCon _ n _ _ _) reify defs val@(NDCon _ n _ _ _)
= case !(full (gamma defs) n) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "Private") => pure Private UN (Basic "Private") => pure Private
NS _ (UN "Export") => pure Export UN (Basic "Export") => pure Export
NS _ (UN "Public") => pure Public UN (Basic "Public") => pure Public
_ => cantReify val "Visibility" _ => cantReify val "Visibility"
reify defs val = cantReify val "Visibility" reify defs val = cantReify val "Visibility"
@ -544,10 +567,10 @@ Reflect Visibility where
export export
Reify TotalReq where Reify TotalReq where
reify defs val@(NDCon _ n _ _ _) reify defs val@(NDCon _ n _ _ _)
= case !(full (gamma defs) n) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "Total") => pure Total UN (Basic "Total") => pure Total
NS _ (UN "CoveringOnly") => pure CoveringOnly UN (Basic "CoveringOnly") => pure CoveringOnly
NS _ (UN "PartialOK") => pure PartialOK UN (Basic "PartialOK") => pure PartialOK
_ => cantReify val "TotalReq" _ => cantReify val "TotalReq"
reify defs val = cantReify val "TotalReq" reify defs val = cantReify val "TotalReq"
@ -560,10 +583,10 @@ Reflect TotalReq where
export export
Reify RigCount where Reify RigCount where
reify defs val@(NDCon _ n _ _ _) reify defs val@(NDCon _ n _ _ _)
= case !(full (gamma defs) n) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "M0") => pure erased UN (Basic "M0") => pure erased
NS _ (UN "M1") => pure linear UN (Basic "M1") => pure linear
NS _ (UN "MW") => pure top UN (Basic "MW") => pure top
_ => cantReify val "Count" _ => cantReify val "Count"
reify defs val = cantReify val "Count" reify defs val = cantReify val "Count"
@ -578,11 +601,11 @@ Reflect RigCount where
export export
Reify t => Reify (PiInfo t) where Reify t => Reify (PiInfo t) where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "ImplicitArg"), _) => pure Implicit (UN (Basic "ImplicitArg"), _) => pure Implicit
(NS _ (UN "ExplicitArg"), _) => pure Explicit (UN (Basic "ExplicitArg"), _) => pure Explicit
(NS _ (UN "AutoImplicit"), _) => pure AutoImplicit (UN (Basic "AutoImplicit"), _) => pure AutoImplicit
(NS _ (UN "DefImplicit"), [_, (_, t)]) (UN (Basic "DefImplicit"), [_, (_, t)])
=> do t' <- reify defs !(evalClosure defs t) => do t' <- reify defs !(evalClosure defs t)
pure (DefImplicit t') pure (DefImplicit t')
_ => cantReify val "PiInfo" _ => cantReify val "PiInfo"
@ -603,10 +626,10 @@ Reflect t => Reflect (PiInfo t) where
export export
Reify LazyReason where Reify LazyReason where
reify defs val@(NDCon _ n _ _ _) reify defs val@(NDCon _ n _ _ _)
= case !(full (gamma defs) n) of = case dropAllNS !(full (gamma defs) n) of
NS _ (UN "LInf") => pure LInf UN (Basic "LInf") => pure LInf
NS _ (UN "LLazy") => pure LLazy UN (Basic "LLazy") => pure LLazy
NS _ (UN "LUnknown") => pure LUnknown UN (Basic "LUnknown") => pure LUnknown
_ => cantReify val "LazyReason" _ => cantReify val "LazyReason"
reify defs val = cantReify val "LazyReason" reify defs val = cantReify val "LazyReason"
@ -619,8 +642,8 @@ Reflect LazyReason where
export export
Reify VirtualIdent where Reify VirtualIdent where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "Interactive"), []) (UN (Basic "Interactive"), [])
=> pure Interactive => pure Interactive
_ => cantReify val "VirtualIdent" _ => cantReify val "VirtualIdent"
reify defs val = cantReify val "VirtualIdent" reify defs val = cantReify val "VirtualIdent"
@ -637,12 +660,12 @@ Reflect BuiltinType where
export export
Reify BuiltinType where Reify BuiltinType where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "BuiltinNatural"), []) (UN (Basic "BuiltinNatural"), [])
=> pure BuiltinNatural => pure BuiltinNatural
(NS _ (UN "NaturalToInteger"), []) (UN (Basic "NaturalToInteger"), [])
=> pure NaturalToInteger => pure NaturalToInteger
(NS _ (UN "IntegerToNatural"), []) (UN (Basic "IntegerToNatural"), [])
=> pure IntegerToNatural => pure IntegerToNatural
_ => cantReify val "BuiltinType" _ => cantReify val "BuiltinType"
reify defs val = cantReify val "BuiltinType" reify defs val = cantReify val "BuiltinType"
@ -655,14 +678,14 @@ Reflect VirtualIdent where
export export
Reify OriginDesc where Reify OriginDesc where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "PhysicalIdrSrc"), [(_, ident)]) (UN (Basic "PhysicalIdrSrc"), [(_, ident)])
=> do ident' <- reify defs !(evalClosure defs ident) => do ident' <- reify defs !(evalClosure defs ident)
pure (PhysicalIdrSrc ident') pure (PhysicalIdrSrc ident')
(NS _ (UN "PhysicalPkgSrc"), [(_, fname)]) (UN (Basic "PhysicalPkgSrc"), [(_, fname)])
=> do fname' <- reify defs !(evalClosure defs fname) => do fname' <- reify defs !(evalClosure defs fname)
pure (PhysicalPkgSrc fname') pure (PhysicalPkgSrc fname')
(NS _ (UN "Virtual"), [(_, ident)]) (UN (Basic "Virtual"), [(_, ident)])
=> do ident' <- reify defs !(evalClosure defs ident) => do ident' <- reify defs !(evalClosure defs ident)
pure (Virtual ident') pure (Virtual ident')
_ => cantReify val "OriginDesc" _ => cantReify val "OriginDesc"
@ -683,13 +706,13 @@ Reflect OriginDesc where
export export
Reify FC where Reify FC where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "MkFC"), [(_, fn), (_, start), (_, end)]) (UN (Basic "MkFC"), [(_, fn), (_, start), (_, end)])
=> do fn' <- reify defs !(evalClosure defs fn) => do fn' <- reify defs !(evalClosure defs fn)
start' <- reify defs !(evalClosure defs start) start' <- reify defs !(evalClosure defs start)
end' <- reify defs !(evalClosure defs end) end' <- reify defs !(evalClosure defs end)
pure (MkFC fn' start' end') pure (MkFC fn' start' end')
(NS _ (UN "EmptyFC"), _) => pure EmptyFC (UN (Basic "EmptyFC"), _) => pure EmptyFC
_ => cantReify val "FC" _ => cantReify val "FC"
reify defs val = cantReify val "FC" reify defs val = cantReify val "FC"

2
src/Core/TT.idr
View File

@ -78,7 +78,7 @@ data Constant
export export
isConstantType : Name -> Maybe Constant isConstantType : Name -> Maybe Constant
isConstantType (UN n) = case n of isConstantType (UN (Basic n)) = case n of
"Int" => Just IntType "Int" => Just IntType
"Int8" => Just Int8Type "Int8" => Just Int8Type
"Int16" => Just Int16Type "Int16" => Just Int16Type

12
src/Core/TTC.idr
View File

@ -73,17 +73,20 @@ TTC FC where
export export
TTC Name where 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 (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 (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 (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 (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 (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 (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 (WithBlock x y) = do tag 8; toBuf b x; toBuf b y
toBuf b (Resolved x) toBuf b (Resolved x)
= throw (InternalError ("Can't write resolved name " ++ show x)) = throw (InternalError ("Can't write resolved name " ++ show x))
toBuf b (UN Underscore) = tag 9
fromBuf b fromBuf b
= case !getTag of = case !getTag of
@ -91,7 +94,7 @@ TTC Name where
x <- fromBuf b x <- fromBuf b
pure (NS xs x) pure (NS xs x)
1 => do x <- fromBuf b 1 => do x <- fromBuf b
pure (UN x) pure (UN $ Basic x)
2 => do x <- fromBuf b 2 => do x <- fromBuf b
y <- fromBuf b y <- fromBuf b
pure (MN x y) pure (MN x y)
@ -102,7 +105,7 @@ TTC Name where
y <- fromBuf b y <- fromBuf b
pure (DN x y) pure (DN x y)
5 => do x <- fromBuf b 5 => do x <- fromBuf b
pure (RF x) pure (UN $ Field x)
6 => do x <- fromBuf b 6 => do x <- fromBuf b
y <- fromBuf b y <- fromBuf b
pure (Nested x y) pure (Nested x y)
@ -112,6 +115,7 @@ TTC Name where
8 => do x <- fromBuf b 8 => do x <- fromBuf b
y <- fromBuf b y <- fromBuf b
pure (WithBlock x y) pure (WithBlock x y)
9 => pure (UN Underscore)
_ => corrupt "Name" _ => corrupt "Name"
export export

4
src/Core/Termination.idr
View File

@ -385,8 +385,8 @@ mutual
| Nothing => undefinedName fc fn_in | Nothing => undefinedName fc fn_in
let fn = fullname gdef let fn = fullname gdef
log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn) log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller")) aSmaller <- resolved (gamma defs) (NS builtinNS (UN $ Basic "assert_smaller"))
cond [(fn == NS builtinNS (UN "assert_total"), pure []) cond [(fn == NS builtinNS (UN $ Basic "assert_total"), pure [])
,(caseFn fn, ,(caseFn fn,
do scs1 <- traverse (findSC defs env g pats) args do scs1 <- traverse (findSC defs env g pats) args
mps <- getCasePats defs fn pats args mps <- getCasePats defs fn pats args

3
src/Core/UnifyState.idr
View File

@ -166,9 +166,8 @@ export
genMVName : {auto c : Ref Ctxt Defs} -> genMVName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
Name -> Core Name Name -> Core Name
genMVName (UN str) = genName str genMVName (UN str) = genName (displayUserName str)
genMVName (MN str _) = genName str genMVName (MN str _) = genName str
genMVName (RF str) = genName str
genMVName n genMVName n
= do ust <- get UST = do ust <- get UST
put UST (record { nextName $= (+1) } ust) put UST (record { nextName $= (+1) } ust)

2
src/Core/Value.idr
View File

@ -105,7 +105,7 @@ mutual
export export
ntCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars 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 ntCon fc n tag Z [] = case isConstantType n of
Just c => NPrimVal fc c Just c => NPrimVal fc c
Nothing => NTCon fc n tag Z [] Nothing => NTCon fc n tag Z []

87
src/Idris/Desugar.idr
View File

@ -35,7 +35,6 @@ import TTImp.Utils
import Libraries.Data.IMaybe import Libraries.Data.IMaybe
import Libraries.Utils.Shunting import Libraries.Utils.Shunting
import Libraries.Utils.String
import Control.Monad.State import Control.Monad.State
import Data.Maybe import Data.Maybe
@ -150,12 +149,12 @@ addNS _ n = n
bindFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp bindFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp
bindFun fc ns ma f = bindFun fc ns ma f =
let fc = virtualiseFC fc in 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 -> Maybe Namespace -> RawImp -> RawImp -> RawImp
seqFun fc ns ma mb = seqFun fc ns ma mb =
let fc = virtualiseFC fc in 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 : List (Name, FC, RawImp) -> Maybe Namespace -> RawImp -> RawImp
bindBangs [] ns tm = tm bindBangs [] ns tm = tm
@ -169,24 +168,24 @@ idiomise fc (IAlternative afc u alts)
= IAlternative afc (mapAltType (idiomise afc) u) (idiomise afc <$> alts) = IAlternative afc (mapAltType (idiomise afc) u) (idiomise afc <$> alts)
idiomise fc (IApp afc f a) idiomise fc (IApp afc f a)
= let fc = virtualiseFC fc in = let fc = virtualiseFC fc in
IApp fc (IApp fc (IVar fc (UN "<*>")) IApp fc (IApp fc (IVar fc (UN $ Basic "<*>"))
(idiomise afc f)) (idiomise afc f))
a a
idiomise fc fn idiomise fc fn
= let fc = virtualiseFC fc in = let fc = virtualiseFC fc in
IApp fc (IVar fc (UN "pure")) fn IApp fc (IVar fc (UN $ Basic "pure")) fn
pairname : Name pairname : Name
pairname = NS builtinNS (UN "Pair") pairname = NS builtinNS (UN $ Basic "Pair")
mkpairname : Name mkpairname : Name
mkpairname = NS builtinNS (UN "MkPair") mkpairname = NS builtinNS (UN $ Basic "MkPair")
dpairname : Name dpairname : Name
dpairname = NS dpairNS (UN "DPair") dpairname = NS dpairNS (UN $ Basic "DPair")
mkdpairname : Name mkdpairname : Name
mkdpairname = NS dpairNS (UN "MkDPair") mkdpairname = NS dpairNS (UN $ Basic "MkDPair")
data Bang : Type where data Bang : Type where
@ -204,7 +203,7 @@ mutual
mn !(desugarB side ps argTy) mn !(desugarB side ps argTy)
!(desugarB side ps' retTy) !(desugarB side ps' retTy)
desugarB side ps (PLam fc rig p pat@(PRef prefFC n@(UN nm)) argTy scope) 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 then do whenJust (isConcreteFC prefFC) $ \nfc
=> addSemanticDecorations [(nfc, Bound, Just n)] => addSemanticDecorations [(nfc, Bound, Just n)]
pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p) pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
@ -270,8 +269,8 @@ mutual
= do l' <- desugarB side ps l = do l' <- desugarB side ps l
r' <- desugarB side ps r r' <- desugarB side ps r
pure $ IAlternative fc FirstSuccess pure $ IAlternative fc FirstSuccess
[apply (IVar fc (UN "===")) [l', r'], [apply (IVar fc (UN $ Basic "===")) [l', r'],
apply (IVar fc (UN "~=~")) [l', r']] apply (IVar fc (UN $ Basic "~=~")) [l', r']]
desugarB side ps (PBracketed fc e) = desugarB side ps e desugarB side ps (PBracketed fc e) = desugarB side ps e
desugarB side ps (POp fc opFC op l r) desugarB side ps (POp fc opFC op l r)
= do ts <- toTokList (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) desugarB side ps (PHole fc br holename)
= do when br $ = do when br $
do syn <- get Syn do syn <- get Syn
put Syn (record { bracketholes $= ((UN holename) ::) } syn) put Syn (record { bracketholes $= ((UN (Basic holename)) ::) } syn)
pure $ IHole fc holename pure $ IHole fc holename
desugarB side ps (PType fc) = pure $ IType fc desugarB side ps (PType fc) = pure $ IType fc
desugarB side ps (PAs fc nameFC vname pattern) desugarB side ps (PAs fc nameFC vname pattern)
@ -405,37 +404,37 @@ mutual
desugarB side ps (PDPair fc opFC l ty r) desugarB side ps (PDPair fc opFC l ty r)
= throw (GenericMsg fc "Invalid dependent pair type") = throw (GenericMsg fc "Invalid dependent pair type")
desugarB side ps (PUnit fc) desugarB side ps (PUnit fc)
= pure $ IAlternative fc (UniqueDefault (IVar fc (UN "MkUnit"))) = pure $ IAlternative fc (UniqueDefault (IVar fc (UN $ Basic "MkUnit")))
[IVar fc (UN "Unit"), [IVar fc (UN $ Basic "Unit"),
IVar fc (UN "MkUnit")] IVar fc (UN $ Basic "MkUnit")]
desugarB side ps (PIfThenElse fc x t e) desugarB side ps (PIfThenElse fc x t e)
= let fc = virtualiseFC fc in = let fc = virtualiseFC fc in
pure $ ICase fc !(desugarB side ps x) (IVar fc (UN "Bool")) pure $ ICase fc !(desugarB side ps x) (IVar fc (UN $ Basic "Bool"))
[PatClause fc (IVar fc (UN "True")) !(desugar side ps t), [PatClause fc (IVar fc (UN $ Basic "True")) !(desugar side ps t),
PatClause fc (IVar fc (UN "False")) !(desugar side ps e)] PatClause fc (IVar fc (UN $ Basic "False")) !(desugar side ps e)]
desugarB side ps (PComprehension fc ret conds) = do desugarB side ps (PComprehension fc ret conds) = do
let ns = mbNamespace !(get Bang) let ns = mbNamespace !(get Bang)
desugarB side ps (PDoBlock fc ns (map (guard ns) conds ++ [toPure ns ret])) desugarB side ps (PDoBlock fc ns (map (guard ns) conds ++ [toPure ns ret]))
where where
guard : Maybe Namespace -> PDo -> PDo guard : Maybe Namespace -> PDo -> PDo
guard ns (DoExp fc tm) 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 guard ns d = d
toPure : Maybe Namespace -> PTerm -> PDo 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) desugarB side ps (PRewrite fc rule tm)
= pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm) = pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm)
desugarB side ps (PRange fc start next end) desugarB side ps (PRange fc start next end)
= let fc = virtualiseFC fc in = let fc = virtualiseFC fc in
desugarB side ps $ case next of desugarB side ps $ case next of
Nothing => papply fc (PRef fc (UN "rangeFromTo")) [start,end] Nothing => papply fc (PRef fc (UN $ Basic "rangeFromTo")) [start,end]
Just n => papply fc (PRef fc (UN "rangeFromThenTo")) [start, n, end] Just n => papply fc (PRef fc (UN $ Basic "rangeFromThenTo")) [start, n, end]
desugarB side ps (PRangeStream fc start next) desugarB side ps (PRangeStream fc start next)
= let fc = virtualiseFC fc in = let fc = virtualiseFC fc in
desugarB side ps $ case next of desugarB side ps $ case next of
Nothing => papply fc (PRef fc (UN "rangeFrom")) [start] Nothing => papply fc (PRef fc (UN $ Basic "rangeFrom")) [start]
Just n => papply fc (PRef fc (UN "rangeFromThen")) [start, n] Just n => papply fc (PRef fc (UN $ Basic "rangeFromThen")) [start, n]
desugarB side ps (PUnifyLog fc lvl tm) desugarB side ps (PUnifyLog fc lvl tm)
= pure $ IUnifyLog fc lvl !(desugarB side ps tm) = pure $ IUnifyLog fc lvl !(desugarB side ps tm)
desugarB side ps (PPostfixApp fc rec projs) desugarB side ps (PPostfixApp fc rec projs)
@ -468,9 +467,9 @@ mutual
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
Side -> List Name -> Side -> List Name ->
(nilFC : FC) -> List (FC, PTerm) -> Core RawImp (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) 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)] [!(desugarB side ps x), !(expandList side ps nilFC xs)]
expandSnocList expandSnocList
@ -480,9 +479,9 @@ mutual
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
Side -> List Name -> (nilFC : FC) -> List (FC, PTerm) -> Core RawImp 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) 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)] [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)]
addFromString : {auto c : Ref Ctxt Defs} -> addFromString : {auto c : Ref Ctxt Defs} ->
@ -526,7 +525,7 @@ mutual
concatStr a b = concatStr a b =
let aFC = virtualiseFC (getFC a) let aFC = virtualiseFC (getFC a)
bFC = virtualiseFC (getFC b) 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 -> Nat -> List (List PStr) -> Core (List PStr)
trimMultiline fc indent lines trimMultiline fc indent lines
@ -647,13 +646,13 @@ mutual
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
Side -> List Name -> Tree OpStr PTerm -> Core RawImp 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 = do l' <- desugarTree side ps l
r' <- desugarTree side ps r r' <- desugarTree side ps r
pure (IAlternative loc FirstSuccess pure (IAlternative loc FirstSuccess
[apply (IVar eqFC (UN "===")) [l', r'], [apply (IVar eqFC (UN $ Basic "===")) [l', r'],
apply (IVar eqFC (UN "~=~")) [l', r']]) apply (IVar eqFC (UN $ Basic "~=~")) [l', r']])
desugarTree side ps (Infix loc _ (UN "$") l r) -- special case since '$' is special syntax desugarTree side ps (Infix loc _ (UN $ Basic "$") l r) -- special case since '$' is special syntax
= do l' <- desugarTree side ps l = do l' <- desugarTree side ps l
r' <- desugarTree side ps r r' <- desugarTree side ps r
pure (IApp loc l' r') pure (IApp loc l' r')
@ -668,7 +667,7 @@ mutual
-- Note: In case of negated signed integer literals, we apply the -- Note: In case of negated signed integer literals, we apply the
-- negation directly. Otherwise, the literal might be -- negation directly. Otherwise, the literal might be
-- truncated to 0 before being passed on to `negate`. -- 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) = let newFC = fromMaybe EmptyFC (mergeFC loc fc)
continue = desugarTree side ps . Leaf . PPrimVal newFC continue = desugarTree side ps . Leaf . PPrimVal newFC
in case c of in case c of
@ -682,11 +681,11 @@ mutual
-- not a signed integer literal. proceed by desugaring -- not a signed integer literal. proceed by desugaring
-- and applying to `negate`. -- and applying to `negate`.
_ => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c) _ => 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 = 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) desugarTree side ps (Pre loc opFC op arg)
= do arg' <- desugarTree side ps arg = do arg' <- desugarTree side ps arg
@ -801,7 +800,7 @@ mutual
ps !(desugar AnyExpr ps ty))) ps !(desugar AnyExpr ps ty)))
where where
toRF : Name -> Name toRF : Name -> Name
toRF (UN n) = RF n toRF (UN (Basic n)) = UN (Field n)
toRF n = n toRF n = n
export export
@ -995,17 +994,19 @@ mutual
fname (MkField _ _ _ _ n _) = n fname (MkField _ _ _ _ n _) = n
mkConName : Name -> Name 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) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp) mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
mapDesugarPiInfo ps = traverse (desugar AnyExpr ps) 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 = do syn <- get Syn
put Syn (record { prefixes $= insert n prec } syn) put Syn (record { prefixes $= insert n prec } syn)
pure [] pure []
desugarDecl ps (PFixity fc fix prec (UN n)) desugarDecl ps (PFixity fc fix prec (UN (Basic n)))
= do syn <- get Syn = do syn <- get Syn
put Syn (record { infixes $= insert n (fix, prec) } syn) put Syn (record { infixes $= insert n (fix, prec) } syn)
pure [] pure []
@ -1022,7 +1023,7 @@ mutual
desugarDecl ps (PTransform fc n lhs rhs) desugarDecl ps (PTransform fc n lhs rhs)
= do (bound, blhs) <- bindNames False !(desugar LHS ps lhs) = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
rhs' <- desugar AnyExpr (bound ++ ps) rhs 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) desugarDecl ps (PRunElabDecl fc tm)
= do tm' <- desugar AnyExpr ps tm = do tm' <- desugar AnyExpr ps tm
pure [IRunElabDecl fc tm'] pure [IRunElabDecl fc tm']

16
src/Idris/Doc/String.idr
View File

@ -120,8 +120,10 @@ prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm
prettyName : Name -> Doc IdrisDocAnn prettyName : Name -> Doc IdrisDocAnn
prettyName n = prettyName n =
let root = nameRoot n in case userNameRoot n of
if isOpName n then parens (pretty root) else pretty root -- 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 : Maybe String -> Doc IdrisDocAnn -> Doc IdrisDocAnn
prettyKindedName Nothing nm = nm prettyKindedName Nothing nm = nm
@ -179,7 +181,7 @@ getDocsForName fc n config
= do syn <- get Syn = do syn <- get Syn
defs <- get Ctxt defs <- get Ctxt
let extra = case nameRoot n of let extra = case nameRoot n of
"-" => [NS numNS (UN "negate")] "-" => [NS numNS (UN $ Basic "negate")]
_ => [] _ => []
resolved <- lookupCtxtName n (gamma defs) resolved <- lookupCtxtName n (gamma defs)
let all@(_ :: _) = extra ++ map fst resolved let all@(_ :: _) = extra ++ map fst resolved
@ -237,7 +239,9 @@ getDocsForName fc n config
getInfixDoc : Name -> Core (List (Doc IdrisDocAnn)) getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))
getInfixDoc n 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 [] | Nothing => pure []
pure $ pure $ hsep pure $ pure $ hsep
[ pretty (show fixity) [ pretty (show fixity)
@ -248,7 +252,9 @@ getDocsForName fc n config
getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn)) getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))
getPrefixDoc n 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 [] | Nothing => pure []
pure $ ["prefix operator, level" <++> pretty (show assoc)] pure $ ["prefix operator, level" <++> pretty (show assoc)]

19
src/Idris/Elab/Implementation.idr
View File

@ -39,7 +39,7 @@ export
mkImplName : FC -> Name -> List RawImp -> Name mkImplName : FC -> Name -> List RawImp -> Name
mkImplName fc n ps mkImplName fc n ps
= DN (show n ++ " implementation at " ++ replaceSep (show fc)) = DN (show n ++ " implementation at " ++ replaceSep (show fc))
(UN ("__Impl_" ++ show n ++ "_" ++ (UN $ Basic ("__Impl_" ++ show n ++ "_" ++
showSep "_" (map show ps))) showSep "_" (map show ps)))
bindConstraints : FC -> PiInfo RawImp -> bindConstraints : FC -> PiInfo RawImp ->
@ -64,7 +64,7 @@ addDefaults fc impName params allms defs body
extendBody [] missing body extendBody [] missing body
where where
specialiseMeth : Name -> (Name, RawImp) 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, -- Given the list of missing names, if any are among the default definitions,
-- add them to the body -- add them to the body
extendBody : List Name -> List Name -> List ImpDecl -> 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 mkLam argns
(impsApply (impsApply
(applyTo (IVar EmptyFC n) argns) (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 where
applyUpdate : (Name, RigCount, PiInfo RawImp) -> applyUpdate : (Name, RigCount, PiInfo RawImp) ->
(Name, RigCount, PiInfo RawImp) (Name, RigCount, PiInfo RawImp)
applyUpdate (UN n, c, p) applyUpdate (UN (Basic n), c, p)
= maybe (UN n, c, p) (\n' => (UN n', c, p)) (lookup n upds) = maybe (UN (Basic n), c, p) (\n' => (UN (Basic n'), c, p)) (lookup n upds)
applyUpdate t = t applyUpdate t = t
methName : Name -> Name methName : Name -> Name
methName (NS _ n) = methName n methName (NS _ n) = methName n
methName n methName n
= DN (show n) = DN (show n)
(UN (show n ++ "_" ++ show iname ++ "_" ++ (UN $ Basic (show n ++ "_" ++ show iname ++ "_" ++
(if named then show impName_in else "") ++ (if named then show impName_in else "") ++
showSep "_" (map show ps))) 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 -- top level method name to current implementation's method name
methNameUpdate : (Name, Name, t) -> (Name, Name) methNameUpdate : (Name, Name, t) -> (Name, Name)
methNameUpdate (UN mn, fn, _) = (UN mn, fn) methNameUpdate (UN mn, fn, _) = (UN mn, fn)
methNameUpdate (RF mn, fn, _) = (RF mn, fn)
methNameUpdate (NS _ mn, fn, p) = methNameUpdate (mn, fn, p) 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 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 ++ "Adding transform for " ++ show meth.name ++ " : " ++ show meth.type ++
"\n\tfor " ++ show iname ++ " in " ++ show ns "\n\tfor " ++ show iname ++ " in " ++ show ns
let lhs = INamedApp vfc (IVar vfc meth.name) let lhs = INamedApp vfc (IVar vfc meth.name)
(UN "__con") (UN $ Basic "__con")
(IVar vfc iname) (IVar vfc iname)
let Just mname = lookup (dropNS meth.name) ns let Just mname = lookup (dropNS meth.name) ns
| Nothing => pure () | 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 log "elab.implementation" 5 $ show lhs ++ " ==> " ++ show rhs
handleUnify handleUnify
(processDecl [] nest env (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 => (\err =>
log "elab.implementation" 5 $ "Can't add transform " ++ log "elab.implementation" 5 $ "Can't add transform " ++
show lhs ++ " ==> " ++ show rhs ++ show lhs ++ " ==> " ++ show rhs ++

28
src/Idris/Elab/Interface.idr
View File

@ -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 -- bind the auto implicit for the interface - put it first, as it may be needed
-- in other method variables, including implicit variables -- in other method variables, including implicit variables
bindIFace : FC -> RawImp -> RawImp -> RawImp 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 -- Get the top level function for implementing a method
getMethToplevel : {vars : _} -> getMethToplevel : {vars : _} ->
@ -201,7 +201,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
let argns = getExplicitArgs 0 sig.type let argns = getExplicitArgs 0 sig.type
-- eta expand the RHS so that we put implicits in the right place -- eta expand the RHS so that we put implicits in the right place
let fnclause = PatClause vfc (INamedApp vfc (IVar sig.location cn) let fnclause = PatClause vfc (INamedApp vfc (IVar sig.location cn)
(UN "__con") (UN $ Basic "__con")
conapp) conapp)
(mkLam argns (mkLam argns
(apply (IVar EmptyFC (methName sig.name)) (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) = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)
applyCon : Name -> (Name, RawImp) 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)) (n, INamedApp vfc (IVar vfc n) name (IVar vfc name))
getExplicitArgs : Int -> RawImp -> List 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) = ILam EmptyFC top Explicit (Just x) (Implicit vfc False) (mkLam xs tm)
bindName : Name -> String bindName : Name -> String
bindName (UN n) = "__bind_" ++ n bindName (UN n) = "__bind_" ++ displayUserName n
bindName (NS _ n) = bindName n bindName (NS _ n) = bindName n
bindName n = show n bindName n = show n
methName : Name -> Name 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 -- Get the function for chasing a constraint. This is one of the
-- arguments to the record, appearing before the method arguments. -- 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 let fty = IPi fc top Explicit Nothing ity con
ty_imp <- bindTypeNames fc [] (meths ++ vars) fty ty_imp <- bindTypeNames fc [] (meths ++ vars) fty
let hintname = DN ("Constraint " ++ show con) 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] let tydecl = IClaim fc top vis [Inline, Hint False]
(MkImpTy EmptyFC EmptyFC hintname ty_imp) (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]) pure (hintname, [tydecl, fndef])
where where
bindName : Name -> String bindName : Name -> String
bindName (UN n) = "__bind_" ++ n bindName (UN n) = "__bind_" ++ displayUserName n
bindName (NS _ n) = bindName n bindName (NS _ n) = bindName n
bindName n = show n bindName n = show n
constName : Name -> Name constName : Name -> Name
constName n = UN (bindName n) constName n = UN (Basic $ bindName n)
impsBind : RawImp -> List String -> RawImp impsBind : RawImp -> List String -> RawImp
impsBind fn [] = fn impsBind fn [] = fn
@ -290,9 +290,11 @@ getDefault _ = Nothing
mkCon : FC -> Name -> Name mkCon : FC -> Name -> Name
mkCon loc (NS ns (UN n)) 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 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} -> updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} -> {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 : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)
nameCons i [] = [] nameCons i [] = []
nameCons i ((_, ty) :: rest) 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 -- Elaborate the data declaration part of the interface
elabAsData : (conName : Name) -> List Name -> 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 : RawImp -> List Name -> RawImp
applyParams tm [] = tm applyParams tm [] = tm
applyParams tm (UN n :: ns) applyParams tm (UN (Basic n) :: ns)
= applyParams (INamedApp vdfc tm (UN n) (IBindVar vdfc n)) ns = applyParams (INamedApp vdfc tm (UN (Basic n)) (IBindVar vdfc n)) ns
applyParams tm (_ :: ns) = applyParams tm ns applyParams tm (_ :: ns) = applyParams tm ns
changeNameTerm : Name -> RawImp -> Core RawImp changeNameTerm : Name -> RawImp -> Core RawImp

4
src/Idris/IDEMode/CaseSplit.idr
View File

@ -44,7 +44,7 @@ Updates = List (RawName, String)
toStrUpdate : {auto c : Ref Ctxt Defs} -> toStrUpdate : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} -> {auto s : Ref Syn SyntaxInfo} ->
(Name, RawImp) -> Core Updates (Name, RawImp) -> Core Updates
toStrUpdate (UN n, term) toStrUpdate (UN (Basic n), term)
= do clause <- pterm (map defaultKindedName term) -- hack = do clause <- pterm (map defaultKindedName term) -- hack
pure [(n, show (bracket clause))] pure [(n, show (bracket clause))]
where where
@ -196,7 +196,7 @@ updateCase splits line col
getIndent acc _ = acc getIndent acc _ = acc
fnName : Bool -> Name -> String fnName : Bool -> Name -> String
fnName lhs (UN n) fnName lhs (UN (Basic n))
= if isIdentNormal n then n = if isIdentNormal n then n
else if lhs then "(" ++ n ++ ")" else if lhs then "(" ++ n ++ ")"
else "op" else "op"

4
src/Idris/IDEMode/Commands.idr
View File

@ -266,10 +266,6 @@ SExpable a => SExpable (Maybe a) where
toSExp Nothing = SExpList [] toSExp Nothing = SExpList []
toSExp (Just x) = toSExp x toSExp (Just x) = toSExp x
export
sym : String -> Name
sym = UN
export export
version : Int -> Int -> SExp version : Int -> Int -> SExp
version maj min = toSExp (SymbolAtom "protocol-version", maj, min) version maj min = toSExp (SymbolAtom "protocol-version", maj, min)

2
src/Idris/IDEMode/Holes.idr
View File

@ -48,7 +48,7 @@ isHole def
-- Bring these back into REPL.idr -- Bring these back into REPL.idr
showName : Name -> Bool showName : Name -> Bool
showName (UN "_") = False showName (UN Underscore) = False
showName (MN _ _) = False showName (MN _ _) = False
showName _ = True showName _ = True

29
src/Idris/IDEMode/REPL.idr
View File

@ -167,40 +167,45 @@ process (LoadFile fname_in _)
replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
process (NameAt name Nothing) process (NameAt name Nothing)
= do defs <- get Ctxt = 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 let dat = map (\(name, _, gdef) => (name, gdef.location)) glob
pure (NameLocList dat) pure (NameLocList dat)
process (NameAt n (Just _)) process (NameAt n (Just _))
= do todoCmd "name-at <name> <line> <column>" = do todoCmd "name-at <name> <line> <column>"
pure $ REPL $ Edited $ DisplayEdit emptyDoc pure $ REPL $ Edited $ DisplayEdit emptyDoc
process (TypeOf n Nothing) 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))) 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) 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) 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) process (AddMissing l n)
= do todoCmd "add-missing" = do todoCmd "add-missing"
pure $ REPL $ Edited $ DisplayEdit emptyDoc pure $ REPL $ Edited $ DisplayEdit emptyDoc
process (ExprSearch l n hs all) process (ExprSearch l n hs all)
= replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l)
(map UN hs))) (UN $ Basic n) (map (UN . Basic) hs)))
process ExprSearchNext process ExprSearchNext
= replWrap $ Idris.REPL.process (Editing ExprSearchNext) = replWrap $ Idris.REPL.process (Editing ExprSearchNext)
process (GenerateDef l n) 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 process GenerateDefNext
= replWrap $ Idris.REPL.process (Editing GenerateDefNext) = replWrap $ Idris.REPL.process (Editing GenerateDefNext)
process (MakeLemma l n) 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) 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) 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) 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) process (Apropos n)
= do todoCmd "apropros" = do todoCmd "apropros"
pure $ REPL $ Printed emptyDoc pure $ REPL $ Printed emptyDoc

2
src/Idris/Package.idr
View File

@ -331,7 +331,7 @@ build pkg opts
Just exec => Just exec =>
do let Just (mainNS, mainFile) = mainmod pkg do let Just (mainNS, mainFile) = mainmod pkg
| Nothing => throw (GenericMsg emptyFC "No main module given") | 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 compileMain mainName mainFile exec
runScript (postbuild pkg) runScript (postbuild pkg)

51
src/Idris/Parser.idr
View File

@ -219,17 +219,17 @@ mutual
else fail "| not allowed here" else fail "| not allowed here"
where where
underscore : FC -> ArgType underscore : FC -> ArgType
underscore fc = NamedArg (UN "_") (PImplicit fc) underscore fc = NamedArg (UN Underscore) (PImplicit fc)
braceArgs : OriginDesc -> IndentInfo -> Rule (List ArgType) braceArgs : OriginDesc -> IndentInfo -> Rule (List ArgType)
braceArgs fname indents braceArgs fname indents
= do start <- bounds (decoratedSymbol fname "{") = do start <- bounds (decoratedSymbol fname "{")
list <- sepBy (decoratedSymbol fname ",") list <- sepBy (decoratedSymbol fname ",")
$ do x <- bounds (decoratedSimpleBinderName fname) $ do x <- bounds (UN . Basic <$> decoratedSimpleBinderName fname)
let fc = boundToFC fname x 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 $ 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 matchAny <- option [] (if isCons list then
do decoratedSymbol fname "," do decoratedSymbol fname ","
x <- bounds (decoratedSymbol fname "_") x <- bounds (decoratedSymbol fname "_")
@ -280,14 +280,14 @@ mutual
pure $ pure $
let fc = boundToFC fname (mergeBounds l r) let fc = boundToFC fname (mergeBounds l r)
opFC = virtualiseFC fc -- already been highlighted: we don't care 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") else fail "= not allowed")
<|> <|>
(do b <- bounds $ do (do b <- bounds $ do
continue indents continue indents
op <- bounds iOperator op <- bounds iOperator
e <- case op.val of e <- case op.val of
UN "$" => typeExpr q fname indents UN (Basic "$") => typeExpr q fname indents
_ => expr q fname indents _ => expr q fname indents
pure (op, e) pure (op, e)
(op, r) <- pure b.val (op, r) <- pure b.val
@ -298,7 +298,7 @@ mutual
dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
dpairType fname start indents dpairType fname start indents
= do loc <- bounds (do x <- decoratedSimpleBinderName fname = do loc <- bounds (do x <- UN . Basic <$> decoratedSimpleBinderName fname
decoratedSymbol fname ":" decoratedSymbol fname ":"
ty <- typeExpr pdef fname indents ty <- typeExpr pdef fname indents
pure (x, ty)) pure (x, ty))
@ -307,7 +307,7 @@ mutual
rest <- bounds (nestedDpair fname loc indents <|> typeExpr pdef fname indents) rest <- bounds (nestedDpair fname loc indents <|> typeExpr pdef fname indents)
pure (PDPair (boundToFC fname (mergeBounds start rest)) pure (PDPair (boundToFC fname (mergeBounds start rest))
(boundToFC fname op) (boundToFC fname op)
(PRef (boundToFC fname loc) (UN x)) (PRef (boundToFC fname loc) x)
ty ty
rest.val) rest.val)
@ -494,13 +494,13 @@ mutual
simplerExpr : OriginDesc -> IndentInfo -> Rule PTerm simplerExpr : OriginDesc -> IndentInfo -> Rule PTerm
simplerExpr fname indents simplerExpr fname indents
= do b <- bounds (do x <- bounds (decoratedSimpleBinderName fname) = do b <- bounds (do x <- bounds (UN . Basic <$> decoratedSimpleBinderName fname)
decoratedSymbol fname "@" decoratedSymbol fname "@"
commit commit
expr <- simpleExpr fname indents expr <- simpleExpr fname indents
pure (x, expr)) pure (x, expr))
(x, expr) <- pure b.val (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 <|> atom fname
<|> record_ fname indents <|> record_ fname indents
<|> singlelineStr pdef fname indents <|> singlelineStr pdef fname indents
@ -586,8 +586,9 @@ mutual
Rule (List (RigCount, WithBounds Name, PTerm)) Rule (List (RigCount, WithBounds Name, PTerm))
pibindListName fname indents pibindListName fname indents
= do rig <- multiplicity fname = do rig <- multiplicity fname
ns <- sepBy1 (decoratedSymbol fname ",") (bounds binderName) ns <- sepBy1 (decoratedSymbol fname ",")
let ns = forget $ map (map UN) ns (bounds $ UN <$> binderName)
let ns = forget ns
decorateBoundedNames fname Bound ns decorateBoundedNames fname Bound ns
decoratedSymbol fname ":" decoratedSymbol fname ":"
ty <- typeExpr pdef fname indents ty <- typeExpr pdef fname indents
@ -601,8 +602,9 @@ mutual
pure (rig, map UN n, ty)) pure (rig, map UN n, ty))
where where
-- _ gets treated specially here, it means "I don't care about the name" -- _ gets treated specially here, it means "I don't care about the name"
binderName : Rule String binderName : Rule UserName
binderName = unqualifiedName <|> (symbol "_" $> "_") binderName = Basic <$> unqualifiedName
<|> symbol "_" $> Underscore
pibindList : OriginDesc -> IndentInfo -> pibindList : OriginDesc -> IndentInfo ->
Rule (List (RigCount, WithBounds (Maybe Name), PTerm)) Rule (List (RigCount, WithBounds (Maybe Name), PTerm))
@ -665,7 +667,7 @@ mutual
ns <- sepBy1 (decoratedSymbol fname ",") ns <- sepBy1 (decoratedSymbol fname ",")
(bounds (decoratedSimpleBinderName fname)) (bounds (decoratedSimpleBinderName fname))
pure $ map (\n => ( erased {a=RigCount} pure $ map (\n => ( erased {a=RigCount}
, map (Just . UN) n , map (Just . UN . Basic) n
, PImplicit (boundToFC fname n)) , PImplicit (boundToFC fname n))
) (forget ns) ) (forget ns)
mustWorkBecause b.bounds "Cannot return a forall quantifier" mustWorkBecause b.bounds "Cannot return a forall quantifier"
@ -806,8 +808,8 @@ mutual
pure (upd path val) pure (upd path val)
where where
fieldName : Name -> String fieldName : Name -> String
fieldName (UN s) = s fieldName (UN (Basic s)) = s
fieldName (RF s) = s fieldName (UN (Field s)) = s
fieldName _ = "_impossible" fieldName _ = "_impossible"
-- this allows the dotted syntax .field -- this allows the dotted syntax .field
@ -844,14 +846,15 @@ mutual
_ => fail "Not a namespaced 'do'" _ => fail "Not a namespaced 'do'"
validPatternVar : Name -> EmptyRule () validPatternVar : Name -> EmptyRule ()
validPatternVar (UN n) validPatternVar (UN Underscore) = pure ()
= unless (lowerFirst n || n == "_") $ validPatternVar (UN (Basic n))
= unless (lowerFirst n) $
fail "Not a pattern variable" fail "Not a pattern variable"
validPatternVar _ = fail "Not a pattern variable" validPatternVar _ = fail "Not a pattern variable"
doAct : OriginDesc -> IndentInfo -> Rule (List PDo) doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
doAct fname indents 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 -- If the name doesn't begin with a lower case letter, we should
-- treat this as a pattern, so fail -- treat this as a pattern, so fail
validPatternVar n.val validPatternVar n.val
@ -1027,7 +1030,7 @@ mutual
start <- bounds (decoratedSymbol fname "(") start <- bounds (decoratedSymbol fname "(")
wval <- bracketedExpr fname start indents wval <- bracketedExpr fname start indents
prf <- optional (decoratedKeyword fname "proof" prf <- optional (decoratedKeyword fname "proof"
*> UN <$> decoratedSimpleBinderName fname) *> UN . Basic <$> decoratedSimpleBinderName fname)
ws <- mustWork $ nonEmptyBlockAfter col ws <- mustWork $ nonEmptyBlockAfter col
$ clause (S withArgs) (Just lhs) fname $ clause (S withArgs) (Just lhs) fname
pure (prf, flags, wval, forget ws)) pure (prf, flags, wval, forget ws))
@ -1343,7 +1346,7 @@ usingDecls fname indents
(do n <- optional (do n <- optional
(do x <- unqualifiedName (do x <- unqualifiedName
decoratedSymbol fname ":" decoratedSymbol fname ":"
pure (UN x)) pure (UN $ Basic x))
ty <- typeExpr pdef fname indents ty <- typeExpr pdef fname indents
pure (n, ty)) pure (n, ty))
decoratedSymbol fname ")" decoratedSymbol fname ")"
@ -1579,10 +1582,10 @@ paramDecls fname indents
oldParamDecls fname indents oldParamDecls fname indents
= do decoratedSymbol fname "(" = do decoratedSymbol fname "("
ps <- sepBy (decoratedSymbol fname ",") ps <- sepBy (decoratedSymbol fname ",")
(do x <- decoratedSimpleBinderName fname (do x <- UN . Basic <$> decoratedSimpleBinderName fname
decoratedSymbol fname ":" decoratedSymbol fname ":"
ty <- typeExpr pdef fname indents ty <- typeExpr pdef fname indents
pure (UN x, top, Explicit, ty)) pure (x, top, Explicit, ty))
decoratedSymbol fname ")" decoratedSymbol fname ")"
pure ps pure ps

10
src/Idris/Parser/Let.idr
View File

@ -82,12 +82,12 @@ mkDoLets origin lets = letFactory
buildDoLets : List (WithBounds LetBinder) -> List PDo buildDoLets : List (WithBounds LetBinder) -> List PDo
buildDoLets [] = [] buildDoLets [] = []
buildDoLets (b :: rest) = let fc = boundToFC origin b in case b.val of buildDoLets (b :: rest) = let fc = boundToFC origin b in case b.val of
(MkLetBinder rig (PRef fc' (UN n)) ty val []) => (MkLetBinder rig (PRef fc' (UN un)) ty val []) =>
(if lowerFirst n (if isPatternVariable un
then DoLet fc fc' (UN n) rig ty val then DoLet fc fc' (UN un) rig ty val
else DoLetPat fc (PRef fc' (UN n)) ty val [] else DoLetPat fc (PRef fc' (UN un)) ty val []
) :: buildDoLets rest ) :: buildDoLets rest
(MkLetBinder rig (PImplicit fc') ty val []) => (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) => (MkLetBinder rig pat ty val alts) =>
DoLetPat fc pat ty val alts :: buildDoLets rest DoLetPat fc pat ty val alts :: buildDoLets rest

4
src/Idris/Pretty.idr
View File

@ -396,12 +396,12 @@ mutual
where where
dePure : IPTerm -> IPTerm dePure : IPTerm -> IPTerm
dePure tm@(PApp _ (PRef _ n) arg) 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 dePure tm = tm
deGuard : PDo' KindedName -> PDo' KindedName deGuard : PDo' KindedName -> PDo' KindedName
deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) 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 deGuard tm = tm
go d (PRewrite _ rule tm) = go d (PRewrite _ rule tm) =
parenthesise (d > appPrec) $ group $ rewrite_ <++> go startPrec rule <+> line <+> in_ <++> go startPrec tm parenthesise (d > appPrec) $ group $ rewrite_ <++> go startPrec rule <+> line <+> in_ <++> go startPrec tm

21
src/Idris/REPL.idr
View File

@ -543,7 +543,10 @@ getItDecls
= do opts <- get ROpts = do opts <- get ROpts
case evalResultName opts of case evalResultName opts of
Nothing => pure [] 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 : prepareExp :
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
@ -553,9 +556,9 @@ prepareExp :
{auto o : Ref ROpts REPLOpts} -> {auto o : Ref ROpts REPLOpts} ->
PTerm -> Core ClosedTerm PTerm -> Core ClosedTerm
prepareExp ctm 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 let ttimpWithIt = ILocal replFC !getItDecls ttimp
inidx <- resolveName (UN "[input]") inidx <- resolveName (UN $ Basic "[input]")
(tm, ty) <- elabTerm inidx InExpr [] (MkNested []) (tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimpWithIt Nothing [] ttimpWithIt Nothing
tm_erased <- linearCheck replFC linear True [] tm tm_erased <- linearCheck replFC linear True [] tm
@ -604,7 +607,7 @@ execDecls decls = do
execDecl : PDecl -> Core () execDecl : PDecl -> Core ()
execDecl decl = do execDecl decl = do
i <- desugarDecl [] decl i <- desugarDecl [] decl
inidx <- resolveName (UN "[defs]") inidx <- resolveName (UN $ Basic "[defs]")
_ <- newRef EST (initEStateSub inidx [] SubRefl) _ <- newRef EST (initEStateSub inidx [] SubRefl)
processLocal [] (MkNested []) [] !getItDecls i processLocal [] (MkNested []) [] !getItDecls i
@ -675,13 +678,13 @@ inferAndElab : {auto c : Ref Ctxt Defs} ->
inferAndElab emode itm inferAndElab emode itm
= do ttimp <- desugar AnyExpr [] itm = do ttimp <- desugar AnyExpr [] itm
let ttimpWithIt = ILocal replFC !getItDecls ttimp 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 -- a TMP HACK to prioritise list syntax for List: hide
-- foreign argument lists. TODO: once the new FFI is fully -- foreign argument lists. TODO: once the new FFI is fully
-- up and running we won't need this. Also, if we add -- up and running we won't need this. Also, if we add
-- 'with' disambiguation we can use that instead. -- 'with' disambiguation we can use that instead.
catch (do hide replFC (NS primIONS (UN "::")) catch (do hide replFC (NS primIONS (UN $ Basic "::"))
hide replFC (NS primIONS (UN "Nil"))) hide replFC (NS primIONS (UN $ Basic "Nil")))
(\err => pure ()) (\err => pure ())
(tm , gty) <- elabTerm inidx emode [] (MkNested []) (tm , gty) <- elabTerm inidx emode [] (MkNested [])
[] ttimpWithIt Nothing [] ttimpWithIt Nothing
@ -745,10 +748,10 @@ process (Eval itm)
then do ity <- resugar [] !(norm defs [] ty) then do ity <- resugar [] !(norm defs [] ty)
pure (Evaluated itm (Just ity)) pure (Evaluated itm (Just ity))
else pure (Evaluated itm Nothing) else pure (Evaluated itm Nothing)
process (Check (PRef fc (UN "it"))) process (Check (PRef fc (UN (Basic "it"))))
= do opts <- get ROpts = do opts <- get ROpts
case evalResultName opts of case evalResultName opts of
Nothing => throw (UndefinedName fc (UN "it")) Nothing => throw (UndefinedName fc (UN $ Basic "it"))
Just n => process (Check (PRef fc n)) Just n => process (Check (PRef fc n))
process (Check (PRef fc fn)) process (Check (PRef fc fn))
= do defs <- get Ctxt = do defs <- get Ctxt

32
src/Idris/Resugar.idr
View File

@ -106,11 +106,11 @@ unbracket tm = tm
||| Attempt to extract a constant natural number ||| Attempt to extract a constant natural number
extractNat : Nat -> IPTerm -> Maybe Nat extractNat : Nat -> IPTerm -> Maybe Nat
extractNat acc tm = case tm of extractNat acc tm = case tm of
PRef _ (MkKindedName _ _ (NS ns (UN n))) => PRef _ (MkKindedName _ _ (NS ns (UN (Basic n)))) =>
do guard (n == "Z") do guard (n == "Z")
guard (ns == typesNS || ns == preludeNS) guard (ns == typesNS || ns == preludeNS)
pure acc 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) "S" => do guard (ns == typesNS || ns == preludeNS)
extractNat (1 + acc) k extractNat (1 + acc) k
"fromInteger" => extractNat acc k "fromInteger" => extractNat acc k
@ -188,9 +188,9 @@ sugarName x = show x
toPRef : FC -> KindedName -> Core IPTerm toPRef : FC -> KindedName -> Core IPTerm
toPRef fc kn@(MkKindedName nt fn nm) = case nm of 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))) 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) Nested _ n => toPRef fc (MkKindedName nt fn n)
_ => pure (sugarApp (PRef fc kn)) _ => pure (sugarApp (PRef fc kn))
@ -218,11 +218,11 @@ mutual
else toPTerm p ret else toPTerm p ret
where where
needsBind : Maybe Name -> Bool needsBind : Maybe Name -> Bool
needsBind (Just (UN t)) needsBind (Just nm@(UN (Basic t)))
= let ret = map rawName ret = let ret = map rawName ret
ns = findBindableNames False [] [] ret ns = findBindableNames False [] [] ret
allNs = findAllNames [] ret in 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 needsBind _ = False
toPTerm p (IPi fc rig pt n arg ret) toPTerm p (IPi fc rig pt n arg ret)
= do arg' <- toPTerm appPrec arg = do arg' <- toPTerm appPrec arg
@ -231,7 +231,7 @@ mutual
bracket p tyPrec (PPi fc rig pt' n arg' ret') bracket p tyPrec (PPi fc rig pt' n arg' ret')
toPTerm p (ILam fc rig pt mn arg sc) toPTerm p (ILam fc rig pt mn arg sc)
= do let n = case mn of = do let n = case mn of
Nothing => UN "_" Nothing => UN Underscore
Just n' => n' Just n' => n'
imp <- showImplicits imp <- showImplicits
arg' <- if imp then toPTerm tyPrec arg arg' <- if imp then toPTerm tyPrec arg
@ -262,8 +262,8 @@ mutual
mkIf : IPTerm -> IPTerm mkIf : IPTerm -> IPTerm
mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [], mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [],
MkPatClause _ (PRef _ fval) f []]) MkPatClause _ (PRef _ fval) f []])
= if dropNS (rawName tval) == UN "True" = if dropNS (rawName tval) == UN (Basic "True")
&& dropNS (rawName fval) == UN "False" && dropNS (rawName fval) == UN (Basic "False")
then PIfThenElse loc sc t f then PIfThenElse loc sc t f
else tm else tm
mkIf tm = tm mkIf tm = tm
@ -304,7 +304,9 @@ mutual
toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c) toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c)
toPTerm p (IHole fc str) = pure (PHole fc False str) toPTerm p (IHole fc str) = pure (PHole fc False str)
toPTerm p (IType fc) = pure (PType fc) 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 (IBindHere fc _ tm) = toPTerm p tm
toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat)) 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)) toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat))
@ -495,19 +497,19 @@ cleanPTerm ptm
cleanName : Name -> Core Name cleanName : Name -> Core Name
cleanName nm = case nm of cleanName nm = case nm of
MN n _ => pure (UN n) MN n _ => pure (UN $ mkUserName n) -- this may be "_"
PV n _ => pure n PV n _ => pure n
DN n _ => pure (UN n) DN n _ => pure (UN $ mkUserName n) -- this may be "_"
NS _ n => cleanName n NS _ n => cleanName n
Nested _ n => cleanName n Nested _ n => cleanName n
RF n => pure (RF n) UN n => pure (UN n)
_ => UN <$> prettyName nm _ => UN . mkUserName <$> prettyName nm
cleanKindedName : KindedName -> Core KindedName cleanKindedName : KindedName -> Core KindedName
cleanKindedName (MkKindedName nt fn nm) = MkKindedName nt fn <$> cleanName nm cleanKindedName (MkKindedName nt fn nm) = MkKindedName nt fn <$> cleanName nm
cleanBinderName : PiInfo IPTerm -> Name -> Core (Maybe Name) 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 cleanBinderName _ nm = Just <$> cleanName nm
cleanNode : IPTerm -> Core IPTerm cleanNode : IPTerm -> Core IPTerm

4
src/Idris/SetOptions.idr
View File

@ -451,11 +451,11 @@ postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest)
= do ignore $ postOptions res rest = do ignore $ postOptions res rest
pure False pure False
postOptions res (OutputFile outfile :: rest) 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 ignore $ postOptions res rest
pure False pure False
postOptions res (ExecFn str :: rest) postOptions res (ExecFn str :: rest)
= do ignore $ execExp (PRef EmptyFC (UN str)) = do ignore $ execExp (PRef EmptyFC (UN $ Basic str))
ignore $ postOptions res rest ignore $ postOptions res rest
pure False pure False
postOptions res (CheckOnly :: rest) postOptions res (CheckOnly :: rest)

21
src/Idris/Syntax.idr
View File

@ -321,17 +321,22 @@ mutual
directiveList : List Directive directiveList : List Directive
directiveList = directiveList =
[ (Hide (UN "")), (Logging Nothing), (LazyOn False) [ (Hide ph), (Logging Nothing), (LazyOn False)
, (UnboundImplicits False), (AmbigDepth 0) , (UnboundImplicits False), (AmbigDepth 0)
, (PairNames (UN "") (UN "") (UN "")), (RewriteName (UN "") (UN "")) , (PairNames ph ph ph), (RewriteName ph ph)
, (PrimInteger (UN "")), (PrimString (UN "")), (PrimChar (UN "")) , (PrimInteger ph), (PrimString ph), (PrimChar ph)
, (PrimDouble (UN "")), (CGAction "" ""), (Names (UN "") []) , (PrimDouble ph), (CGAction "" ""), (Names ph [])
, (StartExpr (PRef EmptyFC (UN ""))), (Overloadable (UN "")) , (StartExpr (PRef EmptyFC ph)), (Overloadable ph)
, (Extension ElabReflection), (DefaultTotality PartialOK) , (Extension ElabReflection), (DefaultTotality PartialOK)
, (PrefixRecordProjections True), (AutoImplicitDepth 0) , (PrefixRecordProjections True), (AutoImplicitDepth 0)
, (NFMetavarThreshold 0), (SearchTimeout 0) , (NFMetavarThreshold 0), (SearchTimeout 0)
] ]
where
-- placeholder
ph : Name
ph = UN $ Basic ""
isPragma : Directive -> Bool isPragma : Directive -> Bool
isPragma (CGAction _ _) = False isPragma (CGAction _ _) = False
isPragma _ = True isPragma _ = True
@ -773,12 +778,12 @@ parameters {0 nm : Type} (toName : nm -> Name)
where where
dePure : PTerm' nm -> PTerm' nm dePure : PTerm' nm -> PTerm' nm
dePure tm@(PApp _ (PRef _ n) arg) 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 dePure tm = tm
deGuard : PDo' nm -> PDo' nm deGuard : PDo' nm -> PDo' nm
deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) 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 deGuard tm = tm
showPTermPrec d (PRewrite _ rule tm) showPTermPrec d (PRewrite _ rule tm)
= "rewrite " ++ showPTermPrec d rule ++ " in " ++ showPTermPrec d tm = "rewrite " ++ showPTermPrec d rule ++ " in " ++ showPTermPrec d tm
@ -987,7 +992,7 @@ initSyntax
initDocStrings initDocStrings
[] []
[] []
(IVar EmptyFC (UN "main")) (IVar EmptyFC (UN $ Basic "main"))
where where

6
src/Libraries/Data/ANameMap.idr
View File

@ -5,7 +5,7 @@ import Core.Name
import Data.List import Data.List
import Libraries.Data.NameMap import Libraries.Data.NameMap
import Libraries.Data.StringMap import Libraries.Data.UserNameMap
%default total %default total
@ -16,7 +16,7 @@ record ANameMap a where
exactNames : NameMap a exactNames : NameMap a
-- for looking up by name root or partially qualified (so possibly -- for looking up by name root or partially qualified (so possibly
-- ambiguous) names. This doesn't store machine generated names. -- ambiguous) names. This doesn't store machine generated names.
hierarchy : StringMap (List (Name, a)) hierarchy : UserNameMap (List (Name, a))
export export
empty : ANameMap a empty : ANameMap a
@ -39,7 +39,7 @@ lookupName n dict
Just ns => filter (matches n . fst) ns Just ns => filter (matches n . fst) ns
addToHier : Name -> a -> addToHier : Name -> a ->
StringMap (List (Name, a)) -> StringMap (List (Name, a)) UserNameMap (List (Name, a)) -> UserNameMap (List (Name, a))
addToHier n val hier addToHier n val hier
-- Only add user defined names. Machine generated names can only be -- Only add user defined names. Machine generated names can only be
-- found with the exactNames -- found with the exactNames

8
src/Libraries/Data/StringMap.idr
View File

@ -2,8 +2,6 @@ module Libraries.Data.StringMap
-- Hand specialised map, for efficiency... -- Hand specialised map, for efficiency...
import Core.Name
%default total %default total
Key : Type Key : Type
@ -219,12 +217,6 @@ lookup : String -> StringMap v -> Maybe v
lookup _ Empty = Nothing lookup _ Empty = Nothing
lookup k (M _ t) = treeLookup k t 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 export
insert : String -> v -> StringMap v -> StringMap v insert : String -> v -> StringMap v -> StringMap v
insert k v Empty = M Z (Leaf k v) insert k v Empty = M Z (Leaf k v)

326
src/Libraries/Data/UserNameMap.idr Normal file
View File

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

16
src/Parser/Lexer/Source.idr
View File

@ -245,16 +245,18 @@ isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
export export
||| Test whether a user name begins with an operator symbol. ||| Test whether a user name begins with an operator symbol.
isOpName : Name -> Bool isOpUserName : UserName -> Bool
isOpName n = fromMaybe False $ do isOpUserName (Basic 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
c <- fst <$> strUncons n c <- fst <$> strUncons n
guard (isOpChar c) guard (isOpChar c)
pure True 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 : Lexer
validSymbol = some (pred isOpChar) validSymbol = some (pred isOpChar)

12
src/Parser/Rule/Source.idr
View File

@ -41,7 +41,7 @@ constant
CharLit c => Ch <$> getCharLit c CharLit c => Ch <$> getCharLit c
DoubleLit d => Just (Db d) DoubleLit d => Just (Db d)
IntegerLit i => Just (BI i) IntegerLit i => Just (BI i)
Ident s => isConstantType (UN s) >>= Ident s => isConstantType (UN $ Basic s) >>=
\case WorldType => Nothing \case WorldType => Nothing
c => Just c c => Just c
_ => Nothing _ => Nothing
@ -140,7 +140,7 @@ aDotIdent = terminal "Expected dot+identifier" $
export export
postfixProj : Rule Name postfixProj : Rule Name
postfixProj = RF <$> aDotIdent postfixProj = UN . Field <$> aDotIdent
export export
symbol : String -> Rule () symbol : String -> Rule ()
@ -188,7 +188,7 @@ operatorCandidate : Rule Name
operatorCandidate operatorCandidate
= terminal "Expected operator" $ = terminal "Expected operator" $
\case \case
Symbol s => Just (UN s) Symbol s => Just (UN $ Basic s) -- TODO: have an operator construct?
_ => Nothing _ => Nothing
export export
@ -199,7 +199,7 @@ operator
Symbol s => Symbol s =>
if s `elem` reservedSymbols if s `elem` reservedSymbols
then Nothing then Nothing
else Just (UN s) else Just (UN $ Basic s) -- TODO: have an operator construct?
_ => Nothing _ => Nothing
identPart : Rule String identPart : Rule String
@ -296,7 +296,7 @@ nameWithCapital b = opNonNS <|> do
let id = snd <$> nsx let id = snd <$> nsx
identWithCapital b id identWithCapital b id
isNotReservedName id isNotReservedName id
pure $ uncurry mkNamespacedName nsx.val pure $ uncurry mkNamespacedName (map Basic nsx.val)
opNS : WithBounds (Maybe Namespace, String) -> Rule Name opNS : WithBounds (Maybe Namespace, String) -> Rule Name
opNS nsx = do opNS nsx = do
@ -325,7 +325,7 @@ capitalisedIdent = do
export export
dataConstructorName : Rule Name dataConstructorName : Rule Name
dataConstructorName = opNonNS <|> UN <$> capitalisedIdent dataConstructorName = opNonNS <|> (UN . Basic) <$> capitalisedIdent
export %inline export %inline
dataTypeName : Rule Name dataTypeName : Rule Name

26
src/TTImp/BindImplicits.idr
View File

@ -19,19 +19,20 @@ export
renameIBinds : (renames : List String) -> renameIBinds : (renames : List String) ->
(used : List String) -> (used : List String) ->
RawImp -> State (List (String, String)) RawImp 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 = if n `elem` rs
then let n' = getUnique (rs ++ us) n then let n' = getUnique (rs ++ us) n
sc' = substNames (map UN (filter (/= n) us)) un' = UN (Basic n')
[(UN n, IVar fc (UN n'))] sc in sc' = substNames (map (UN . Basic) (filter (/= n) us))
[(un, IVar fc un')] sc in
do scr <- renameIBinds rs (n' :: us) sc' do scr <- renameIBinds rs (n' :: us) sc'
ty' <- renameIBinds rs us ty ty' <- renameIBinds rs us ty
upds <- get upds <- get
put ((n, n') :: upds) 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 else do scr <- renameIBinds rs us sc
ty' <- renameIBinds rs us ty 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) renameIBinds rs us (IPi fc c p n ty sc)
= pure $ IPi fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us 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) renameIBinds rs us (ILam fc c p n ty sc)
@ -73,18 +74,18 @@ renameIBinds rs us tm = pure $ tm
export export
doBind : List (String, String) -> RawImp -> RawImp doBind : List (String, String) -> RawImp -> RawImp
doBind [] tm = tm doBind [] tm = tm
doBind ns (IVar fc (UN n)) doBind ns (IVar fc nm@(UN (Basic n)))
= maybe (IVar fc (UN n)) = maybe (IVar fc nm)
(\n' => IBindVar fc n') (IBindVar fc)
(lookup n ns) (lookup n ns)
doBind ns (IPi fc rig p mn aty retty) doBind ns (IPi fc rig p mn aty retty)
= let ns' = case mn of = 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 _ => ns in
IPi fc rig p mn (doBind ns' aty) (doBind ns' retty) IPi fc rig p mn (doBind ns' aty) (doBind ns' retty)
doBind ns (ILam fc rig p mn aty sc) doBind ns (ILam fc rig p mn aty sc)
= let ns' = case mn of = 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 _ => ns in
ILam fc rig p mn (doBind ns' aty) (doBind ns' sc) ILam fc rig p mn (doBind ns' aty) (doBind ns' sc)
doBind ns (IApp fc fn av) doBind ns (IApp fc fn av)
@ -120,7 +121,7 @@ bindNames arg tm
= if !isUnboundImplicits = if !isUnboundImplicits
then do let ns = nub (findBindableNames arg [] [] tm) then do let ns = nub (findBindableNames arg [] [] tm)
log "elab.bindnames" 10 $ "Found names :" ++ show ns 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) else pure ([], tm)
-- if the name is part of the using decls, add the relevant binder for it: -- 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 : List String -> RawImp -> RawImp
piBind [] ty = ty piBind [] ty = ty
piBind (n :: ns) 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

6
src/TTImp/Elab/Ambiguity.idr
View File

@ -18,7 +18,7 @@ import TTImp.TTImp
import Data.List import Data.List
import Data.String import Data.String
import Libraries.Data.StringMap import Libraries.Data.UserNameMap
%default covering %default covering
@ -31,7 +31,7 @@ expandAmbigName : {vars : _} ->
RawImp -> Maybe (Glued vars) -> Core RawImp RawImp -> Maybe (Glued vars) -> Core RawImp
expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp
= do est <- get EST = do est <- get EST
if UN n `elem` lhsPatVars est if UN (Basic n) `elem` lhsPatVars est
then pure $ IMustUnify fc NonLinearVar orig then pure $ IMustUnify fc NonLinearVar orig
else pure $ orig else pure $ orig
expandAmbigName mode nest env orig args (IVar fc x) exp 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) (uniqType primNs x args)
(map (mkAlt primApp est) nalts) (map (mkAlt primApp est) nalts)
where where
lookupUN : Maybe String -> StringMap a -> Maybe a lookupUN : Maybe UserName -> UserNameMap a -> Maybe a
lookupUN Nothing _ = Nothing lookupUN Nothing _ = Nothing
lookupUN (Just n) sm = lookup n sm lookupUN (Just n) sm = lookup n sm

8
src/TTImp/Elab/App.idr
View File

@ -536,14 +536,14 @@ mutual
export export
findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp
findBindAllExpPattern = lookup (UN "_") findBindAllExpPattern = lookup (UN Underscore)
isImplicitAs : RawImp -> Bool isImplicitAs : RawImp -> Bool
isImplicitAs (IAs _ _ UseLeft _ (Implicit _ _)) = True isImplicitAs (IAs _ _ UseLeft _ (Implicit _ _)) = True
isImplicitAs _ = False isImplicitAs _ = False
isBindAllExpPattern : Name -> Bool isBindAllExpPattern : Name -> Bool
isBindAllExpPattern (UN "_") = True isBindAllExpPattern (UN Underscore) = True
isBindAllExpPattern _ = False isBindAllExpPattern _ = False
-- Check an application of 'fntm', with type 'fnty' to the given list -- Check an application of 'fntm', with type 'fnty' to the given list
@ -598,7 +598,7 @@ mutual
then -- We are done then -- We are done
checkExp rig elabinfo env fc tm (glueBack defs env ty) expty 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 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 "<auto>")) autoargs ++ map fst namedargs) tm) throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)
-- Function type is delayed, so force the term and continue -- 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 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 = 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 = do defs <- get Ctxt
if all isImplicitAs (autoargs ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs)) if all isImplicitAs (autoargs ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))
then checkExp rig elabinfo env fc tm (glueBack defs env ty) expty then checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
else throw (InvalidArgs fc env (map (const (UN "<auto>")) autoargs ++ map fst namedargs) tm) else throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)
||| Entrypoint for checkAppWith: run the elaboration first and, if we're ||| Entrypoint for checkAppWith: run the elaboration first and, if we're
||| on the LHS and the result is an under-applied constructor then insist ||| on the LHS and the result is an under-applied constructor then insist

4
src/TTImp/Elab/Case.idr
View File

@ -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 -- so that it applies to the right original variable
getBindName : Int -> Name -> List Name -> (Name, Name) getBindName : Int -> Name -> List Name -> (Name, Name)
getBindName idx n@(UN un) vs 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 getBindName idx n vs
= if n `elem` vs then (n, MN "_cn" idx) else (n, n) = 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 -- Names used in the pattern we're matching on, so don't bind them
-- in the generated case block -- in the generated case block
usedIn : RawImp -> List Name usedIn : RawImp -> List Name
usedIn (IBindVar _ n) = [UN n] usedIn (IBindVar _ n) = [UN $ Basic n]
usedIn (IApp _ f a) = usedIn f ++ usedIn a usedIn (IApp _ f a) = usedIn f ++ usedIn a
usedIn (IAs _ _ _ n a) = n :: usedIn a usedIn (IAs _ _ _ n a) = n :: usedIn a
usedIn (IAlternative _ _ alts) = concatMap usedIn alts usedIn (IAlternative _ _ alts) = concatMap usedIn alts

8
src/TTImp/Elab/Check.idr
View File

@ -20,7 +20,7 @@ import Data.Either
import Libraries.Data.IntMap import Libraries.Data.IntMap
import Data.List import Data.List
import Libraries.Data.NameMap import Libraries.Data.NameMap
import Libraries.Data.StringMap import Libraries.Data.UserNameMap
%default covering %default covering
@ -143,7 +143,7 @@ record EState (vars : List Name) where
linearUsed : List (Var vars) linearUsed : List (Var vars)
saveHoles : NameMap () -- things we'll need to save to TTC, even if solved 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. -- Mapping from userNameRoot to fully resolved names.
-- For names in this mapping, we don't run disambiguation. -- For names in this mapping, we don't run disambiguation.
-- Used in with-expressions. -- Used in with-expressions.
@ -547,7 +547,7 @@ successful allowCons ((tm, elab) :: elabs)
defs <- branch defs <- branch
catch (do -- Run the elaborator catch (do -- Run the elaborator
logC "elab" 5 $ logC "elab" 5 $
do tm' <- maybe (pure (UN "__")) do tm' <- maybe (pure (UN $ Basic "__"))
toFullNames tm toFullNames tm
pure ("Running " ++ show tm') pure ("Running " ++ show tm')
res <- elab res <- elab
@ -567,7 +567,7 @@ successful allowCons ((tm, elab) :: elabs)
put MD md put MD md
put Ctxt defs put Ctxt defs
logC "elab" 5 $ logC "elab" 5 $
do tm' <- maybe (pure (UN "__")) do tm' <- maybe (pure (UN $ Basic "__"))
toFullNames tm toFullNames tm
pure ("Success " ++ show tm' ++ pure ("Success " ++ show tm' ++
" (" ++ show ncons' ++ " - " " (" ++ show ncons' ++ " - "

4
src/TTImp/Elab/Hole.idr
View File

@ -35,7 +35,7 @@ checkHole : {vars : _} ->
{auto e : Ref EST (EState vars)} -> {auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo -> RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars -> NestedNames vars -> Env Term vars ->
FC -> String -> Maybe (Glued vars) -> FC -> UserName -> Maybe (Glued vars) ->
Core (Term vars, Glued vars) Core (Term vars, Glued vars)
checkHole rig elabinfo nest env fc n_in (Just gexpty) checkHole rig elabinfo nest env fc n_in (Just gexpty)
= do nm <- inCurrentNS (UN n_in) = do nm <- inCurrentNS (UN n_in)
@ -58,7 +58,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
saveHole nm saveHole nm
pure (metaval, gexpty) pure (metaval, gexpty)
checkHole rig elabinfo nest env fc n_in exp 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 let env' = letToLam env
ty <- metaVar fc erased env' nmty (TType fc) ty <- metaVar fc erased env' nmty (TType fc)
nm <- inCurrentNS (UN n_in) nm <- inCurrentNS (UN n_in)

2
src/TTImp/Elab/ImplicitBind.idr
View File

@ -401,7 +401,7 @@ checkBindVar : {vars : _} ->
{auto e : Ref EST (EState vars)} -> {auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo -> RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars -> 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) -> Maybe (Glued vars) ->
Core (Term vars, Glued vars) Core (Term vars, Glued vars)
checkBindVar rig elabinfo nest env fc str topexp checkBindVar rig elabinfo nest env fc str topexp

9
src/TTImp/Elab/Record.idr
View File

@ -44,7 +44,7 @@ applyImp f ((Just n, arg) :: xs)
toLHS' : FC -> Rec -> (Maybe Name, RawImp) toLHS' : FC -> Rec -> (Maybe Name, RawImp)
toLHS' loc (Field mn@(Just _) n _) 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 (Field mn n _) = (mn, IBindVar EmptyFC n)
toLHS' loc (Constr mn con args) toLHS' loc (Constr mn con args)
= let args' = map (toLHS' loc . snd) args in = 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 = do fldn <- genFieldName p
args' <- mkArgs ps args' <- mkArgs ps
-- If it's an implicit argument, leave it as _ by default -- 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)) (const (Implicit loc False))
imp imp
pure ((p, Field imp fldn arg) :: args') 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' -- then set the path on the rhs to 'val'
= findPath loc path path (Just tyn) (const val) rec = findPath loc path path (Just tyn) (const val) rec
getSides loc (ISetFieldApp path val) tyn orig 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} -> getAllSides : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
@ -184,7 +185,7 @@ recUpdate rigc elabinfo iloc nest env flds rec grecty
| Nothing => throw (RecordTypeNeeded iloc env) | Nothing => throw (RecordTypeNeeded iloc env)
fldn <- genFieldName "__fld" fldn <- genFieldName "__fld"
sides <- getAllSides iloc flds rectyn rec 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] pure $ ICase vloc rec (Implicit vloc False) [mkClause sides]
where where
vloc : FC vloc : FC

6
src/TTImp/Elab/RunElab.idr
View File

@ -35,7 +35,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
= do defs <- get Ctxt = do defs <- get Ctxt
fnm <- toFullNames nm fnm <- toFullNames nm
case fnm of case fnm of
NS ns (UN n) NS ns (UN (Basic n))
=> if ns == reflectionNS => if ns == reflectionNS
then elabCon defs n (map snd args) then elabCon defs n (map snd args)
else failWith defs $ "bad reflection namespace " ++ show ns 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] elabCon defs "Check" [exp, ttimp]
= do exp' <- evalClosure defs exp = do exp' <- evalClosure defs exp
ttimp' <- evalClosure defs ttimp ttimp' <- evalClosure defs ttimp
tidx <- resolveName (UN "[elaborator script]") tidx <- resolveName (UN $ Basic "[elaborator script]")
e <- newRef EST (initEState tidx env) e <- newRef EST (initEState tidx env)
(checktm, _) <- runDelays (const True) $ (checktm, _) <- runDelays (const True) $
check top (initElabInfo InExpr) nest env !(reify defs ttimp') check top (initElabInfo InExpr) nest env !(reify defs ttimp')
@ -190,7 +190,7 @@ checkRunElab rig elabinfo nest env fc script exp
defs <- get Ctxt defs <- get Ctxt
unless (isExtension ElabReflection defs) $ unless (isExtension ElabReflection defs) $
throw (GenericMsg fc "%language ElabReflection not enabled") throw (GenericMsg fc "%language ElabReflection not enabled")
let n = NS reflectionNS (UN "Elab") let n = NS reflectionNS (UN $ Basic "Elab")
let ttn = reflectiontt "TT" let ttn = reflectiontt "TT"
elabtt <- appCon fc defs n [expected] elabtt <- appCon fc defs n [expected]
(stm, sty) <- runDelays (const True) $ (stm, sty) <- runDelays (const True) $

10
src/TTImp/Elab/Term.idr
View File

@ -1,6 +1,6 @@
module TTImp.Elab.Term module TTImp.Elab.Term
import Libraries.Data.StringMap import Libraries.Data.UserNameMap
import Core.Context import Core.Context
import Core.Core import Core.Core
@ -133,7 +133,7 @@ checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
AutoImplicit => genVarName "conArg" AutoImplicit => genVarName "conArg"
(DefImplicit _) => genVarName "defArg" (DefImplicit _) => genVarName "defArg"
checkPi rig elabinfo nest env fc r p n argTy retTy exp 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 Nothing argTy retTy) exp
checkTerm rig elabinfo nest env (IPi fc r p (Just n) 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 = 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 checkTerm rig elabinfo nest env (IBindHere fc binder sc) exp
= checkBindHere rig elabinfo nest env fc binder sc exp = checkBindHere rig elabinfo nest env fc binder sc exp
checkTerm rig elabinfo nest env (IBindVar fc n) 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 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 = checkAs rig elabinfo nest env fc nameFC side n_in tm exp
checkTerm rig elabinfo nest env (IMustUnify fc reason 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 = checkExp rig elabinfo env fc (TType fc) (gType fc) exp
checkTerm rig elabinfo nest env (IHole fc str) 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 checkTerm rig elabinfo nest env (IUnifyLog fc lvl tm) exp
= withLogLevel lvl $ check rig elabinfo nest env tm exp = withLogLevel lvl $ check rig elabinfo nest env tm exp
checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty) 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 pure result
where 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 [] = pure empty
resolveNames fc (n :: ns) = resolveNames fc (n :: ns) =
case userNameRoot n of case userNameRoot n of

8
src/TTImp/Interactive/CaseSplit.idr
View File

@ -122,7 +122,7 @@ unique : List String -> List String -> Int -> List Name -> String
unique [] supply suff usedns = unique supply supply (suff + 1) usedns unique [] supply suff usedns = unique supply supply (suff + 1) usedns
unique (str :: next) supply suff usedns unique (str :: next) supply suff usedns
= let var = mkVarN str suff in = let var = mkVarN str suff in
if UN var `elem` usedns if UN (Basic var) `elem` usedns
then unique next supply suff usedns then unique next supply suff usedns
else var else var
where where
@ -154,7 +154,7 @@ getArgName defs x bound allvars ty
else lookupName n ts else lookupName n ts
notBound : String -> Bool 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 : NF vars -> Core (List String)
findNames (NBind _ x (Pi _ _ _ _) _) findNames (NBind _ x (Pi _ _ _ _) _)
@ -166,7 +166,7 @@ getArgName defs x bound allvars ty
findNames ty = pure (filter notBound defaultNames) findNames ty = pure (filter notBound defaultNames)
getName : Name -> List String -> List Name -> String 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 getName _ defs used = unique defs defs 0 used
export 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))] Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))]
_ => pure [] _ => pure []
sc' <- sc defs (toClosure defaultOpts env (Erased fc False)) 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 [] getArgNames defs bound allvars env val = pure []
export export

4
src/TTImp/Interactive/ExprSearch.idr
View File

@ -364,7 +364,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty all
(\r => nameRoot (recname r) ++ "_rhs") (\r => nameRoot (recname r) ++ "_rhs")
(recData opts) (recData opts)
hn <- uniqueName defs (map nameRoot vars) base 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)) (Hole (length env) (holeInit False))
False False
one (tm, []) 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 getSuccessful fc rig opts False env ty topty
[searchLocal fc rig opts env (Bind bfc n b sc) topty, [searchLocal fc rig opts env (Bind bfc n b sc) topty,
(do defs <- get Ctxt (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 env' : Env Term (n' :: _) = b :: env
let sc' = renameTop n' sc let sc' = renameTop n' sc
log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc' log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc'

8
src/TTImp/Interactive/GenerateDef.idr
View File

@ -28,7 +28,7 @@ import Data.List
%default covering %default covering
fnName : Bool -> Name -> String fnName : Bool -> Name -> String
fnName lhs (UN n) fnName lhs (UN (Basic n))
= if isIdentNormal n then n = if isIdentNormal n then n
else if lhs then "(" ++ n ++ ")" else if lhs then "(" ++ n ++ ")"
else "op" else "op"
@ -89,7 +89,7 @@ expandClause loc opts n c
splittableNames : RawImp -> List Name splittableNames : RawImp -> List Name
splittableNames (IApp _ f (IBindVar _ n)) splittableNames (IApp _ f (IBindVar _ n))
= splittableNames f ++ [UN n] = splittableNames f ++ [UN $ Basic n]
splittableNames (IApp _ f _) splittableNames (IApp _ f _)
= splittableNames f = splittableNames f
splittableNames (IAutoApp _ f _) splittableNames (IAutoApp _ f _)
@ -114,7 +114,7 @@ trySplit loc lhsraw lhs rhs n
valid _ = Nothing valid _ = Nothing
fixNames : RawImp -> RawImp 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 (IVar loc' (MN _ _)) = Implicit loc' True
fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a) fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a)
fixNames (IAutoApp loc' f a) = IAutoApp 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 Nothing => IVar loc' n
Just tm => fixNames tm Just tm => fixNames tm
updateLHS ups (IBindVar loc' n) updateLHS ups (IBindVar loc' n)
= case lookup (UN n) ups of = case lookup (UN (Basic n)) ups of
Nothing => IBindVar loc' n Nothing => IBindVar loc' n
Just tm => fixNames tm Just tm => fixNames tm
updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a) updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a)

2
src/TTImp/Interactive/MakeLemma.idr
View File

@ -47,7 +47,7 @@ getArgs : {vars : _} ->
getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc) getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc)
= do defs <- get Ctxt = do defs <- get Ctxt
ty' <- map (map rawName) $ unelab env !(normalise defs env ty) 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) (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 -- Don't need to use the name if it's not used in the scope type
let mn = if c == top let mn = if c == top

21
src/TTImp/Parser.idr
View File

@ -180,15 +180,15 @@ mutual
implicitArg fname indents implicitArg fname indents
= do start <- location = do start <- location
symbol "{" symbol "{"
x <- unqualifiedName x <- UN . Basic <$> unqualifiedName
(do symbol "=" (do symbol "="
commit commit
tm <- expr fname indents tm <- expr fname indents
symbol "}" symbol "}"
pure (Just (UN x), tm)) pure (Just x, tm))
<|> (do symbol "}" <|> (do symbol "}"
end <- location end <- location
pure (Just (UN x), IVar (MkFC fname start end) (UN x))) pure (Just x, IVar (MkFC fname start end) x))
<|> do symbol "@{" <|> do symbol "@{"
commit commit
tm <- expr fname indents tm <- expr fname indents
@ -198,12 +198,12 @@ mutual
as : OriginDesc -> IndentInfo -> Rule RawImp as : OriginDesc -> IndentInfo -> Rule RawImp
as fname indents as fname indents
= do start <- location = do start <- location
x <- unqualifiedName x <- UN . Basic <$> unqualifiedName
nameEnd <- location nameEnd <- location
symbol "@" symbol "@"
pat <- simpleExpr fname indents pat <- simpleExpr fname indents
end <- location 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 : OriginDesc -> IndentInfo -> Rule RawImp
simpleExpr fname indents simpleExpr fname indents
@ -247,7 +247,7 @@ mutual
(do symbol ":" (do symbol ":"
appExpr fname indents) appExpr fname indents)
rig <- getMult rigc rig <- getMult rigc
pure (rig, UN n, ty)) pure (rig, UN (Basic n), ty))
pibindListName : OriginDesc -> FilePos -> IndentInfo -> pibindListName : OriginDesc -> FilePos -> IndentInfo ->
@ -259,7 +259,7 @@ mutual
ty <- expr fname indents ty <- expr fname indents
atEnd indents atEnd indents
rig <- getMult rigc 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 ",") <|> forget <$> sepBy1 (symbol ",")
(do rigc <- multiplicity (do rigc <- multiplicity
n <- name n <- name
@ -297,7 +297,10 @@ mutual
ns <- sepBy1 (symbol ",") unqualifiedName ns <- sepBy1 (symbol ",") unqualifiedName
nend <- location nend <- location
let nfc = MkFC fname nstart nend 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 "." symbol "."
scope <- typeExpr fname indents scope <- typeExpr fname indents
end <- location end <- location
@ -628,7 +631,7 @@ fieldDecl fname indents
ty <- expr fname indents ty <- expr fname indents
end <- location end <- location
pure (map (\n => MkIField (MkFC fname start end) 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 : OriginDesc -> IndentInfo -> Rule ImpDecl
recordDecl fname indents recordDecl fname indents

10
src/TTImp/PartialEval.idr
View File

@ -142,11 +142,11 @@ getSpecPats fc pename fn stk fnty args sargs pats
mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app (a :: as) ((_, Dynamic) :: ds) mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app (a :: as) ((_, Dynamic) :: ds)
= do defs <- get Ctxt = do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) 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) mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app (a :: as) ((_, Dynamic) :: ds)
= do defs <- get Ctxt = do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) 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) mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app as ((_, Static tm) :: ds)
= do defs <- get Ctxt = do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) 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 -- Type will depend on the value here (we assume a variadic function) but
-- the argument names are still needed -- the argument names are still needed
mkRHSargs ty app (a :: as) ((_, Dynamic) :: ds) 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 _ _ mkRHSargs _ app _ _
= pure app = pure app
@ -293,7 +293,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
getAllRefs : NameMap Bool -> List ArgMode -> NameMap Bool getAllRefs : NameMap Bool -> List ArgMode -> NameMap Bool
getAllRefs ns (Dynamic :: xs) = getAllRefs ns xs getAllRefs ns (Dynamic :: xs) = getAllRefs ns xs
getAllRefs ns (Static t :: xs) getAllRefs ns (Static t :: xs)
= addRefs False (UN "_") (getAllRefs ns xs) t = addRefs False (UN Underscore) (getAllRefs ns xs) t
getAllRefs ns [] = ns getAllRefs ns [] = ns
updateApp : Name -> RawImp -> RawImp updateApp : Name -> RawImp -> RawImp
@ -364,7 +364,7 @@ specialise {vars} fc env gdef fn stk
let nhash = hash (mapMaybe getStatic (map snd sargs)) let nhash = hash (mapMaybe getStatic (map snd sargs))
`hashWithSalt` fn -- add function name to hash to avoid namespace clashes `hashWithSalt` fn -- add function name to hash to avoid namespace clashes
let pename = NS partialEvalNS let pename = NS partialEvalNS
(UN ("PE_" ++ nameRoot fnfull ++ "_" ++ asHex nhash)) (UN $ Basic ("PE_" ++ nameRoot fnfull ++ "_" ++ asHex nhash))
defs <- get Ctxt defs <- get Ctxt
case lookup pename (peFailures defs) of case lookup pename (peFailures defs) of
Nothing => Just <$> mkSpecDef fc gdef pename sargs fn stk Nothing => Just <$> mkSpecDef fc gdef pename sargs fn stk

10
src/TTImp/ProcessDef.idr
View File

@ -589,8 +589,8 @@ checkClause {vars} mult vis totreq hashit n opts nest env
Nothing => [] Nothing => []
Just _ => Just _ =>
let fc = emptyFC in let fc = emptyFC in
let refl = IVar fc (NS builtinNS (UN "Refl")) in let refl = IVar fc (NS builtinNS (UN $ Basic "Refl")) in
[(mprf, INamedApp fc refl (UN "x") wval_raw)] [(mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)]
let rhs_in = gapply (IVar vfc wname) let rhs_in = gapply (IVar vfc wname)
$ map (\ nm => (Nothing, IVar vfc nm)) envns $ 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 bindWithArgs {xs} wvalTy (Just (name, wval)) wvalEnv = do
defs <- get Ctxt defs <- get Ctxt
let eqName = NS builtinNS (UN "Equal") let eqName = NS builtinNS (UN $ Basic "Equal")
Just (TCon t ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs) Just (TCon t ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs)
| _ => throw (InternalError "Cannot find builtin Equal") | _ => throw (InternalError "Cannot find builtin Equal")
let eqTyCon = Ref vfc (TyCon t ar) !(toResolvedNames eqName) let eqTyCon = Ref vfc (TyCon t ar) !(toResolvedNames eqName)
@ -830,7 +830,7 @@ mkRunTime fc n
mkCrash : {vars : _} -> String -> Term vars mkCrash : {vars : _} -> String -> Term vars
mkCrash msg 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)] [Erased fc False, PrimVal fc (Str msg)]
matchAny : Term vars -> Term vars matchAny : Term vars -> Term vars
@ -954,7 +954,7 @@ processDef opts nest env fc n_in cs_in
defs <- get Ctxt defs <- get Ctxt
put Ctxt (record { toCompileCase $= (n ::) } defs) 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)) $ when (not (InCase `elem` opts)) $
do calcRefs False atotal (Resolved nidx) do calcRefs False atotal (Resolved nidx)
sc <- calculateSizeChange fc n sc <- calculateSizeChange fc n

8
src/TTImp/ProcessRecord.idr
View File

@ -136,8 +136,8 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
upds (b :: tyenv) sc upds (b :: tyenv) sc
else else
do let fldNameStr = nameRoot n do let fldNameStr = nameRoot n
rfNameNS <- inCurrentNS (RF fldNameStr) rfNameNS <- inCurrentNS (UN $ Field fldNameStr)
unNameNS <- inCurrentNS (UN fldNameStr) unNameNS <- inCurrentNS (UN $ Basic fldNameStr)
let nestDrop let nestDrop
= map (\ (n, (_, ns, _)) => (n, length ns)) = 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) let lhs = IApp bfc (IVar bfc rfNameNS)
(if imp == Explicit (if imp == Explicit
then lhs_exp then lhs_exp
else INamedApp bfc lhs_exp (UN fldNameStr) else INamedApp bfc lhs_exp (UN $ Basic fldNameStr)
(IBindVar bfc 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 log "declare.record.projection" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs
processDecl [] nest env processDecl [] nest env
(IDef bfc rfNameNS [PatClause bfc lhs rhs]) (IDef bfc rfNameNS [PatClause bfc lhs rhs])

4
src/TTImp/ProcessRunElab.idr
View File

@ -28,8 +28,8 @@ processRunElab eopts nest env fc tm
= do defs <- get Ctxt = do defs <- get Ctxt
unless (isExtension ElabReflection defs) $ unless (isExtension ElabReflection defs) $
throw (GenericMsg fc "%language ElabReflection not enabled") throw (GenericMsg fc "%language ElabReflection not enabled")
tidx <- resolveName (UN "[elaborator script]") tidx <- resolveName (UN $ Basic "[elaborator script]")
let n = NS reflectionNS (UN "Elab") let n = NS reflectionNS (UN $ Basic "Elab")
unit <- getCon fc defs (builtin "Unit") unit <- getCon fc defs (builtin "Unit")
exp <- appCon fc defs n [unit] exp <- appCon fc defs n [unit]

4
src/TTImp/ProcessType.idr
View File

@ -91,7 +91,7 @@ processFnOpt fc _ ndef (SpecArgs ns)
then collectDDeps sc' then collectDDeps sc'
else do aty <- quote empty [] nty else do aty <- quote empty [] nty
-- Get names depended on by nty -- Get names depended on by nty
let deps = keys (getRefs (UN "_") aty) let deps = keys (getRefs (UN Underscore) aty)
rest <- collectDDeps sc' rest <- collectDDeps sc'
pure (rest ++ deps) pure (rest ++ deps)
collectDDeps _ = pure [] collectDDeps _ = pure []
@ -184,7 +184,7 @@ getFnString : {auto c : Ref Ctxt Defs} ->
RawImp -> Core String RawImp -> Core String
getFnString (IPrimVal _ (Str st)) = pure st getFnString (IPrimVal _ (Str st)) = pure st
getFnString tm getFnString tm
= do inidx <- resolveName (UN "[foreign]") = do inidx <- resolveName (UN $ Basic "[foreign]")
let fc = getFC tm let fc = getFC tm
let gstr = gnf [] (PrimVal fc StringType) let gstr = gnf [] (PrimVal fc StringType)
etm <- checkTerm inidx InExpr [] (MkNested []) [] tm gstr etm <- checkTerm inidx InExpr [] (MkNested []) [] tm gstr

188
src/TTImp/Reflect.idr
View File

@ -14,12 +14,12 @@ import TTImp.TTImp
export export
Reify BindMode where Reify BindMode where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "PI"), [(_, c)]) (UN (Basic "PI"), [(_, c)])
=> do c' <- reify defs !(evalClosure defs c) => do c' <- reify defs !(evalClosure defs c)
pure (PI c') pure (PI c')
(NS _ (UN "PATTERN"), _) => pure PATTERN (UN (Basic "PATTERN"), _) => pure PATTERN
(NS _ (UN "NONE"), _) => pure NONE (UN (Basic "NONE"), _) => pure NONE
_ => cantReify val "BindMode" _ => cantReify val "BindMode"
reify deva val = cantReify val "BindMode" reify deva val = cantReify val "BindMode"
@ -36,9 +36,9 @@ Reflect BindMode where
export export
Reify UseSide where Reify UseSide where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "UseLeft"), _) => pure UseLeft (UN (Basic "UseLeft"), _) => pure UseLeft
(NS _ (UN "UseRight"), _) => pure UseRight (UN (Basic "UseRight"), _) => pure UseRight
_ => cantReify val "UseSide" _ => cantReify val "UseSide"
reify defs val = cantReify val "UseSide" reify defs val = cantReify val "UseSide"
@ -52,14 +52,14 @@ Reflect UseSide where
export export
Reify DotReason where Reify DotReason where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "NonLinearVar"), _) => pure NonLinearVar (UN (Basic "NonLinearVar"), _) => pure NonLinearVar
(NS _ (UN "VarApplied"), _) => pure VarApplied (UN (Basic "VarApplied"), _) => pure VarApplied
(NS _ (UN "NotConstructor"), _) => pure NotConstructor (UN (Basic "NotConstructor"), _) => pure NotConstructor
(NS _ (UN "ErasedArg"), _) => pure ErasedArg (UN (Basic "ErasedArg"), _) => pure ErasedArg
(NS _ (UN "UserDotted"), _) => pure UserDotted (UN (Basic "UserDotted"), _) => pure UserDotted
(NS _ (UN "UnknownDot"), _) => pure UnknownDot (UN (Basic "UnknownDot"), _) => pure UnknownDot
(NS _ (UN "UnderAppliedCon"), _) => pure UnderAppliedCon (UN (Basic "UnderAppliedCon"), _) => pure UnderAppliedCon
_ => cantReify val "DotReason" _ => cantReify val "DotReason"
reify defs val = cantReify val "DotReason" reify defs val = cantReify val "DotReason"
@ -85,12 +85,12 @@ mutual
export export
Reify RawImp where Reify RawImp where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "IVar"), [fc, n]) (UN (Basic "IVar"), [fc, n])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (IVar fc' 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) => do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c) c' <- reify defs !(evalClosure defs c)
p' <- reify defs !(evalClosure defs p) p' <- reify defs !(evalClosure defs p)
@ -98,7 +98,7 @@ mutual
aty' <- reify defs !(evalClosure defs aty) aty' <- reify defs !(evalClosure defs aty)
rty' <- reify defs !(evalClosure defs rty) rty' <- reify defs !(evalClosure defs rty)
pure (IPi fc' c' p' mn' aty' 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) => do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c) c' <- reify defs !(evalClosure defs c)
p' <- reify defs !(evalClosure defs p) p' <- reify defs !(evalClosure defs p)
@ -106,7 +106,7 @@ mutual
aty' <- reify defs !(evalClosure defs aty) aty' <- reify defs !(evalClosure defs aty)
lty' <- reify defs !(evalClosure defs lty) lty' <- reify defs !(evalClosure defs lty)
pure (ILam fc' c' p' mn' aty' 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) => do fc' <- reify defs !(evalClosure defs fc)
lhsFC' <- reify defs !(evalClosure defs lhsFC) lhsFC' <- reify defs !(evalClosure defs lhsFC)
c' <- reify defs !(evalClosure defs c) c' <- reify defs !(evalClosure defs c)
@ -115,123 +115,123 @@ mutual
val' <- reify defs !(evalClosure defs val) val' <- reify defs !(evalClosure defs val)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (ILet fc' lhsFC' c' n' ty' val' 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) => do fc' <- reify defs !(evalClosure defs fc)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
ty' <- reify defs !(evalClosure defs ty) ty' <- reify defs !(evalClosure defs ty)
cs' <- reify defs !(evalClosure defs cs) cs' <- reify defs !(evalClosure defs cs)
pure (ICase fc' sc' ty' 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) => do fc' <- reify defs !(evalClosure defs fc)
ds' <- reify defs !(evalClosure defs ds) ds' <- reify defs !(evalClosure defs ds)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (ILocal fc' ds' 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) => do fc' <- reify defs !(evalClosure defs fc)
ds' <- reify defs !(evalClosure defs ds) ds' <- reify defs !(evalClosure defs ds)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (IUpdate fc' ds' 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) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (IApp fc' f' 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) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
m' <- reify defs !(evalClosure defs m) m' <- reify defs !(evalClosure defs m)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (INamedApp fc' f' m' 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) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (IAutoApp fc' f' 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) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (IWithApp fc' f' a') pure (IWithApp fc' f' a')
(NS _ (UN "ISearch"), [fc, d]) (UN (Basic "ISearch"), [fc, d])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
d' <- reify defs !(evalClosure defs d) d' <- reify defs !(evalClosure defs d)
pure (ISearch fc' d') pure (ISearch fc' d')
(NS _ (UN "IAlternative"), [fc, t, as]) (UN (Basic "IAlternative"), [fc, t, as])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
as' <- reify defs !(evalClosure defs as) as' <- reify defs !(evalClosure defs as)
pure (IAlternative fc' t' 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) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (IRewrite fc' t' 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) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (IBindHere fc' t' sc') pure (IBindHere fc' t' sc')
(NS _ (UN "IBindVar"), [fc, n]) (UN (Basic "IBindVar"), [fc, n])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (IBindVar fc' 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) => do fc' <- reify defs !(evalClosure defs fc)
nameFC' <- reify defs !(evalClosure defs nameFC) nameFC' <- reify defs !(evalClosure defs nameFC)
s' <- reify defs !(evalClosure defs s) s' <- reify defs !(evalClosure defs s)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IAs fc' nameFC' s' n' 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) => do fc' <- reify defs !(evalClosure defs fc)
r' <- reify defs !(evalClosure defs r) r' <- reify defs !(evalClosure defs r)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IMustUnify fc' r' 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) => do fc' <- reify defs !(evalClosure defs fc)
r' <- reify defs !(evalClosure defs r) r' <- reify defs !(evalClosure defs r)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IDelayed fc' r' t') pure (IDelayed fc' r' t')
(NS _ (UN "IDelay"), [fc, t]) (UN (Basic "IDelay"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IDelay fc' t') pure (IDelay fc' t')
(NS _ (UN "IForce"), [fc, t]) (UN (Basic "IForce"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IForce fc' t') pure (IForce fc' t')
(NS _ (UN "IQuote"), [fc, t]) (UN (Basic "IQuote"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IQuote fc' t') pure (IQuote fc' t')
(NS _ (UN "IQuoteName"), [fc, t]) (UN (Basic "IQuoteName"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IQuoteName fc' t') pure (IQuoteName fc' t')
(NS _ (UN "IQuoteDecl"), [fc, t]) (UN (Basic "IQuoteDecl"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IQuoteDecl fc' t') pure (IQuoteDecl fc' t')
(NS _ (UN "IUnquote"), [fc, t]) (UN (Basic "IUnquote"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IUnquote fc' t') pure (IUnquote fc' t')
(NS _ (UN "IPrimVal"), [fc, t]) (UN (Basic "IPrimVal"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IPrimVal fc' t') pure (IPrimVal fc' t')
(NS _ (UN "IType"), [fc]) (UN (Basic "IType"), [fc])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
pure (IType fc') pure (IType fc')
(NS _ (UN "IHole"), [fc, n]) (UN (Basic "IHole"), [fc, n])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (IHole fc' n') pure (IHole fc' n')
(NS _ (UN "Implicit"), [fc, n]) (UN (Basic "Implicit"), [fc, n])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (Implicit fc' n') pure (Implicit fc' n')
(NS _ (UN "IWithUnambigNames"), [fc, ns, t]) (UN (Basic "IWithUnambigNames"), [fc, ns, t])
=> do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
ns' <- reify defs !(evalClosure defs ns) ns' <- reify defs !(evalClosure defs ns)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
@ -242,12 +242,12 @@ mutual
export export
Reify IFieldUpdate where Reify IFieldUpdate where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "ISetField"), [(_, x), (_, y)]) (UN (Basic "ISetField"), [(_, x), (_, y)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (ISetField x' y') pure (ISetField x' y')
(NS _ (UN "ISetFieldApp"), [(_, x), (_, y)]) (UN (Basic "ISetFieldApp"), [(_, x), (_, y)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (ISetFieldApp x' y') pure (ISetFieldApp x' y')
@ -257,12 +257,12 @@ mutual
export export
Reify AltType where Reify AltType where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "FirstSuccess"), _) (UN (Basic "FirstSuccess"), _)
=> pure FirstSuccess => pure FirstSuccess
(NS _ (UN "Unique"), _) (UN (Basic "Unique"), _)
=> pure Unique => pure Unique
(NS _ (UN "UniqueDefault"), [(_, x)]) (UN (Basic "UniqueDefault"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (UniqueDefault x') pure (UniqueDefault x')
_ => cantReify val "AltType" _ => cantReify val "AltType"
@ -271,25 +271,25 @@ mutual
export export
Reify FnOpt where Reify FnOpt where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "Inline"), _) => pure Inline (UN (Basic "Inline"), _) => pure Inline
(NS _ (UN "TCInline"), _) => pure TCInline (UN (Basic "TCInline"), _) => pure TCInline
(NS _ (UN "Hint"), [(_, x)]) (UN (Basic "Hint"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Hint x') pure (Hint x')
(NS _ (UN "GlobalHint"), [(_, x)]) (UN (Basic "GlobalHint"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (GlobalHint x') pure (GlobalHint x')
(NS _ (UN "ExternFn"), _) => pure ExternFn (UN (Basic "ExternFn"), _) => pure ExternFn
(NS _ (UN "ForeignFn"), [(_, x)]) (UN (Basic "ForeignFn"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (ForeignFn x') pure (ForeignFn x')
(NS _ (UN "Invertible"), _) => pure Invertible (UN (Basic "Invertible"), _) => pure Invertible
(NS _ (UN "Totality"), [(_, x)]) (UN (Basic "Totality"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Totality x') pure (Totality x')
(NS _ (UN "Macro"), _) => pure Macro (UN (Basic "Macro"), _) => pure Macro
(NS _ (UN "SpecArgs"), [(_, x)]) (UN (Basic "SpecArgs"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (SpecArgs x') pure (SpecArgs x')
_ => cantReify val "FnOpt" _ => cantReify val "FnOpt"
@ -298,8 +298,8 @@ mutual
export export
Reify ImpTy where Reify ImpTy where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "MkTy"), [w, x, y, z]) (UN (Basic "MkTy"), [w, x, y, z])
=> do w' <- reify defs !(evalClosure defs w) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
@ -311,29 +311,29 @@ mutual
export export
Reify DataOpt where Reify DataOpt where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), args) of = case (dropAllNS !(full (gamma defs) n), args) of
(NS _ (UN "SearchBy"), [(_, x)]) (UN (Basic "SearchBy"), [(_, x)])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (SearchBy x') pure (SearchBy x')
(NS _ (UN "NoHints"), _) => pure NoHints (UN (Basic "NoHints"), _) => pure NoHints
(NS _ (UN "UniqueSearch"), _) => pure UniqueSearch (UN (Basic "UniqueSearch"), _) => pure UniqueSearch
(NS _ (UN "External"), _) => pure External (UN (Basic "External"), _) => pure External
(NS _ (UN "NoNewtype"), _) => pure NoNewtype (UN (Basic "NoNewtype"), _) => pure NoNewtype
_ => cantReify val "DataOpt" _ => cantReify val "DataOpt"
reify defs val = cantReify val "DataOpt" reify defs val = cantReify val "DataOpt"
export export
Reify ImpData where Reify ImpData where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "MkData"), [v,w,x,y,z]) (UN (Basic "MkData"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v) => do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (MkImpData v' w' x' y' 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) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
@ -344,8 +344,8 @@ mutual
export export
Reify IField where Reify IField where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "MkIField"), [v,w,x,y,z]) (UN (Basic "MkIField"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v) => do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
@ -358,8 +358,8 @@ mutual
export export
Reify ImpRecord where Reify ImpRecord where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "MkRecord"), [v,w,x,y,z]) (UN (Basic "MkRecord"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v) => do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
@ -372,8 +372,8 @@ mutual
export export
Reify WithFlag where Reify WithFlag where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "Syntactic"), []) (UN (Basic "Syntactic"), [])
=> pure Syntactic => pure Syntactic
_ => cantReify val "WithFlag" _ => cantReify val "WithFlag"
reify defs val = cantReify val "WithFlag" reify defs val = cantReify val "WithFlag"
@ -381,13 +381,13 @@ mutual
export export
Reify ImpClause where Reify ImpClause where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "PatClause"), [x,y,z]) (UN (Basic "PatClause"), [x,y,z])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (PatClause x' y' 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) => do u' <- reify defs !(evalClosure defs u)
v' <- reify defs !(evalClosure defs v) v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
@ -395,7 +395,7 @@ mutual
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (WithClause u' v' w' x' y' 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) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (ImpossibleClause x' y') pure (ImpossibleClause x' y')
@ -405,47 +405,47 @@ mutual
export export
Reify ImpDecl where Reify ImpDecl where
reify defs val@(NDCon _ n _ _ args) reify defs val@(NDCon _ n _ _ args)
= case (!(full (gamma defs) n), map snd args) of = case (dropAllNS !(full (gamma defs) n), map snd args) of
(NS _ (UN "IClaim"), [v,w,x,y,z]) (UN (Basic "IClaim"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v) => do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IClaim v' w' x' y' 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) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IData x' y' 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) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IDef x' y' 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) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IParameters x' y' 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) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IRecord w' x' y' 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) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (INamespace w' x' 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) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (ITransform w' x' y' z') pure (ITransform w' x' y' z')
(NS _ (UN "ILog"), [x]) (UN (Basic "ILog"), [x])
=> do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (ILog x') pure (ILog x')
_ => cantReify val "Decl" _ => cantReify val "Decl"

15
src/TTImp/TTImp.idr
View File

@ -500,7 +500,7 @@ findIBinds (INamedApp _ fn _ av)
= findIBinds fn ++ findIBinds av = findIBinds fn ++ findIBinds av
findIBinds (IWithApp fc fn av) findIBinds (IWithApp fc fn av)
= findIBinds fn ++ findIBinds av = findIBinds fn ++ findIBinds av
findIBinds (IAs fc _ _ (UN n) pat) findIBinds (IAs fc _ _ (UN (Basic n)) pat)
= n :: findIBinds pat = n :: findIBinds pat
findIBinds (IAs fc _ _ n pat) findIBinds (IAs fc _ _ n pat)
= findIBinds pat = findIBinds pat
@ -522,7 +522,7 @@ findIBinds tm = []
export export
findImplicits : RawImp' nm -> List String 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 = mn :: findImplicits aty ++ findImplicits retty
findImplicits (IPi fc rig p mn aty retty) findImplicits (IPi fc rig p mn aty retty)
= findImplicits aty ++ findImplicits retty = findImplicits aty ++ findImplicits retty
@ -563,7 +563,7 @@ implicitsAs : {auto c : Ref Ctxt Defs} ->
implicitsAs n defs ns tm implicitsAs n defs ns tm
= do let implicits = findIBinds tm = do let implicits = findIBinds tm
log "declare.def.lhs.implicits" 30 $ "Found implicits: " ++ show implicits 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 where
-- Takes the function application expression which is the lhs of a clause -- Takes the function application expression which is the lhs of a clause
-- and decomposes it into the underlying function symbol and the variables -- 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)) = do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
case es of case es of
-- Explicits were skipped, therefore all explicits are given anyway -- 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 -- Explicits weren't skipped, so we need to check
_ => case updateNs x es of _ => case updateNs x es of
Nothing => pure [] -- explicit wasn't given Nothing => pure [] -- explicit wasn't given
@ -659,9 +659,9 @@ implicitsAs n defs ns tm
impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp
impAs loc' [] tm = tm impAs loc' [] tm = tm
impAs loc' ((UN n, AutoImplicit) :: ns) tm impAs loc' ((nm@(UN (Basic n)), AutoImplicit) :: ns) tm
= impAs loc' ns $ = 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' ((n, Implicit) :: ns) tm
= impAs loc' ns $ = impAs loc' ns $
@ -694,7 +694,6 @@ definedInBlock ns decls =
UN _ => NS ns n UN _ => NS ns n
MN _ _ => NS ns n MN _ _ => NS ns n
DN _ _ => NS ns n DN _ _ => NS ns n
RF _ => NS ns n
_ => n _ => n
defName : Namespace -> ImpDecl -> List Name defName : Namespace -> ImpDecl -> List Name
@ -711,7 +710,7 @@ definedInBlock ns decls =
fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
toRF : Name -> Name toRF : Name -> Name
toRF (UN n) = RF n toRF (UN (Basic n)) = UN (Field n)
toRF n = n toRF n = n
fnsUN : List Name fnsUN : List Name

2
src/TTImp/Unelab.idr
View File

@ -309,7 +309,7 @@ mutual
let nm = if used 0 sctm || isNoSugar umode let nm = if used 0 sctm || isNoSugar umode
then Just x then Just x
else if rig /= top || isDefImp p else if rig /= top || isDefImp p
then Just (UN "_") then Just (UN Underscore)
else Nothing else Nothing
pure (IPi fc rig p' nm ty' sc, gType fc) pure (IPi fc rig p' nm ty' sc, gType fc)
where where

20
src/TTImp/Utils.idr
View File

@ -60,8 +60,8 @@ findBindableNames : (arg : Bool) -> List Name -> (used : List String) ->
findBindableNamesQuot : List Name -> (used : List String) -> RawImp -> findBindableNamesQuot : List Name -> (used : List String) -> RawImp ->
List (String, String) List (String, String)
findBindableNames True env used (IVar fc (UN n)) findBindableNames True env used (IVar fc nm@(UN (Basic n)))
= if not (UN n `elem` env) && lowerFirst n = if not (nm `elem` env) && lowerFirst n
then [(n, getUnique used n)] then [(n, getUnique used n)]
else [] else []
findBindableNames arg env used (IPi fc rig p mn aty retty) 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 False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IWithApp fc fn av) findBindableNames arg env used (IWithApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used 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 = (n, getUnique used n) :: findBindableNames arg env used pat
findBindableNames arg env used (IAs fc _ _ n pat) findBindableNames arg env used (IAs fc _ _ n pat)
= findBindableNames arg env used pat = findBindableNames arg env used pat
@ -184,7 +184,7 @@ findUniqueBindableNames fc arg env used t
do defs <- get Ctxt do defs <- get Ctxt
let ctxt = gamma defs let ctxt = gamma defs
ns <- map catMaybes $ for assoc $ \ (n, _) => do 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) => let ns = flip mapMaybe ns $ \(n, _, d) =>
case definition d of case definition d of
-- do not warn about holes: `?a` is not actually -- do not warn about holes: `?a` is not actually
@ -255,7 +255,7 @@ findIBindVars (IAutoApp fc fn av)
findIBindVars (IWithApp fc fn av) findIBindVars (IWithApp fc fn av)
= findIBindVars fn ++ findIBindVars av = findIBindVars fn ++ findIBindVars av
findIBindVars (IBindVar fc v) findIBindVars (IBindVar fc v)
= [UN v] = [UN (Basic v)]
findIBindVars (IDelayed fc r t) findIBindVars (IDelayed fc r t)
= findIBindVars t = findIBindVars t
findIBindVars (IDelay fc t) findIBindVars (IDelay fc t)
@ -279,8 +279,8 @@ mutual
_ => IVar fc n _ => IVar fc n
else IVar fc n else IVar fc n
substNames' True bound ps (IBindVar fc n) substNames' True bound ps (IBindVar fc n)
= if not (UN n `elem` bound) = if not (UN (Basic n) `elem` bound)
then case lookup (UN n) ps of then case lookup (UN $ Basic n) ps of
Just t => t Just t => t
_ => IBindVar fc n _ => IBindVar fc n
else IBindVar fc n else IBindVar fc n
@ -331,13 +331,13 @@ mutual
substNamesClause' : Bool -> List Name -> List (Name, RawImp) -> substNamesClause' : Bool -> List Name -> List (Name, RawImp) ->
ImpClause -> ImpClause ImpClause -> ImpClause
substNamesClause' bvar bound ps (PatClause fc lhs rhs) 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 ++ findIBindVars lhs
++ bound in ++ bound in
PatClause fc (substNames' bvar [] [] lhs) PatClause fc (substNames' bvar [] [] lhs)
(substNames' bvar bound' ps rhs) (substNames' bvar bound' ps rhs)
substNamesClause' bvar bound ps (WithClause fc lhs wval prf flags cs) 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 ++ findIBindVars lhs
++ bound in ++ bound in
WithClause fc (substNames' bvar [] [] lhs) WithClause fc (substNames' bvar [] [] lhs)
@ -483,7 +483,7 @@ uniqueName defs used n
where where
usedName : Core Bool usedName : Core Bool
usedName usedName
= pure $ case !(lookupTyName (UN n) (gamma defs)) of = pure $ case !(lookupTyName (UN $ Basic n) (gamma defs)) of
[] => n `elem` used [] => n `elem` used
_ => True _ => True

8
src/TTImp/WithClause.idr
View File

@ -96,10 +96,10 @@ mutual
-- one of them is okay -- one of them is okay
getMatch lhs (IAlternative fc _ as) (IAlternative _ _ as') getMatch lhs (IAlternative fc _ as) (IAlternative _ _ as')
= matchAny fc lhs (zip as 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' = do ms <- getMatch lhs p p'
mergeMatches lhs ((n, IBindVar fc n') :: ms) 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' = do ms <- getMatch lhs p p'
mergeMatches lhs ((n, p') :: ms) mergeMatches lhs ((n, p') :: ms)
getMatch lhs (IAs _ _ _ _ p) p' = getMatch lhs p p' 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 (arg : Maybe (PiInfo RawImp, Name)) -> RawImp
getArgMatch ploc mode search warg ms Nothing = warg getArgMatch ploc mode search warg ms Nothing = warg
getArgMatch ploc mode True warg ms (Just (AutoImplicit, nm)) 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 Just tm => tm
Nothing => Nothing =>
let arg = ISearch ploc 500 in 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 then IAs ploc ploc UseLeft nm arg
else arg else arg
getArgMatch ploc mode search warg ms (Just (_, nm)) 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 Just tm => tm
Nothing => Nothing =>
let arg = Implicit ploc True in let arg = Implicit ploc True in

6
tests/idris2/docs002/expected
View File

@ -7,6 +7,8 @@ a : SimpleRec -> Int
b : SimpleRec -> String b : SimpleRec -> String
hello : Int -> Int hello : Int -> Int
world : Nat -> Nat world : Nat -> Nat
.a : SimpleRec -> Int
.b : SimpleRec -> String
Doc> Doc.NS.NestedNS.Foo : Type Doc> Doc.NS.NestedNS.Foo : Type
A type of Foo A type of Foo
@ -17,6 +19,6 @@ Doc> record Doc.SimpleRec : Type
Totality: total Totality: total
Constructor: MkSimpleRec : Int -> String -> SimpleRec Constructor: MkSimpleRec : Int -> String -> SimpleRec
Projections: Projections:
a : SimpleRec -> Int .a : SimpleRec -> Int
b : SimpleRec -> String .b : SimpleRec -> String
Doc> Bye for now! Doc> Bye for now!

10
tests/idris2/docs003/expected
View File

@ -3,17 +3,17 @@ RecordDoc>
RecordDoc> record RecordDoc.A : Type -> Type RecordDoc> record RecordDoc.A : Type -> Type
Totality: total Totality: total
Constructor: __mkA : _ Constructor: __mkA : _
Projection: anA : A a -> a Projection: .anA : A a -> a
RecordDoc> record RecordDoc.Tuple : Type -> Type -> Type RecordDoc> record RecordDoc.Tuple : Type -> Type -> Type
Totality: total Totality: total
Constructor: __mkTuple : _ Constructor: __mkTuple : _
Projections: Projections:
proj1 : Tuple a b -> a .proj1 : Tuple a b -> a
proj2 : Tuple a b -> b .proj2 : Tuple a b -> b
RecordDoc> record RecordDoc.Singleton : a -> Type RecordDoc> record RecordDoc.Singleton : a -> Type
Totality: total Totality: total
Constructor: __mkSingleton : _ Constructor: __mkSingleton : _
Projections: Projections:
equal : (rec : Singleton v) -> value rec = v .equal : (rec : Singleton v) -> value rec = v
value : Singleton v -> a .value : Singleton v -> a
RecordDoc> Bye for now! RecordDoc> Bye for now!

10
tests/idris2/reflection001/expected
View File

@ -33,9 +33,9 @@ quote:37:1--37:21
37 | %runElab noExtension 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 (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 "+")) (IVar (MkFC (Virtual Interactive) (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC (Virtual Interactive) (0, 14) (0, 19)) (UN "False")) 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 "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"])) (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 "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> 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 "names", NS (MkNS ["Prelude"]) (UN "+")] Main> [UN (Basic "names"), NS (MkNS ["Prelude"]) (UN (Basic "+"))]
Main> Bye for now! Main> Bye for now!

5
tests/idris2/reflection004/refdecl.idr
View File

@ -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 : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl
mkPoint n mkPoint n
= let type = "Point" ++ show n ++ "D" in = let type = "Point" ++ show n ++ "D" in
let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in
IRecord emptyFC Nothing Public IRecord emptyFC Nothing Public
(MkRecord emptyFC (NS (MkNS ["Main"]) (UN type)) [] (NS (MkNS ["Main"]) (UN ("Mk" ++ type))) (MkRecord emptyFC (mkMainUN type) [] (mkMainUN ("Mk" ++ type))
(toList $ map (\axis => MkIField emptyFC MW ExplicitArg (RF axis) `(Double)) (axes n))) (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n)))
logDecls : TTImp -> Elab (Int -> Int) logDecls : TTImp -> Elab (Int -> Int)
logDecls v logDecls v

2
tests/idris2/reg033/DerivingEq.idr
View File

@ -21,7 +21,7 @@ genEq typeName = do
let and : TTImp -> TTImp -> TTImp let and : TTImp -> TTImp -> TTImp
and x y = `(~(x) && ~(y)) and x y = `(~(x) && ~(y))
compareEq : String -> String -> TTImp 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 : Name -> Elab Clause
makeClause constr = do makeClause constr = do
[(_, ty)] <- getType constr [(_, ty)] <- getType constr