mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-23 04:42:05 +03:00
Block reduction of private/export names
This commit is contained in:
Edwin Brady
parent
ed43fd49b9
commit
1be12c7f72
@ -205,13 +205,13 @@ searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) ta
|
||||
Core (Term vars)
|
||||
findDirect defs prf f ty target
|
||||
= do (args, appTy) <- mkArgs fc rigc env ty
|
||||
logNF 10 "Trying " env ty
|
||||
ures <- unify InTerm fc env target appTy
|
||||
let [] = constraints ures
|
||||
| _ => throw (CantSolveGoal fc [] top)
|
||||
-- We can only use the local if its type is not an unsolved hole
|
||||
if !(usableLocal fc defaults env ty)
|
||||
then do
|
||||
logNF 10 "Trying " env ty
|
||||
ures <- unify InTerm fc env target appTy
|
||||
let [] = constraints ures
|
||||
| _ => throw (CantSolveGoal fc [] top)
|
||||
then do
|
||||
let candidate = apply fc (f prf) (map metaApp args)
|
||||
logTermNF 10 "Candidate " env candidate
|
||||
traverse (searchIfHole fc defaults False depth def top env) args
|
||||
@ -413,7 +413,9 @@ searchType {vars} fc rigc defaults depth def top env target
|
||||
tryGroups nty (g :: gs)
|
||||
= handleUnify
|
||||
(do logC 5 (do gn <- traverse getFullName g
|
||||
pure ("Search: Trying names " ++ show gn))
|
||||
pure ("Search: Trying " ++ show (length gn) ++
|
||||
" names " ++ show gn))
|
||||
logNF 5 "For target" env nty
|
||||
searchNames fc rigc defaults depth def top env g nty)
|
||||
(\err => if ambig err || isNil gs
|
||||
then throw err
|
||||
@ -426,9 +428,8 @@ searchType {vars} fc rigc defaults depth def top env target
|
||||
-- (defaults : Bool) -> (depth : Nat) ->
|
||||
-- (defining : Name) -> (topTy : Term vars) -> Env Term vars ->
|
||||
-- Core (Term vars)
|
||||
Core.Unify.search fc rigc defaults depth def top_in env
|
||||
Core.Unify.search fc rigc defaults depth def top env
|
||||
= do defs <- get Ctxt
|
||||
top <- normaliseScope defs env top_in
|
||||
logTerm 2 "Initial target: " top
|
||||
log 2 $ "Running search with defaults " ++ show defaults
|
||||
tm <- searchType fc rigc defaults depth def
|
||||
|
||||
@ -190,8 +190,7 @@ writeToTTC : TTC extra =>
|
||||
{auto u : Ref UST UState} ->
|
||||
extra -> (fname : String) -> Core ()
|
||||
writeToTTC extradata fname
|
||||
= logTime "Writing TTC" $
|
||||
do buf <- initBinary
|
||||
= do buf <- initBinary
|
||||
defs <- get Ctxt
|
||||
ust <- get UST
|
||||
gdefs <- getSaveDefs !getSave [] defs
|
||||
@ -283,8 +282,7 @@ readFromTTC : TTC extra =>
|
||||
List (List String, Bool, List String),
|
||||
NameRefs))
|
||||
readFromTTC loc reexp fname modNS importAs
|
||||
= logTime "Reading TTC" $
|
||||
do defs <- get Ctxt
|
||||
= do defs <- get Ctxt
|
||||
-- If it's already in the context, don't load it again
|
||||
let False = (fname, importAs) `elem` allImported defs
|
||||
| True => pure Nothing
|
||||
|
||||
@ -778,8 +778,8 @@ visibleIn nspace n _ = True
|
||||
|
||||
export
|
||||
reducibleIn : (nspace : List String) -> Name -> Visibility -> Bool
|
||||
reducibleIn nspace (NS ns n) Export = isSuffixOf ns nspace
|
||||
reducibleIn nspace (NS ns n) Private = isSuffixOf ns nspace
|
||||
reducibleIn nspace (NS ns (UN n)) Export = isSuffixOf ns nspace
|
||||
reducibleIn nspace (NS ns (UN n)) Private = isSuffixOf ns nspace
|
||||
reducibleIn nspace n _ = True
|
||||
|
||||
export
|
||||
|
||||
@ -181,10 +181,10 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
evalRef env locs meta fc nt n stk def
|
||||
= do Just res <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure def
|
||||
let redok = True -- evalAll topopts ||
|
||||
-- reducibleIn (currentNS defs)
|
||||
-- (fullname res)
|
||||
-- (visibility res)
|
||||
let redok = evalAll topopts ||
|
||||
reducibleIn (currentNS defs)
|
||||
(fullname res)
|
||||
(visibility res)
|
||||
if redok
|
||||
then do
|
||||
opts' <- if noCycles res
|
||||
|
||||
@ -430,8 +430,8 @@ nameIn defs tyns (NApp _ _ args)
|
||||
nameIn defs tyns (NTCon _ n _ _ args)
|
||||
= if n `elem` tyns
|
||||
then pure True
|
||||
else anyM (nameIn defs tyns)
|
||||
!(traverse (evalClosure defs) args)
|
||||
else do args' <- traverse (evalClosure defs) args
|
||||
anyM (nameIn defs tyns) args'
|
||||
nameIn defs tyns (NDCon _ n _ _ args)
|
||||
= anyM (nameIn defs tyns)
|
||||
!(traverse (evalClosure defs) args)
|
||||
|
||||
@ -567,6 +567,6 @@ checkExp rig elabinfo env fc tm got (Just exp)
|
||||
empty <- clearDefs defs
|
||||
cty <- getTerm exp
|
||||
ctm <- newConstant fc rig env tm cty cs
|
||||
dumpConstraints 1 False
|
||||
dumpConstraints 5 False
|
||||
pure (ctm, got)
|
||||
checkExp rig elabinfo env fc tm got Nothing = pure (tm, got)
|
||||
|
||||
@ -470,15 +470,21 @@ exprSearch : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> Name -> List Name -> Core (List ClosedTerm)
|
||||
exprSearch fc n hints
|
||||
exprSearch fc n_in hints
|
||||
= do defs <- get Ctxt
|
||||
let Just idx = getNameID n (gamma defs)
|
||||
| Nothing => throw (UndefinedName fc n)
|
||||
Just (n, idx, gdef) <- lookupHoleName n_in defs
|
||||
| Nothing => throw (UndefinedName fc n_in)
|
||||
lhs <- findHoleLHS (Resolved idx)
|
||||
log 10 $ "LHS hole data " ++ show (n, lhs)
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => throw (UndefinedName fc n)
|
||||
rs <- search fc (multiplicity gdef) (MkSearchOpts False True 5)
|
||||
!(getLHSData defs lhs) (type gdef) n
|
||||
dropLinearErrors fc rs
|
||||
where
|
||||
lookupHoleName : Name -> Defs -> Core (Maybe (Name, Int, GlobalDef))
|
||||
lookupHoleName n defs
|
||||
= case !(lookupCtxtExactI n (gamma defs)) of
|
||||
Just (idx, res) => pure $ Just (n, idx, res)
|
||||
Nothing => case !(lookupCtxtName n (gamma defs)) of
|
||||
[res] => pure $ Just res
|
||||
_ => pure Nothing
|
||||
|
||||
|
||||
@ -28,7 +28,7 @@ process eopts nest env (IClaim fc rig vis opts ty)
|
||||
process eopts nest env (IData fc vis ddef)
|
||||
= processData eopts nest env fc vis ddef
|
||||
process eopts nest env (IDef fc fname def)
|
||||
= processDef eopts nest env fc fname def
|
||||
= logTime (show fname) $ processDef eopts nest env fc fname def
|
||||
process eopts nest env (IParameters fc ps decls)
|
||||
= throw (InternalError "Parameters blocks not yet implemented")
|
||||
process eopts nest env (IRecord fc vis rec)
|
||||
|
||||
@ -316,7 +316,8 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
|
||||
Rig0 => InType
|
||||
_ => InExpr
|
||||
log 5 $ "Checking RHS " ++ show rhs
|
||||
rhstm <- checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
|
||||
rhstm <- logTime ("RHS of " ++ show n) $
|
||||
checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
|
||||
clearHoleLHS
|
||||
|
||||
logTerm 5 "RHS term" rhstm
|
||||
|
||||
@ -6,18 +6,23 @@ the : (a : Type) -> a -> a
|
||||
the _ $x = x
|
||||
|
||||
namespace List
|
||||
public export
|
||||
data List : Type -> Type where
|
||||
Nil : List $a
|
||||
Cons : $a -> List $a -> List $a
|
||||
|
||||
public export
|
||||
length : List $a -> Nat
|
||||
length Nil = Z
|
||||
length (Cons $x $xs) = S (length xs)
|
||||
|
||||
namespace Vect
|
||||
public export
|
||||
data Vect : ? -> Type -> Type where
|
||||
Nil : Vect Z $a
|
||||
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
||||
|
||||
public export
|
||||
length : Vect $n $a -> Nat
|
||||
length Nil = Z
|
||||
length (Cons $x $xs) = S (length xs)
|
||||
|
||||
@ -51,13 +51,16 @@ mapList $f (Cons $x $xs) = Cons (f x) (map f xs)
|
||||
ListFunctor = MkFunctor mapList
|
||||
|
||||
namespace Vect
|
||||
public export
|
||||
data Vect : ? -> Type -> Type where
|
||||
Nil : Vect Z $a
|
||||
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
||||
|
||||
%hint
|
||||
public export
|
||||
VectFunctor : Functor (Vect $n)
|
||||
|
||||
public export
|
||||
mapVect : ($a -> $b) -> Vect $n $a -> Vect $n $b
|
||||
mapVect $f Nil = Nil
|
||||
mapVect $f (Cons $x $xs) = Cons (f x) (map f xs)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user