edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 05:32:03 +03:00
Code Issues Projects Releases Wiki Activity

Eliminate cycles in auto search

Browse Source 
This is important for, e.g. interfaces with parent constraints, so we
don't keep looping making the constraint bigger
This commit is contained in:
Edwin Brady 2019-06-17 09:32:59 +01:00
parent 8bc46c3438
commit 6a72508e80
9 changed files with 79 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Compiler/CompileExpr.idr
View File

@ -322,8 +322,7 @@ export
compileDef : {auto c : Ref Ctxt Defs} -> NameTags -> Name -> Core ()
compileDef tags n
= do defs <- get Ctxt
case !(lookupDefExact n (gamma defs)) of
Just d =>
do ce <- toCDef tags n d
setCompiled n ce
Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
ce <- toCDef tags n (definition gdef)
setCompiled n ce

8
src/Compiler/Inline.idr
View File

@ -110,8 +110,8 @@ mutual
| Nothing => pure (unload stk (CRef fc n))
let arity = getArity def
if (Inline `elem` flags gdef) && (not (n `elem` rec))
then pure $ maybe (unloadApp arity stk (CRef fc n)) id
!(tryApply (n :: rec) stk env def)
then do ap <- tryApply (n :: rec) stk env def
pure $ maybe (unloadApp arity stk (CRef fc n)) id ap
else pure $ unloadApp arity stk (CRef fc n)
eval {vars} {free} rec env [] (CLam fc x sc)
= do let thinsc = thin x {outer = x :: vars} {inner = free} sc
@ -236,8 +236,8 @@ inlineDef n
case compexpr def of
Nothing => pure ()
Just cexpr =>
do -- coreLift $ putStrLn $ show n ++ " before: " ++ show cexpr
do -- coreLift $ putStrLn $ show (fullname def) ++ " before: " ++ show cexpr
inlined <- inline cexpr
-- coreLift $ putStrLn $ show n ++ " after: " ++ show inlined
-- coreLift $ putStrLn $ show (fullname def) ++ " after: " ++ show inlined
setCompiled n inlined

86
src/Core/AutoSearch.idr
View File

@ -16,7 +16,8 @@ SearchEnv vars = List (NF vars, Closure vars)
searchType : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defaults : Bool) -> (trying : List (Term vars)) ->
(depth : Nat) ->
(defining : Name) -> (topTy : ClosedTerm) ->
Env Term vars -> (target : Term vars) -> Core (Term vars)
@ -51,13 +52,14 @@ mkArgs fc rigc env ty = pure ([], ty)
searchIfHole : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC ->
(defaults : Bool) -> (ispair : Bool) -> (depth : Nat) ->
(defaults : Bool) -> List (Term vars) ->
(ispair : Bool) -> (depth : Nat) ->
(defining : Name) -> (topTy : ClosedTerm) -> Env Term vars ->
(arg : ArgInfo vars) ->
Core ()
searchIfHole fc defaults ispair Z def top env arg
searchIfHole fc defaults trying ispair Z def top env arg
= throw (CantSolveGoal fc [] top) -- possibly should say depth limit hit?
searchIfHole fc defaults ispair (S depth) def top env arg
searchIfHole fc defaults trying ispair (S depth) def top env arg
= do let hole = holeID arg
let rig = argRig arg
@ -70,7 +72,7 @@ searchIfHole fc defaults ispair (S depth) def top env arg
then type gdef
else top
argdef <- searchType fc rig defaults depth def top' env
argdef <- searchType fc rig defaults trying depth def top' env
!(normaliseScope defs env (argType arg))
vs <- unify InTerm fc env (metaApp arg) argdef
let [] = constraints vs
@ -185,18 +187,19 @@ usableLocal loc _ _ _ = pure True
searchLocalWith : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defaults : Bool) -> List (Term vars) ->
(depth : Nat) ->
(defining : Name) -> (topTy : ClosedTerm) ->
Env Term vars -> List (Term vars, Term vars) ->
(target : NF vars) -> Core (Term vars)
searchLocalWith fc rigc defaults depth def top env [] target
searchLocalWith fc rigc defaults trying depth def top env [] target
= throw (CantSolveGoal fc [] top)
searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) target
searchLocalWith {vars} fc rigc defaults trying depth def top env ((prf, ty) :: rest) target
= tryUnify
(do defs <- get Ctxt
nty <- nf defs env ty
findPos defs prf id nty target)
(searchLocalWith fc rigc defaults depth def top env rest target)
(searchLocalWith fc rigc defaults trying depth def top env rest target)
where
findDirect : Defs -> Term vars ->
(Term vars -> Term vars) ->
@ -214,7 +217,7 @@ searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) ta
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
traverse (searchIfHole fc defaults trying False depth def top env) args
pure candidate
else do logNF 10 "Can't use " env ty
throw (CantSolveGoal fc [] top)
@ -258,12 +261,13 @@ searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) ta
searchLocal : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defaults : Bool) -> List (Term vars) ->
(depth : Nat) ->
(defining : Name) -> (topTy : ClosedTerm) ->
Env Term vars ->
(target : NF vars) -> Core (Term vars)
searchLocal fc rig defaults depth def top env target
= searchLocalWith fc rig defaults depth def top env (getAllEnv fc [] env) target
searchLocal fc rig defaults trying depth def top env target
= searchLocalWith fc rig defaults trying depth def top env (getAllEnv fc [] env) target
isPairNF : Env Term vars -> NF vars -> Defs -> Core Bool
isPairNF env (NTCon _ n _ _ _) defs
@ -275,12 +279,13 @@ isPairNF _ _ _ = pure False
searchName : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defaults : Bool) -> List (Term vars) ->
(depth : Nat) ->
(defining : Name) -> (topTy : ClosedTerm) ->
Env Term vars -> (target : NF vars) ->
(Name, GlobalDef) ->
Core (Term vars)
searchName fc rigc defaults depth def top env target (n, ndef)
searchName fc rigc defaults trying depth def top env target (n, ndef)
= do defs <- get Ctxt
let ty = type ndef
let namety : NameType
@ -296,24 +301,25 @@ searchName fc rigc defaults depth def top env target (n, ndef)
ispair <- isPairNF env nty defs
let candidate = apply fc (Ref fc namety n) (map metaApp args)
logTermNF 10 "Candidate " env candidate
traverse (searchIfHole fc defaults ispair depth def top env) args
traverse (searchIfHole fc defaults trying ispair depth def top env) args
pure candidate
searchNames : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> RigCount ->
(defaults : Bool) -> (depth : Nat) ->
(defaults : Bool) -> List (Term vars) ->
(depth : Nat) ->
(defining : Name) -> (topTy : ClosedTerm) ->
Env Term vars -> List Name ->
(target : NF vars) -> Core (Term vars)
searchNames fc rigc defaults depth defining topty env [] target
searchNames fc rigc defaults trying depth defining topty env [] target
= throw (CantSolveGoal fc [] topty)
searchNames fc rigc defaults depth defining topty env (n :: ns) target
searchNames fc rigc defaults trying depth defining topty env (n :: ns) target
= do defs <- get Ctxt
visnsm <- traverse (visible (gamma defs) (currentNS defs)) (n :: ns)
let visns = mapMaybe id visnsm
exactlyOne fc env topty
(map (searchName fc rigc defaults depth defining topty env target) visns)
(map (searchName fc rigc defaults trying depth defining topty env target) visns)
where
visible : Context GlobalDef ->
List String -> Name -> Core (Maybe (Name, GlobalDef))
@ -377,17 +383,29 @@ checkConcreteDets fc defaults env top (NTCon tfc tyn t a args)
checkConcreteDets fc defaults env top _
= pure ()
-- Declared at the top
searchType fc rigc defaults depth def top env (Bind nfc x (Pi c p ty) sc)
= pure (Bind nfc x (Lam c p ty)
!(searchType fc rigc defaults depth def top
(Pi c p ty :: env) sc))
searchType fc rigc defaults depth def top env (Bind nfc x (Let c val ty) sc)
= pure (Bind nfc x (Let c val ty)
!(searchType fc rigc defaults depth def top
(Let c val ty :: env) sc))
searchType {vars} fc rigc defaults depth def top env target
abandonIfCycle : {auto c : Ref Ctxt Defs} ->
Env Term vars -> Term vars -> List (Term vars) ->
Core ()
abandonIfCycle env tm [] = pure ()
abandonIfCycle env tm (ty :: tys)
= do defs <- get Ctxt
if !(convert defs env tm ty)
then throw (InternalError "Cycle in search")
else abandonIfCycle env tm tys
-- Declared at the top
searchType fc rigc defaults trying depth def top env (Bind nfc x (Pi c p ty) sc)
= pure (Bind nfc x (Lam c p ty)
!(searchType fc rigc defaults [] depth def top
(Pi c p ty :: env) sc))
searchType fc rigc defaults trying depth def top env (Bind nfc x (Let c val ty) sc)
= pure (Bind nfc x (Let c val ty)
!(searchType fc rigc defaults [] depth def top
(Let c val ty :: env) sc))
searchType {vars} fc rigc defaults trying depth def top env target
= do defs <- get Ctxt
abandonIfCycle env target trying
let trying' = target :: trying
nty <- nf defs env target
case nty of
NTCon tfc tyn t a args =>
@ -398,11 +416,11 @@ searchType {vars} fc rigc defaults depth def top env target
checkConcreteDets fc defaults env top
(NTCon tfc tyn t a args)
tryUnify
(searchLocal fc rigc defaults depth def top env nty)
(searchLocal fc rigc defaults trying' depth def top env nty)
(tryGroups nty (hintGroups sd))
else throw (CantSolveGoal fc [] top)
_ => do logNF 10 "Next target: " env nty
searchLocal fc rigc defaults depth def top env nty
searchLocal fc rigc defaults trying' depth def top env nty
where
ambig : Error -> Bool
ambig (AmbiguousSearch _ _ _) = True
@ -416,7 +434,7 @@ searchType {vars} fc rigc defaults depth def top env target
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)
searchNames fc rigc defaults (target :: trying) depth def top env g nty)
(\err => if ambig err || isNil gs
then throw err
else tryGroups nty gs)
@ -432,7 +450,7 @@ Core.Unify.search fc rigc defaults depth def top env
= do defs <- get Ctxt
logTerm 2 "Initial target: " top
log 2 $ "Running search with defaults " ++ show defaults
tm <- searchType fc rigc defaults depth def
tm <- searchType fc rigc defaults [] depth def
(abstractEnvType fc env top) env
top
defs <- get Ctxt

19
src/Core/Normalise.idr
View File

@ -70,7 +70,7 @@ parameters (defs : Defs, topopts : EvalOpts)
Env Term free -> LocalEnv free vars ->
Term (vars ++ free) -> Stack free -> Core (NF free)
eval env locs (Local fc mrig idx prf) stk
= evalLocal env locs fc mrig idx prf stk
= evalLocal env fc mrig idx prf stk locs
eval env locs (Ref fc nt fn) stk
= evalRef env locs False fc nt fn stk (NApp fc (NRef nt fn) stk)
eval env locs (Meta fc name idx args) stk
@ -115,12 +115,13 @@ parameters (defs : Defs, topopts : EvalOpts)
eval env locs (TType fc) stk = pure $ NType fc
evalLocal : {vars : _} ->
Env Term free -> LocalEnv free vars ->
Env Term free ->
FC -> Maybe RigCount ->
(idx : Nat) -> .(IsVar name idx (vars ++ free)) ->
Stack free ->
LocalEnv free vars ->
Core (NF free)
evalLocal {vars = []} env locs fc mrig idx prf stk
evalLocal {vars = []} env fc mrig idx prf stk locs
= if not (holesOnly topopts || argHolesOnly topopts) && isLet idx env
then
case getBinder prf env of
@ -133,10 +134,10 @@ parameters (defs : Defs, topopts : EvalOpts)
isLet Z _ = False
isLet (S k) (b :: env) = isLet k env
isLet (S k) [] = False
evalLocal env (MkClosure opts locs' env' tm' :: locs) fc mrig Z First stk
evalLocal env fc mrig Z First stk (MkClosure opts locs' env' tm' :: locs)
= evalWithOpts defs opts env' locs' tm' stk
evalLocal {free} {vars = x :: xs}
env (MkNFClosure nf :: locs) fc mrig Z First stk
env fc mrig Z First stk (MkNFClosure nf :: locs)
= applyToStack nf stk
where
applyToStack : NF free -> Stack free -> Core (NF free)
@ -148,7 +149,7 @@ parameters (defs : Defs, topopts : EvalOpts)
(NApp fc (NRef nt fn) args)
applyToStack (NApp fc (NLocal mrig idx p) args) stk
= let MkVar p' = insertVarNames {outer=[]} {ns = xs} idx p in
evalLocal env locs fc mrig _ p' (args ++ stk)
evalLocal env fc mrig _ p' (args ++ stk) locs
applyToStack (NDCon fc n t a args) stk
= pure $ NDCon fc n t a (args ++ stk)
applyToStack (NTCon fc n t a args) stk
@ -156,8 +157,8 @@ parameters (defs : Defs, topopts : EvalOpts)
applyToStack nf _ = pure nf
evalLocal {vars = x :: xs} {free}
env (_ :: locs) fc mrig (S idx) (Later p) stk
= evalLocal {vars = xs} env locs fc mrig idx p stk
env fc mrig (S idx) (Later p) stk (_ :: locs)
= evalLocal {vars = xs} env fc mrig idx p stk locs
evalMeta : {vars : _} ->
Env Term free -> LocalEnv free vars ->
@ -289,7 +290,7 @@ parameters (defs : Defs, topopts : EvalOpts)
= do let x' : IsVar _ _ ((args ++ vars) ++ free)
= rewrite sym (appendAssociative args vars free) in
varExtend x
xval <- evalLocal env loc fc Nothing idx x' []
xval <- evalLocal env fc Nothing idx x' [] loc
findAlt env loc opts fc stk xval alts def
evalTree {args} {vars} {free} env loc opts fc stk (STerm tm) def
= do let tm' : Term ((args ++ vars) ++ free)

1
src/Core/TT.idr
View File

@ -871,6 +871,7 @@ mkLocals bs (TType fc) = TType fc
export
refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
refsToLocals None y = y
refsToLocals bs y = mkLocals {later = []} bs y
-- Replace any reference to 'x' with a locally bound name 'new'

2
src/Idris/Main.idr
View File

@ -145,7 +145,7 @@ stMain opts
replIDE {c} {u} {m}
else do
iputStrLn $ "Welcome to Idris 2 version " ++ version
++ ". Fingers crossed!"
++ ". Please be gentle."
repl {c} {u} {m}
else
-- exit with an error code if there was an error, otherwise

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

@ -288,9 +288,9 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
exp <- getTerm expected
-- If we don't know the target type on the first attempt,
-- delay
when (not delayed &&
!(holeIn (gamma defs) exp)) $
throw (AllFailed [])
-- when (not delayed &&
-- !(holeIn (gamma defs) exp)) $
-- throw (AllFailed [])
-- We can't just use the old NF on the second attempt,
-- because we might know more now, so recalculate it
let exp' = if delayed
@ -298,6 +298,7 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
else expected
logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++
" at " ++ show fc ++
"\nTarget type ") env exp'
let tryall = case uniq of
FirstSuccess => anyOne fc

2
tests/idris2/basic001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Vect (Vect.idr)
Welcome to Idris 2 version 0.0. Fingers crossed!
Welcome to Idris 2 version 0.0. Please be gentle.
Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat
Mismatch between:

4
tests/idris2/import001/expected
View File

@ -1,10 +1,10 @@
1/3: Building Nat (Nat.idr)
2/3: Building Mult (Mult.idr)
3/3: Building Test (Test.idr)
Welcome to Idris 2 version 0.0. Fingers crossed!
Welcome to Idris 2 version 0.0. Please be gentle.
Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
Test> Bye for now!
2/3: Building Mult (Mult.idr)
Welcome to Idris 2 version 0.0. Fingers crossed!
Welcome to Idris 2 version 0.0. Please be gentle.
Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
Test> Bye for now!