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

Elaborate implementations in the right environment

Browse Source 
This involves a small extension to IPragma, because to properly
elaborate names in a local scope we need to know which names are defined
in that scope so that they get applied to the environment when needed.

This means we can now define implementations of interfaces locally (but
there's still some work to do, because we don't yet have a way of
applying locally defined hints in auto search. It's coming soon!)
This commit is contained in:
Edwin Brady 2020-12-05 20:53:03 +00:00
parent bfea7d785a
commit 22a534f400
8 changed files with 55 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Options/Log.idr
View File

@ -116,7 +116,7 @@ defaultLogLevel = singleton [] 0
export
insertLogLevel : LogLevel -> LogLevels -> LogLevels
insertLogLevel (MkLogLevel ps n) = insertWith ps (maybe n (max n))
insertLogLevel (MkLogLevel ps n) = insert ps n
----------------------------------------------------------------------------------
-- CHECKING WHETHER TO LOG

3
src/Core/UnifyState.idr
View File

@ -89,8 +89,7 @@ record UState where
-- we didn't have enough type information to elaborate
-- successfully yet.
-- 'Nat' is the priority (lowest first)
-- The 'Int' is the resolved name. Delays can't be nested,
-- so we just process them in order.
-- The 'Int' is the resolved name.
logging : Bool
export

40
src/Idris/Desugar.idr
View File

@ -703,7 +703,8 @@ mutual
doBind bnames (Builtin.snd ntm))) cons'
body' <- traverse (desugarDecl (ps ++ mnames ++ map fst params)) body
pure [IPragma (\nest, env =>
pure [IPragma (maybe [tn] (\n => [tn, n]) conname)
(\nest, env =>
elabInterface fc vis env nest consb
tn paramsb det conname
(concat body'))]
@ -746,7 +747,8 @@ mutual
body' <- maybe (pure Nothing)
(\b => do b' <- traverse (desugarDecl ps) b
pure (Just (concat b'))) body
pure [IPragma (\nest, env =>
pure [IPragma (maybe [] (\n => [n]) impname)
(\nest, env =>
elabImplementation fc vis opts pass env nest isb consb
tn paramsb impname nusing
body')]
@ -823,27 +825,27 @@ mutual
pure [IRunElabDecl fc tm']
desugarDecl ps (PDirective fc d)
= case d of
Hide n => pure [IPragma (\nest, env => hide fc n)]
Hide n => pure [IPragma [] (\nest, env => hide fc n)]
Logging i => pure [ILog (topics i, verbosity i)]
LazyOn a => pure [IPragma (\nest, env => lazyActive a)]
LazyOn a => pure [IPragma [] (\nest, env => lazyActive a)]
UnboundImplicits a => do
setUnboundImplicits a
pure [IPragma (\nest, env => setUnboundImplicits a)]
pure [IPragma [] (\nest, env => setUnboundImplicits a)]
PrefixRecordProjections b => do
pure [IPragma (\nest, env => setPrefixRecordProjections b)]
AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]
RewriteName eq rw => pure [IPragma (\nest, env => setRewrite fc eq rw)]
PrimInteger n => pure [IPragma (\nest, env => setFromInteger n)]
PrimString n => pure [IPragma (\nest, env => setFromString n)]
PrimChar n => pure [IPragma (\nest, env => setFromChar n)]
CGAction cg dir => pure [IPragma (\nest, env => addDirective cg dir)]
Names n ns => pure [IPragma (\nest, env => addNameDirective fc n ns)]
StartExpr tm => pure [IPragma (\nest, env => throw (InternalError "%start not implemented"))] -- TODO!
Overloadable n => pure [IPragma (\nest, env => setNameFlag fc n Overloadable)]
Extension e => pure [IPragma (\nest, env => setExtension e)]
DefaultTotality tot => pure [IPragma (\_, _ => setDefaultTotalityOption tot)]
pure [IPragma [] (\nest, env => setPrefixRecordProjections b)]
AmbigDepth n => pure [IPragma [] (\nest, env => setAmbigLimit n)]
AutoImplicitDepth n => pure [IPragma [] (\nest, env => setAutoImplicitLimit n)]
PairNames ty f s => pure [IPragma [] (\nest, env => setPair fc ty f s)]
RewriteName eq rw => pure [IPragma [] (\nest, env => setRewrite fc eq rw)]
PrimInteger n => pure [IPragma [] (\nest, env => setFromInteger n)]
PrimString n => pure [IPragma [] (\nest, env => setFromString n)]
PrimChar n => pure [IPragma [] (\nest, env => setFromChar n)]
CGAction cg dir => pure [IPragma [] (\nest, env => addDirective cg dir)]
Names n ns => pure [IPragma [] (\nest, env => addNameDirective fc n ns)]
StartExpr tm => pure [IPragma [] (\nest, env => throw (InternalError "%start not implemented"))] -- TODO!
Overloadable n => pure [IPragma [] (\nest, env => setNameFlag fc n Overloadable)]
Extension e => pure [IPragma [] (\nest, env => setExtension e)]
DefaultTotality tot => pure [IPragma [] (\_, _ => setDefaultTotalityOption tot)]
export
desugar : {auto s : Ref Syn SyntaxInfo} ->

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

@ -117,7 +117,11 @@ elabImplementation : {vars : _} ->
-- TODO: Refactor all these steps into separate functions
elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nusing mbody
= do let impName_in = maybe (mkImpl fc iname ps) id impln
impName <- inCurrentNS impName_in
-- If we're in a nested block, update the name
let impName_nest = case lookup impName_in (names nest) of
Just (Just n', _) => n'
_ => impName_in
impName <- inCurrentNS impName_nest
-- The interface name might be qualified, so check if it's an
-- alias for something
syn <- get Syn
@ -224,7 +228,13 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- Make sure we don't use this name to solve parent constraints
-- when elaborating the record, or we'll end up in a cycle!
setFlag fc impName BlockedHint
traverse (processDecl [] nest env) [impFn]
-- Update nested names so we elaborate the body in the right
-- environment
names' <- traverse applyEnv (impName :: mtops)
let nest' = record { names $= (names' ++) } nest
traverse (processDecl [] nest' env) [impFn]
unsetFlag fc impName BlockedHint
setFlag fc impName TCInline
@ -237,8 +247,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- 5. Elaborate the method bodies
let upds = map methNameUpdate fns
body' <- traverse (updateBody upds) body
log "elab.implementation" 10 $ "Implementation body: " ++ show body'
traverse (processDecl [] nest env) body'
traverse (processDecl [] nest' env) body'
-- 6. Add transformation rules for top level methods
traverse (addTransform impName upds) (methods cdata)
@ -251,6 +262,14 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
setOpenHints hs
pure ()) mbody
where
applyEnv : Name ->
Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))
applyEnv n
= do n' <- resolveName n
pure (Resolved n', (Nothing, reverse (allVars env),
\fn, nt => applyToFull fc
(Ref fc nt (Resolved n')) env))
-- For the method fields in the record, get the arguments we need to abstract
-- over
getFieldArgs : Term vs -> List (Name, List (Name, RigCount, PiInfo RawImp))

2
src/Idris/Resugar.idr
View File

@ -430,7 +430,7 @@ mutual
!(toPTerm startPrec rhs)))
toPDecl (IRunElabDecl fc tm)
= pure (Just (PRunElabDecl fc !(toPTerm startPrec tm)))
toPDecl (IPragma _) = pure Nothing
toPDecl (IPragma _ _) = pure Nothing
toPDecl (ILog _) = pure Nothing
export

2
src/TTImp/ProcessDecls.idr
View File

@ -56,7 +56,7 @@ process eopts nest env (ITransform fc n lhs rhs)
= processTransform eopts nest env fc n lhs rhs
process eopts nest env (IRunElabDecl fc tm)
= processRunElab eopts nest env fc tm
process eopts nest env (IPragma act)
process eopts nest env (IPragma _ act)
= act nest env
process eopts nest env (ILog lvl)
= addLogLevel (uncurry unsafeMkLogLevel lvl)

2
src/TTImp/Reflect.idr
View File

@ -748,7 +748,7 @@ mutual
appCon fc defs (reflectionttimp "ITransform") [w', x', y', z']
reflect fc defs lhs env (IRunElabDecl w x)
= throw (GenericMsg fc "Can't reflect a %runElab")
reflect fc defs lhs env (IPragma x)
reflect fc defs lhs env (IPragma _ x)
= throw (GenericMsg fc "Can't reflect a pragma")
reflect fc defs lhs env (ILog x)
= do x' <- reflect fc defs lhs env x

10
src/TTImp/TTImp.idr
View File

@ -344,7 +344,10 @@ mutual
INamespace : FC -> Namespace -> List ImpDecl -> ImpDecl
ITransform : FC -> Name -> RawImp -> RawImp -> ImpDecl
IRunElabDecl : FC -> RawImp -> ImpDecl
IPragma : ({vars : _} ->
IPragma : List Name -> -- pragmas might define names that wouldn't
-- otherwise be spotted in 'definedInBlock' so they
-- can be flagged here.
({vars : _} ->
NestedNames vars -> Env Term vars -> Core ()) ->
ImpDecl
ILog : (List String, Nat) -> ImpDecl
@ -365,7 +368,7 @@ mutual
= "%transform " ++ show n ++ " " ++ show lhs ++ " ==> " ++ show rhs
show (IRunElabDecl _ tm)
= "%runElab " ++ show tm
show (IPragma _) = "[externally defined pragma]"
show (IPragma _ _) = "[externally defined pragma]"
show (ILog (topic, lvl)) = "%logging " ++ case topic of
[] => show lvl
_ => concat (intersperse "." topic) ++ " " ++ show lvl
@ -610,6 +613,7 @@ definedInBlock ns decls =
all : List Name
all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
defName ns (IPragma pns _) = map (expandNS ns) pns
defName _ _ = []
export
@ -1018,7 +1022,7 @@ mutual
= do tag 6; toBuf b fc; toBuf b n; toBuf b lhs; toBuf b rhs
toBuf b (IRunElabDecl fc tm)
= do tag 7; toBuf b fc; toBuf b tm
toBuf b (IPragma f) = throw (InternalError "Can't write Pragma")
toBuf b (IPragma _ f) = throw (InternalError "Can't write Pragma")
toBuf b (ILog n)
= do tag 8; toBuf b n