idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-20 17:57:38 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #109 from ziman/with-disamb

Browse Source 
`with` expressions for name disambiguation
This commit is contained in:
Edwin Brady 2020-05-23 12:22:35 +01:00 committed by GitHub
commit aeea2b80c9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
16 changed files with 203 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
CHANGELOG.md
View File

@ -21,6 +21,9 @@ Language changes:
* A %spec flag on functions which allows arguments to be marked for partial
evaluation, following the rules from "Scrapping Your Inefficient Engine"
(ICFP 2010, Brady & Hammond)
* To improve error messages, one can use `with NS.name <term>`
or `with [NS.name1, NS.name2, ...] <term>` to disable disambiguation
for the given names in `<term>`. Example: `with MyNS.(>>=) do ...`.
Library additions:

10
docs/source/tutorial/modules.rst
View File

@ -64,7 +64,15 @@ the name of the module. The names defined in the ``BTree`` module are, in full:
If names are otherwise unambiguous, there is no need to give the fully
qualified name. Names can be disambiguated either by giving an explicit
qualification, or according to their type.
qualification, using the ``with`` keyword, or according to their type.
The ``with`` keyword in expressions comes in two variants:
* ``with BTree.insert (insert x empty)`` for one name
* ``with [BTree.insert, BTree.empty] (insert x empty)`` for multiple names
This is particularly useful with ``do`` notation, where it can often improve
error messages: ``with MyModule.(>>=) do ...``
There is no formal link between the module name and its filename,
although it is generally advisable to use the same name for each. An

2
src/Core/Binary.idr
View File

@ -28,7 +28,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 28
ttcVersion = 29
export
checkTTCVersion : String -> Int -> Int -> Core ()

2
src/Idris/Desugar.idr
View File

@ -353,6 +353,8 @@ mutual
= desugarB side ps $
PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc) $
foldl (\r, f => PApp fc (PRef fc f) r) (PRef fc (MN "rec" 0)) fields
desugarB side ps (PWithUnambigNames fc ns rhs)
= IWithUnambigNames fc ns <$> desugarB side ps rhs
desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
{auto b : Ref Bang BangData} ->

24
src/Idris/Parser.idr
View File

@ -128,6 +128,7 @@ mutual
<|> lambdaCase fname indents
<|> lazy fname indents
<|> if_ fname indents
<|> with_ fname indents
<|> doBlock fname indents
<|> do start <- location
f <- simpleExpr fname indents
@ -188,6 +189,29 @@ mutual
symbol "}"
pure (Nothing, tm)
with_ : FileName -> IndentInfo -> SourceRule PTerm
with_ fname indents
= do start <- location
keyword "with"
commit
ns <- singleName <|> nameList
end <- location
rhs <- expr pdef fname indents
pure (PWithUnambigNames (MkFC fname start end) ns rhs)
where
singleName : SourceRule (List Name)
singleName = do
n <- name
pure [n]
nameList : SourceRule (List Name)
nameList = do
symbol "["
commit
ns <- sepBy1 (symbol ",") name
symbol "]"
pure ns
opExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
opExpr q fname indents
= do start <- location

3
src/Idris/Resugar.idr
View File

@ -252,6 +252,9 @@ mutual
toPTerm p (Implicit fc True) = pure (PImplicit fc)
toPTerm p (Implicit fc False) = pure (PInfer fc)
toPTerm p (IWithUnambigNames fc ns rhs) =
PWithUnambigNames fc ns <$> toPTerm startPrec rhs
mkApp : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
PTerm -> List (FC, Maybe (Maybe Name), PTerm) -> Core PTerm

8
src/Idris/Syntax.idr
View File

@ -96,7 +96,8 @@ mutual
-- Debugging
PUnifyLog : FC -> Nat -> PTerm -> PTerm
-- TODO: 'with' disambiguation
-- with-disambiguation
PWithUnambigNames : FC -> List Name -> PTerm -> PTerm
public export
data PFieldUpdate : Type where
@ -493,6 +494,8 @@ mutual
= showPrec d rec ++ concatMap show fields
showPrec d (PRecordProjection fc fields)
= concatMap show fields
showPrec d (PWithUnambigNames fc ns rhs)
= "with " ++ show ns ++ " " ++ showPrec d rhs
public export
record IFaceInfo where
@ -776,6 +779,9 @@ mapPTermM f = goPTerm where
>>= f
goPTerm (PRecordProjection fc fields) =
f (PRecordProjection fc fields)
goPTerm (PWithUnambigNames fc ns rhs) =
PWithUnambigNames fc ns <$> goPTerm rhs
>>= f
goPFieldUpdate : PFieldUpdate -> Core PFieldUpdate
goPFieldUpdate (PSetField p t) = PSetField p <$> goPTerm t

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

@ -15,6 +15,7 @@ import TTImp.TTImp
import Data.Bool.Extra
import Data.List
import Data.StringMap
%default covering
@ -49,17 +50,26 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
ci <- fromCharName
let prims = mapMaybe id [fi, si, ci]
let primApp = isPrimName prims x
ns <- lookupCtxtName x (gamma defs)
ns' <- filterM visible ns
case ns' of
[] => do log 10 $ "Failed to find " ++ show orig
pure orig
[nalt] =>
do log 10 $ "Only one " ++ show (fst nalt)
pure $ mkAlt primApp est nalt
nalts => pure $ IAlternative fc (uniqType fi si ci x args)
(map (mkAlt primApp est) nalts)
case lookupUN (userNameRoot x) (unambiguousNames est) of
Just xr => do
log 10 $ "unambiguous: " ++ show (fst xr)
pure $ mkAlt primApp est xr
Nothing => do
ns <- lookupCtxtName x (gamma defs)
ns' <- filterM visible ns
case ns' of
[] => do log 10 $ "Failed to find " ++ show orig
pure orig
[nalt] =>
do log 10 $ "Only one " ++ show (fst nalt)
pure $ mkAlt primApp est nalt
nalts => pure $ IAlternative fc (uniqType fi si ci x args)
(map (mkAlt primApp est) nalts)
where
lookupUN : Maybe String -> StringMap a -> Maybe a
lookupUN Nothing _ = Nothing
lookupUN (Just n) sm = lookup n sm
visible : (Name, Int, GlobalDef) -> Core Bool
visible (n, i, def)
= do let NS ns x = fullname def

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

@ -131,13 +131,18 @@ record EState (vars : List Name) where
linearUsed : List (Var vars)
saveHoles : NameMap () -- things we'll need to save to TTC, even if solved
unambiguousNames : StringMap (Name, Int, GlobalDef)
-- Mapping from userNameRoot to fully resolved names.
-- For names in this mapping, we don't run disambiguation.
-- Used in with-expressions.
export
data EST : Type where
export
initEStateSub : {outer : _} ->
Int -> Env Term outer -> SubVars outer vars -> EState vars
initEStateSub n env sub = MkEState n env sub [] [] [] [] [] Z [] empty
initEStateSub n env sub = MkEState n env sub [] [] [] [] [] Z [] empty empty
export
initEState : {vars : _} ->
@ -167,7 +172,8 @@ weakenedEState {e}
(allPatVars est)
(delayDepth est)
(map weaken (linearUsed est))
(saveHoles est))
(saveHoles est)
(unambiguousNames est))
pure eref
where
wknTms : (Name, ImplBinding vs) ->
@ -199,7 +205,8 @@ strengthenedEState {n} {vars} c e fc env
(allPatVars est)
(delayDepth est)
(mapMaybe dropTop (linearUsed est))
(saveHoles est))
(saveHoles est)
(unambiguousNames est))
where
dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
dropSub (DropCons sub) = pure sub
@ -293,6 +300,7 @@ updateEnv env sub bif st
(delayDepth st)
(linearUsed st)
(saveHoles st)
(unambiguousNames st)
export
addBindIfUnsolved : {vars : _} ->
@ -309,6 +317,7 @@ addBindIfUnsolved hn r p env tm ty st
(delayDepth st)
(linearUsed st)
(saveHoles st)
(unambiguousNames st)
clearBindIfUnsolved : EState vars -> EState vars
clearBindIfUnsolved st
@ -320,6 +329,7 @@ clearBindIfUnsolved st
(delayDepth st)
(linearUsed st)
(saveHoles st)
(unambiguousNames st)
-- Clear the 'toBind' list, except for the names given
export

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

@ -1,5 +1,7 @@
module TTImp.Elab.Term
import Data.StringMap
import Core.Context
import Core.Core
import Core.Env
@ -215,6 +217,36 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
do est <- get EST
put EST (addBindIfUnsolved nm rig Explicit env metaval ty est)
pure (metaval, gnf env ty)
checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
= do -- enter the scope -> add unambiguous names
est <- get EST
rns <- resolveNames fc ns
put EST $ record { unambiguousNames = mergeLeft rns (unambiguousNames est) } est
-- inside the scope -> check the RHS
result <- check rig elabinfo nest env rhs exp
-- exit the scope -> restore unambiguous names
newEST <- get EST
put EST $ record { unambiguousNames = unambiguousNames est } newEST
pure result
where
resolveNames : FC -> List Name -> Core (StringMap (Name, Int, GlobalDef))
resolveNames fc [] = pure empty
resolveNames fc (n :: ns) =
case userNameRoot n of
-- should never happen
Nothing => throw $ InternalError $ "non-UN in \"with\" LHS: " ++ show n
Just nRoot => do
-- this will always be a global name
-- so we lookup only among the globals
ctxt <- get Ctxt
rns <- lookupCtxtName n (gamma ctxt)
case rns of
[] => throw $ UndefinedName fc n
[rn] => insert nRoot rn <$> resolveNames fc ns
_ => throw $ AmbiguousName fc (map fst rns)
-- Declared in TTImp.Elab.Check
-- check : {vars : _} ->

11
src/TTImp/TTImp.idr
View File

@ -105,6 +105,9 @@ mutual
-- at the end of elaborator
Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp
-- with-disambiguation
IWithUnambigNames : FC -> List Name -> RawImp -> RawImp
public export
data IFieldUpdate : Type where
ISetField : (path : List String) -> RawImp -> IFieldUpdate
@ -170,6 +173,7 @@ mutual
show (IType fc) = "%type"
show (Implicit fc True) = "_"
show (Implicit fc False) = "?"
show (IWithUnambigNames fc ns rhs) = "(%with " ++ show ns ++ " " ++ show rhs ++ ")"
export
Show IFieldUpdate where
@ -590,6 +594,7 @@ getFC (IUnquote x _) = x
getFC (IRunElab x _) = x
getFC (IAs x _ _ _) = x
getFC (Implicit x _) = x
getFC (IWithUnambigNames x _ _) = x
export
apply : RawImp -> List RawImp -> RawImp
@ -679,6 +684,8 @@ mutual
toBuf b (Implicit fc i)
= do tag 28; toBuf b fc; toBuf b i
toBuf b (IWithUnambigNames fc ns rhs)
= do tag 29; toBuf b ns; toBuf b rhs
fromBuf b
= case !getTag of
@ -763,6 +770,10 @@ mutual
28 => do fc <- fromBuf b
i <- fromBuf b
pure (Implicit fc i)
29 => do fc <- fromBuf b
ns <- fromBuf b
rhs <- fromBuf b
pure (IWithUnambigNames fc ns rhs)
_ => corrupt "RawImp"
export

4
tests/Main.idr
View File

@ -91,7 +91,9 @@ idrisTests
"total001", "total002", "total003", "total004", "total005",
"total006", "total007", "total008",
-- The 'with' rule
"with001", "with002"]
"with001", "with002",
-- with-disambiguation
"with003"]
typeddTests : List String
typeddTests

10
tests/idris2/with003/Main.idr Normal file
View File

@ -0,0 +1,10 @@
module Main
import Data.List
import Data.Vect
-- add some definition of (>>=) in another namespace
namespace Other
public export
(>>=) : IO a -> IO b -> IO b
(>>=) f x = f *> x

53
tests/idris2/with003/expected Normal file
View File

@ -0,0 +1,53 @@
1/1: Building Main (Main.idr)
Main> (interactive):1:60--1:73:Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
?_ -> IO ()
and
IO ?b
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
?_ -> IO ()
and
IO ?b
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
?_ -> IO ()
and
IO ?b
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
?_ -> IO ()
and
IO ?b
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b
Mismatch between:
?_ -> IO ()
and
IO ?b
Main> (interactive):1:57--1:62:Can't find an implementation for Num ()
Main> (interactive):1:4--1:6:Ambiguous elaboration. Possible correct results:
[]
[]
[]
Main> [] : Vect 0 ?elem
Main> [] : List ?a
Main> (interactive):1:34--1:41:When unifying Vect 0 ?elem and List ?a
Mismatch between:
Vect 0 ?elem
and
List ?a
Main> the (Maybe Integer) (pure 4) : Maybe Integer
Main> Parse error: Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input])
Main> Bye for now!

9
tests/idris2/with003/input Normal file
View File

@ -0,0 +1,9 @@
do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo"
with Prelude.(>>=) do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo"
:t []
:t with Vect.Nil []
:t with Prelude.Nil []
:t with [Vect.Nil, Prelude.(::)] [1,2,3]
:t with pure the (Maybe _) (pure 4)
:t with [] 4
:q

3
tests/idris2/with003/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-banner Main.idr < input
rm -rf build