edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-02 17:52:09 +03:00
Code Issues Projects Releases Wiki Activity

Add namespaces for metavariable names

Browse Source 
Since they're saved, they need to be unique across different input
files, so put them in a namespace. We might also add more metavariables
in the REPL, so save the name of the next variable in the current
namespace.
This commit is contained in:
Edwin Brady 2019-04-26 16:33:06 +01:00
parent 6d473014fd
commit 190690e925
5 changed files with 36 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Core/Binary.idr
View File

@ -49,6 +49,7 @@ record TTCFile extra where
constraints : List (Int, Constraint)
context : List GlobalDef
imported : List (List String, Bool, List String)
nextVar : Int
currentNS : List String
extraData : extra
@ -101,6 +102,7 @@ writeTTCFile b file
toBuf b (constraints file)
toBuf b (context file)
toBuf b (imported file)
toBuf b (nextVar file)
toBuf b (currentNS file)
toBuf b (extraData file)
@ -129,10 +131,11 @@ readTTCFile modns as r b
defs <- fromBuf r b
-- coreLift $ putStrLn $ "Read " ++ show (length (map fullname defs)) ++ " defs"
imp <- fromBuf r b
nextv <- fromBuf r b
cns <- fromBuf r b
ex <- fromBuf r b
pure (MkTTCFile ver ifaceHash importHashes r
holes guesses constraints defs imp cns ex)
holes guesses constraints defs imp nextv cns ex)
-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : List Name -> List GlobalDef -> Defs -> Core (List GlobalDef)
@ -165,6 +168,7 @@ writeToTTC extradata fname
(toList (constraints ust))
gdefs
(imported defs)
(nextName ust)
(currentNS defs)
extradata)
Right ok <- coreLift $ writeToFile fname !(get Bin)
@ -218,7 +222,8 @@ readFromTTC loc reexp fname modNS importAs
-- ttc
ust <- get UST
put UST (record { holes = fromList (holes ttc),
constraints = fromList (constraints ttc) } ust)
constraints = fromList (constraints ttc),
nextName = nextVar ttc } ust)
pure (Just (extraData ttc, ifaceHash ttc, imported ttc))
getImportHashes : NameRefs -> Ref Bin Binary ->

2
src/Core/Unify.idr
View File

@ -506,7 +506,7 @@ mutual
logC 10 $ (do ty' <- quote empty env ty
pure ("Unifying arg types " ++ show tx' ++ " and " ++ show ty'))
ct <- unify mode loc env tx ty
xn <- genName "x"
xn <- genVarName "x"
let env' : Env Term (x :: _)
= Pi cx ix tx' :: env
case constraints ct of

25
src/Core/UnifyState.idr
View File

@ -78,22 +78,38 @@ initUState = MkUState empty empty empty empty 0 0 Nothing
export
data UST : Type where
-- Generate a global name based on the given root, in the current namespace
export
genName : {auto u : Ref UST UState} ->
genName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
String -> Core Name
genName str
= do ust <- get UST
put UST (record { nextName $= (+1) } ust)
pure (MN str (nextName ust))
n <- inCurrentNS (MN str (nextName ust))
pure n
-- Generate a global name based on the given name, in the current namespace
export
genMVName : {auto u : Ref UST UState} ->
genMVName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Name -> Core Name
genMVName (UN str) = genName str
genMVName n
= do ust <- get UST
put UST (record { nextName $= (+1) } ust)
pure (MN (show n) (nextName ust))
mn <- inCurrentNS (MN (show n) (nextName ust))
pure mn
-- Generate a unique variable name based on the given root
export
genVarName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
String -> Core Name
genVarName str
= do ust <- get UST
put UST (record { nextName $= (+1) } ust)
pure (MN str (nextName ust))
addHoleName : {auto u : Ref UST UState} ->
FC -> Name -> Int -> Core ()
@ -264,6 +280,7 @@ newMeta : {auto c : Ref Ctxt Defs} ->
newMeta {vars} fc rig env n ty
= do let hty = abstractEnvType fc env ty
let hole = newDef fc n rig hty Public (Hole False)
log 10 $ "Adding new meta " ++ show n
idx <- addDef n hole
addHoleName fc n idx
pure (Meta fc n idx envArgs)

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

@ -149,7 +149,7 @@ bindUnsolved {vars} fc elabmode _
Nothing => do tmn <- toFullNames expected
throw (GenericMsg fc ("Can't bind implicit of type " ++ show tmn))
Just exp' =>
do impn <- genName (nameRoot n)
do impn <- genVarName (nameRoot n)
tm <- metaVar fc rig env impn exp'
est <- get EST
put EST (record { toBind $= ((impn, (embedSub subvars tm,

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

@ -32,7 +32,7 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamTm tm@(ILam _ _ Implicit _ _ _) (Bind fc n (Pi _ Implicit _) sc)
= pure (Just tm)
bindLamTm tm (Bind fc n (Pi c Implicit ty) sc)
= do n' <- genName ("imp_" ++ show n)
= do n' <- genVarName ("imp_" ++ show n)
Just sc' <- bindLamTm tm sc
| Nothing => pure Nothing
pure $ Just (ILam fc c Implicit (Just n') (Implicit fc False) sc')
@ -47,7 +47,7 @@ insertImpLam {vars} env tm (Just ty) = bindLam tm ty
bindLamNF tm@(ILam _ _ Implicit _ _ _) (NBind fc n (Pi _ Implicit _) sc)
= pure tm
bindLamNF tm (NBind fc n (Pi c Implicit ty) sc)
= do n' <- genName ("imp_" ++ show n)
= do n' <- genVarName ("imp_" ++ show n)
sctm <- sc (toClosure defaultOpts env (Ref fc Bound n'))
sc' <- bindLamNF tm sctm
pure $ ILam fc c Implicit (Just n') (Implicit fc False) sc'
@ -80,14 +80,14 @@ checkTerm rig elabinfo env (IPi fc r p (Just n) argTy retTy) exp
= checkPi rig elabinfo env fc r p n argTy retTy exp
checkTerm rig elabinfo env (IPi fc r p Nothing argTy retTy) exp
= do n <- case p of
Explicit => genName "arg"
Implicit => genName "imp"
AutoImplicit => genName "con"
Explicit => genVarName "arg"
Implicit => genVarName "imp"
AutoImplicit => genVarName "con"
checkPi rig elabinfo env fc r p n argTy retTy exp
checkTerm rig elabinfo env (ILam fc r p (Just n) argTy scope) exp
= checkLambda rig elabinfo env fc r p n argTy scope exp
checkTerm rig elabinfo env (ILam fc r p Nothing argTy scope) exp
= do n <- genName "lam"
= do n <- genVarName "lam"
checkLambda rig elabinfo env fc r p n argTy scope exp
checkTerm rig elabinfo env (IApp fc fn arg) exp
= checkApp rig elabinfo env fc fn [arg] [] exp