edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-03 10:14:53 +03:00
Code Issues Projects Releases Wiki Activity

Some small tweaks

Browse Source 
These are attempts to allocate slightly less memory. They don't achieve
much, but also don't do any harm...
This commit is contained in:
Edwin Brady 2019-05-20 13:36:32 +01:00
parent 0ac539fdc2
commit 11a72dc953
4 changed files with 69 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/Core/TT.idr
View File

@ -304,7 +304,7 @@ dropVar (n :: xs) (Later p) = n :: dropVar xs p
public export
data Var : List Name -> Type where
MkVar : {i : Nat} -> {n : _} -> .(IsVar n i vars) -> Var vars
MkVar : {i : Nat} -> .(IsVar n i vars) -> Var vars
export
sameVar : Var xs -> Var xs -> Bool
@ -316,7 +316,7 @@ varIdx (MkVar {i} _) = i
export
Show (Var ns) where
show (MkVar {n} _) = show n
show (MkVar {i} _) = show i
public export
record AppInfo where
@ -402,6 +402,34 @@ Eq LazyReason where
(==) LLazy LLazy = True
(==) _ _ = False
export
Eq a => Eq (Binder a) where
(Lam c p ty) == (Lam c' p' ty') = c == c' && p == p' && ty == ty'
(Let c v ty) == (Let c' v' ty') = c == c' && v == v' && ty == ty'
(Pi c p ty) == (Pi c' p' ty') = c == c' && p == p' && ty == ty'
(PVar c ty) == (PVar c' ty') = c == c' && ty == ty'
(PLet c v ty) == (PLet c' v' ty') = c == c' && v == v' && ty == ty'
(PVTy c ty) == (PVTy c' ty') = c == c' && ty == ty'
_ == _ = False
export
Eq (Term vars) where
(==) (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
(==) (Ref _ _ n) (Ref _ _ n') = n == n'
(==) (Meta _ _ i args) (Meta _ _ i' args')
= assert_total (i == i' && args == args')
(==) (Bind _ _ b sc) (Bind _ _ b' sc')
= assert_total (b == b' && sc == believe_me sc')
(==) (App _ f _ a) (App _ f' _ a') = f == f' && a == a'
(==) (As _ a p) (As _ a' p') = a == a' && p == p'
(==) (TDelayed _ _ t) (TDelayed _ _ t') = t == t'
(==) (TDelay _ _ t) (TDelay _ _ t') = t == t'
(==) (TForce _ t) (TForce _ t') = t == t'
(==) (PrimVal _ c) (PrimVal _ c') = c == c'
(==) (Erased _) (Erased _) = True
(==) (TType _) (TType _) = True
(==) _ _ = False
public export
interface Weaken (tm : List Name -> Type) where
weaken : tm vars -> tm (n :: vars)

48
src/Core/Unify.idr
View File

@ -149,20 +149,13 @@ unifyArgs mode loc env _ _ = ufail loc ""
-- are not variables, fail if there's any repetition of variables
-- We use this to check that the pattern unification rule is applicable
-- when solving a metavariable applied to arguments
getVars : List (NF vars) -> Maybe (List (Var vars))
getVars [] = Just []
getVars (NApp fc (NLocal r idx v) [] :: xs)
= if vIn xs then Nothing
else do xs' <- getVars xs
getVarsBelow : Nat -> List (NF vars) -> Maybe (List (Var vars))
getVarsBelow max [] = Just []
getVarsBelow max (NApp fc (NLocal r idx v) [] :: xs)
= if idx >= max then Nothing
else do xs' <- getVarsBelow idx xs
pure (MkVar v :: xs')
where
-- Check the variable doesn't appear later
vIn : List (NF vars) -> Bool
vIn [] = False
vIn (NApp _ (NLocal r idx' el') [] :: xs)
= if idx == idx' then True else vIn xs
vIn (_ :: xs) = vIn xs
getVars (_ :: xs) = Nothing
getVarsBelow _ (_ :: xs) = Nothing
-- Make a sublist representing the variables used in the application.
-- We'll use this to ensure that local variables which appear in a term
@ -209,17 +202,20 @@ patternEnv : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{vars : _} ->
Env Term vars -> List (AppInfo, Closure vars) ->
Core (Maybe (newvars ** (List (Var newvars),
Core (Maybe (newvars ** (Maybe (List (Var newvars)),
SubVars newvars vars)))
patternEnv env args
patternEnv {vars} env args
= do defs <- get Ctxt
empty <- clearDefs defs
args' <- traverse (evalArg empty) args
case getVars args' of
case getVarsBelow 1000000 args' of
Nothing => pure Nothing
Just vs =>
let (newvars ** svs) = toSubVars _ vs in
pure (Just (newvars ** (updateVars vs svs, svs)))
pure (Just (newvars **
(if vars == newvars
then Nothing
else Just (updateVars vs svs), svs)))
where
-- Update the variable list to point into the sub environment
-- (All of these will succeed because the SubVars we have comes from
@ -240,7 +236,7 @@ instantiate : {auto c : Ref Ctxt Defs} ->
{newvars : _} ->
FC -> Env Term vars ->
(metavar : Name) -> (mref : Int) -> (mdef : GlobalDef) ->
List (Var newvars) -> -- Variable each argument maps to
Maybe (List (Var newvars)) -> -- Variable each argument maps to
Term vars -> -- original, just for error message
Term newvars -> -- shrunk environment
Core ()
@ -294,10 +290,10 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
mkDef : (got : List Name) -> (vs : List Name) -> SnocList vs ->
CompatibleVars got rest ->
List (Var (vs ++ got)) -> Term (vs ++ got) ->
Maybe (List (Var (vs ++ got))) -> Term (vs ++ got) ->
NF [] -> Core (Term rest)
mkDef got [] Empty cvs locs tm ty
= do let Just tm' = updateLocs (reverse locs) tm
= do let Just tm' = maybe (Just tm) (\lvs => updateLocs (reverse lvs) tm) locs
| Nothing => ufail loc ("Can't make solution for " ++ show mname)
pure (renameVars cvs tm')
mkDef got (vs ++ [v]) (Snoc rec) cvs locs tm (NBind bfc x (Pi c _ ty) scfn)
@ -356,7 +352,7 @@ mutual
(metaname : Name) -> (metaref : Int) ->
(margs : List (AppInfo, Closure vars)) ->
(margs' : List (AppInfo, Closure vars)) ->
List (Var newvars) ->
Maybe (List (Var newvars)) ->
SubVars newvars vars ->
(solfull : Term vars) -> -- Original solution
(soln : Term newvars) -> -- Solution with shrunk environment
@ -367,8 +363,7 @@ mutual
empty <- clearDefs defs
-- if the terms are the same, this isn't a solution
-- but they are already unifying, so just return
if !(convert empty env (NApp loc (NMeta mname mref margs) margs')
solnf)
if solutionHeadSame solnf
then pure success
else -- Rather than doing the occurs check here immediately,
-- we'll wait until all metavariables are resolved, and in
@ -379,6 +374,13 @@ mutual
| Nothing => throw (InternalError ("Can't happen: Lost hole " ++ show mname))
instantiate loc env mname mref hdef locs solfull stm
pure solvedHole
where
-- Only need to check the head metavar is the same, we've already
-- checked the rest if they are the same (and we couldn't instantiate it
-- anyway...)
solutionHeadSame : NF vars -> Bool
solutionHeadSame (NApp _ (NMeta _ shead _) _) = shead == mref
solutionHeadSame _ = False
unifyHole : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->

12
src/Data/IntMap.idr
View File

@ -192,12 +192,14 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
Right t3' => Left (merge3 t1 k1 t2 k2 t3')
treeToList : Tree n v -> List (Key, v)
treeToList = treeToList' (:: [])
treeToList = treeToList' []
where
treeToList' : ((Key, v) -> List (Key, v)) -> Tree n v -> List (Key, v)
treeToList' cont (Leaf k v) = cont (k, v)
treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
treeToList' : List (Key, v) -> Tree n v -> List (Key, v)
treeToList' rest (Leaf k v) = (k, v) :: rest
treeToList' rest (Branch2 t1 _ t2)
= treeToList' (treeToList' rest t2) t1
treeToList' rest (Branch3 t1 _ t2 _ t3)
= treeToList' (treeToList' (treeToList' rest t3) t2) t1
export
data IntMap : Type -> Type where

12
src/Data/NameMap.idr
View File

@ -194,12 +194,14 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
Right t3' => Left (merge3 t1 k1 t2 k2 t3')
treeToList : Tree n v -> List (Key, v)
treeToList = treeToList' (:: [])
treeToList = treeToList' []
where
treeToList' : ((Key, v) -> List (Key, v)) -> Tree n v -> List (Key, v)
treeToList' cont (Leaf k v) = cont (k, v)
treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
treeToList' : List (Key, v) -> Tree n v -> List (Key, v)
treeToList' rest (Leaf k v) = (k, v) :: rest
treeToList' rest (Branch2 t1 _ t2)
= treeToList' (treeToList' rest t2) t1
treeToList' rest (Branch3 t1 _ t2 _ t3)
= treeToList' (treeToList' (treeToList' rest t3) t2) t1
export
data NameMap : Type -> Type where