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

Cache whether a local is let bound, if we can

Browse Source 
Since lookup up a binding can be expensive in a big environment, and we
only need to reduce it if it turns out to be a let, caching it can be a
noticeable win
This commit is contained in:
Edwin Brady 2019-06-23 23:12:27 +01:00
parent 9c902de5d1
commit 40ea548a65
9 changed files with 51 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2.ipkg
View File

@ -118,6 +118,7 @@ modules =
sourcedir = src
executable = idris2
-- opts = "--cg-opt -O2 --partial-eval"
-- opts = "--cg-opt -pg --partial-eval"
opts = "--partial-eval"
main = Idris.Main

8
src/Core/CaseBuilder.idr
View File

@ -524,7 +524,7 @@ groupCons fc fn pvars cs
-- In 'As' replace the name on the RHS with a reference to the
-- variable we're doing the case split on
addGroup (PAs fc n p) pprf pats rhs acc
= addGroup p pprf pats (substName n (Local fc Nothing _ pprf) rhs) acc
= addGroup p pprf pats (substName n (Local fc (Just True) _ pprf) rhs) acc
addGroup (PCon _ n t a pargs) pprf pats rhs acc
= addConG n t pargs pats rhs acc
addGroup (PTyCon _ n a pargs) pprf pats rhs acc
@ -801,13 +801,13 @@ mutual
-- replace the name with the relevant variable on the rhs
updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) rhs)
= pure $ MkPatClause (n :: pvars)
!(substInPats fc a (Local pfc Nothing _ prf) pats)
(substName n (Local pfc Nothing _ prf) rhs)
!(substInPats fc a (Local pfc (Just False) _ prf) pats)
(substName n (Local pfc (Just False) _ prf) rhs)
-- If it's an as pattern, replace the name with the relevant variable on
-- the rhs then continue with the inner pattern
updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) rhs)
= do pats' <- substInPats fc a (mkTerm _ pat) pats
let rhs' = substName n (Local pfc Nothing _ prf) rhs
let rhs' = substName n (Local pfc (Just True) _ prf) rhs
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') rhs')
-- match anything, name won't appear in rhs but need to update
-- LHS pattern types based on what we've learned

18
src/Core/Normalise.idr
View File

@ -116,24 +116,28 @@ parameters (defs : Defs, topopts : EvalOpts)
evalLocal : {vars : _} ->
Env Term free ->
FC -> Maybe RigCount ->
FC -> Maybe Bool ->
(idx : Nat) -> .(IsVar name idx (vars ++ free)) ->
Stack free ->
LocalEnv free vars ->
Core (NF free)
evalLocal {vars = []} env fc mrig idx prf stk locs
= if not (holesOnly topopts || argHolesOnly topopts) && isLet idx env
= if not (holesOnly topopts || argHolesOnly topopts) && isLet mrig idx env
then
case getBinder prf env of
Let _ val _ => eval env [] val stk
_ => pure $ NApp fc (NLocal mrig idx prf) stk
else pure $ NApp fc (NLocal mrig idx prf) stk
where
isLet : Nat -> Env tm vars -> Bool
isLet Z (Let _ _ _ :: env) = True
isLet Z _ = False
isLet (S k) (b :: env) = isLet k env
isLet (S k) [] = False
isLet' : Nat -> Env tm vars -> Bool
isLet' Z (Let _ _ _ :: env) = True
isLet' Z _ = False
isLet' (S k) (b :: env) = isLet' k env
isLet' (S k) [] = False
isLet : Maybe Bool -> Nat -> Env tm vars -> Bool
isLet (Just t) _ _ = t
isLet _ n env = isLet' n env
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}

13
src/Core/TT.idr
View File

@ -351,7 +351,7 @@ data LazyReason = LInf | LLazy | LUnknown
public export
data Term : List Name -> Type where
Local : {name : _} ->
FC -> Maybe RigCount ->
FC -> Maybe Bool ->
(idx : Nat) -> .(IsVar name idx vars) -> Term vars
Ref : FC -> NameType -> (name : Name) -> Term vars
-- Metavariables and the scope they are applied to
@ -893,7 +893,7 @@ export
resolveNames : (vars : List Name) -> Term vars -> Term vars
resolveNames vars (Ref fc Bound name)
= case isVar name vars of
Just (MkVar prf) => Local fc Nothing _ prf
Just (MkVar prf) => Local fc (Just False) _ prf
_ => Ref fc Bound name
resolveNames vars (Meta fc n i xs)
= Meta fc n i (map (resolveNames vars) xs)
@ -924,7 +924,7 @@ namespace SubstEnv
SubstEnv ds vars -> SubstEnv (d :: ds) vars
findDrop : {drop : _} -> {idx : Nat} ->
FC -> Maybe RigCount -> .(IsVar name idx (drop ++ vars)) ->
FC -> Maybe Bool -> .(IsVar name idx (drop ++ vars)) ->
SubstEnv drop vars -> Term vars
findDrop {drop = []} fc r var env = Local fc r _ var
findDrop {drop = x :: xs} fc r First (tm :: env) = tm
@ -932,7 +932,7 @@ namespace SubstEnv
= findDrop fc r p env
find : {outer : _} -> {idx : Nat} ->
FC -> Maybe RigCount -> .(IsVar name idx (outer ++ (drop ++ vars))) ->
FC -> Maybe Bool -> .(IsVar name idx (outer ++ (drop ++ vars))) ->
SubstEnv drop vars ->
Term (outer ++ vars)
find {outer = []} fc r var env = findDrop fc r var env
@ -1050,7 +1050,10 @@ export Show (Term vars) where
show tm = let (fn, args) = getFnArgs tm in showApp fn args
where
showApp : Term vars -> List (Term vars) -> String
showApp (Local {name} _ _ idx _) [] = show name ++ "[" ++ show idx ++ "]"
showApp (Local {name} _ c idx _) []
= case c of
Just _ => show name ++ "[" ++ show idx ++ "!]"
_ => show name ++ "[" ++ show idx ++ "]"
showApp (Ref _ _ n) [] = show n
showApp (Meta _ n i args) []
= "?" ++ show n ++ "_" ++ show args

12
src/Core/TTC.idr
View File

@ -201,8 +201,10 @@ mutual
toBuf b (Local {name} fc c idx y)
= if idx < 244
then do toBuf b (prim__truncBigInt_B8 (12 + cast idx))
toBuf b c
toBuf b name
else do tag 0
toBuf b c
toBuf b name
toBuf b idx
toBuf b (Ref fc nt name)
@ -243,9 +245,10 @@ mutual
fromBuf b
= case !getTag of
0 => do name <- fromBuf b
0 => do c <- fromBuf b
name <- fromBuf b
idx <- fromBuf b
pure (Local {name} emptyFC Nothing idx (mkPrf idx))
pure (Local {name} emptyFC c idx (mkPrf idx))
1 => do nt <- fromBuf b; name <- fromBuf b
pure (Ref emptyFC nt name)
2 => do n <- fromBuf b
@ -270,9 +273,10 @@ mutual
pure (PrimVal emptyFC c)
10 => pure (Erased emptyFC)
11 => pure (TType emptyFC)
idxp => do name <- fromBuf b
idxp => do c <- fromBuf b
name <- fromBuf b
let idx = fromInteger (prim__sextB8_BigInt idxp - 12)
pure (Local {name} emptyFC Nothing idx (mkPrf idx))
pure (Local {name} emptyFC c idx (mkPrf idx))
export
TTC Pat where

20
src/Core/UnifyState.idr
View File

@ -275,14 +275,14 @@ mkConstantAppArgs : Bool -> FC -> Env Term vars ->
mkConstantAppArgs lets fc [] wkns = []
mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns
= let rec = mkConstantAppArgs {done} lets fc env (wkns ++ [x]) in
if lets || notLet b
then Local fc Nothing (length wkns) (mkVar wkns) ::
if lets || not (isLet b)
then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
where
notLet : Binder (Term vars) -> Bool
notLet (Let _ _ _) = False
notLet _ = True
isLet : Binder (Term vars) -> Bool
isLet (Let _ _ _) = True
isLet _ = False
mkVar : (wkns : List Name) ->
IsVar name (length wkns) (wkns ++ name :: vars ++ done)
@ -305,14 +305,14 @@ mkConstantAppArgsOthers {done} {vars = x :: xs}
mkConstantAppArgsOthers {done} {vars = x :: xs}
lets fc (b :: env) (DropCons p) wkns
= let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns ++ [x]) in
if lets || notLet b
then Local fc Nothing (length wkns) (mkVar wkns) ::
if lets || not (isLet b)
then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
rewrite appendAssociative wkns [x] (xs ++ done) in rec
else rewrite appendAssociative wkns [x] (xs ++ done) in rec
where
notLet : Binder (Term vars) -> Bool
notLet (Let _ _ _) = False
notLet _ = True
isLet : Binder (Term vars) -> Bool
isLet (Let _ _ _) = True
isLet _ = False
mkVar : (wkns : List Name) ->
IsVar name (length wkns) (wkns ++ name :: vars ++ done)

2
src/Core/Value.idr
View File

@ -59,7 +59,7 @@ mutual
-- The head of a value: things you can apply arguments to
public export
data NHead : List Name -> Type where
NLocal : Maybe RigCount -> (idx : Nat) -> IsVar name idx vars ->
NLocal : Maybe Bool -> (idx : Nat) -> IsVar name idx vars ->
NHead vars
NRef : NameType -> Name -> NHead vars
NMeta : Name -> Int -> List (Closure vars) -> NHead vars

9
src/TTImp/Elab/App.idr
View File

@ -28,13 +28,14 @@ getNameType rigc env fc x
= case defined x env of
Just (MkIsDefined rigb lv) =>
do rigSafe rigb rigc
let bty = binderType (getBinder lv env)
let binder = getBinder lv env
let bty = binderType binder
addNameType fc x env bty
when (isLinear rigb) $
do est <- get EST
put EST
(record { linearUsed $= ((MkVar lv) :: ) } est)
pure (Local fc (Just rigb) _ lv, gnf env bty)
pure (Local fc (Just (isLet binder)) _ lv, gnf env bty)
Nothing =>
do defs <- get Ctxt
[(fullname, i, def)] <- lookupCtxtName x (gamma defs)
@ -48,6 +49,10 @@ getNameType rigc env fc x
addNameType fc x env (embed (type def))
pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
where
isLet : Binder t -> Bool
isLet (Let _ _ _) = True
isLet _ = False
rigSafe : RigCount -> RigCount -> Core ()
rigSafe Rig1 RigW = throw (LinearMisuse fc x Rig1 RigW)
rigSafe Rig0 RigW = throw (LinearMisuse fc x Rig0 RigW)

2
src/TTImp/ProcessDef.idr
View File

@ -374,7 +374,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
let scenv = Pi RigW Explicit wvalTy :: wvalEnv
wtyScope <- replace defs scenv !(nf defs scenv (weaken wval))
(Local fc (Just RigW) _ First)
(Local fc (Just False) _ First)
!(nf defs scenv
(weaken (bindNotReq fc 0 env' withSub reqty)))
let bNotReq = Bind fc wargn (Pi RigW Explicit wvalTy) wtyScope