git.iko.soy/Idris-dev
on master help sign in
Shave a bit more off IBC size
dfc3e44Edwin Brady
src/Idris/AbsSyntax.hs+4−4
compare with master
unifiedsplit
@@ -1068,7 +1068,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1068 imps top env (PPi (Imp l _ doc _) n ty sc)
1068 imps top env (PPi (Imp l _ doc _) n ty sc)
1069 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1069 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1070 (decls , ns) <- get
1070 (decls , ns) <- get
1071− put (PImp (getPriority ist ty) True l n ty doc : decls,
1071+ put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1072 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1072 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1073 imps True (n:env) sc
1073 imps True (n:env) sc
1074 imps top env (PPi (Exp l _ doc _) n ty sc)
1074 imps top env (PPi (Exp l _ doc _) n ty sc)
@@ -1076,7 +1076,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1076 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1076 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1077 _ -> [])
1077 _ -> [])
1078 (decls, ns) <- get -- ignore decls in HO types
1078 (decls, ns) <- get -- ignore decls in HO types
1079− put (PExp (getPriority ist ty) l ty doc : decls,
1079+ put (PExp (getPriority ist ty) l Placeholder doc : decls,
1080 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1080 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1081 imps True (n:env) sc
1081 imps True (n:env) sc
1082 imps top env (PPi (Constraint l _ doc) n ty sc)
1082 imps top env (PPi (Constraint l _ doc) n ty sc)
@@ -1084,7 +1084,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1084 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1084 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1085 _ -> [])
1085 _ -> [])
1086 (decls, ns) <- get -- ignore decls in HO types
1086 (decls, ns) <- get -- ignore decls in HO types
1087− put (PConstraint 10 l ty doc : decls,
1087+ put (PConstraint 10 l Placeholder doc : decls,
1088 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1088 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1089 imps True (n:env) sc
1089 imps True (n:env) sc
1090 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1090 imps top env (PPi (TacImp l _ scr doc) n ty sc)
@@ -1092,7 +1092,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1092 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1092 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1093 _ -> [])
1093 _ -> [])
1094 (decls, ns) <- get -- ignore decls in HO types
1094 (decls, ns) <- get -- ignore decls in HO types
1095− put (PTacImplicit 10 l n scr ty doc : decls,
1095+ put (PTacImplicit 10 l n scr Placeholder doc : decls,
1096 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1096 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1097 imps True (n:env) sc
1097 imps True (n:env) sc
1098 imps top env (PEq _ l r)
1098 imps top env (PEq _ l r)
src/Idris/Core/ProofState.hs+4−2
@@ -739,11 +739,13 @@ keepGiven du (u@(n, _) : us) hs
739 | n `elem` du = u : keepGiven du us hs
739 | n `elem` du = u : keepGiven du us hs
740keepGiven du (u : us) hs = keepGiven du us hs
740keepGiven du (u : us) hs = keepGiven du us hs
741
741
742−updateSolved [] x = x
743updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
742updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
744 updateSolved' xs x
743 updateSolved' xs x
744+updateSolved' [] x = x
745updateSolved' xs (Bind n (Hole ty) t)
745updateSolved' xs (Bind n (Hole ty) t)
746+ | Just v <- lookup n xs = case xs of
747+ [_] -> psubst n v t
746− | Just v <- lookup n xs = psubst n v (updateSolved' xs t)
748+ _ -> psubst n v (updateSolved' xs t)
747updateSolved' xs (Bind n b t)
749updateSolved' xs (Bind n b t)
748 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
750 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
749updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
751updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
src/Idris/IBC.hs+13−17
@@ -24,7 +24,7 @@ import Debug.Trace
24import Paths_idris
24import Paths_idris
25
25
26ibcVersion :: Word8
26ibcVersion :: Word8
27−ibcVersion = 51
27+ibcVersion = 52
28
28
29data IBCFile = IBCFile { ver :: Word8,
29data IBCFile = IBCFile { ver :: Word8,
30 sourcefile :: FilePath,
30 sourcefile :: FilePath,
@@ -208,7 +208,9 @@ pImports fs
208pImps :: [(Name, [PArg])] -> Idris ()
208pImps :: [(Name, [PArg])] -> Idris ()
209pImps imps = mapM_ (\ (n, imp) ->
209pImps imps = mapM_ (\ (n, imp) ->
210 do i <- getIState
210 do i <- getIState
211+ case lookupDefAcc n False (tt_ctxt i) of
212+ [(n, Hidden)] -> return ()
211− putIState (i { idris_implicits
213+ _ -> putIState (i { idris_implicits
212 = addDef n imp (idris_implicits i) }))
214 = addDef n imp (idris_implicits i) }))
213 imps
215 imps
214
216
@@ -371,13 +373,11 @@ instance Binary CGInfo where
371instance Binary FC where
373instance Binary FC where
372 put (FC x1 x2 x3)
374 put (FC x1 x2 x3)
373 = do put x1
375 = do put x1
374− put x2
376+ put (x2 * 65536 + x3)
375− put x3
376 get
377 get
377 = do x1 <- get
378 = do x1 <- get
378− x2 <- get
379− x3 <- get
379+ x2x3 <- get
380− return (FC x1 x2 x3)
380+ return (FC x1 (x2x3 `div` 65536) (x2x3 `mod` 65536))
381
381
382
382
383instance Binary Name where
383instance Binary Name where
@@ -624,22 +624,18 @@ instance Binary NameType where
624 Bound -> putWord8 0
624 Bound -> putWord8 0
625 Ref -> putWord8 1
625 Ref -> putWord8 1
626 DCon x1 x2 -> do putWord8 2
626 DCon x1 x2 -> do putWord8 2
627− put x1
627+ put (x1 * 65536 + x2)
628− put x2
629 TCon x1 x2 -> do putWord8 3
628 TCon x1 x2 -> do putWord8 3
630− put x1
629+ put (x1 * 65536 + x2)
631− put x2
632 get
630 get
633 = do i <- getWord8
631 = do i <- getWord8
634 case i of
632 case i of
635 0 -> return Bound
633 0 -> return Bound
636 1 -> return Ref
634 1 -> return Ref
637− 2 -> do x1 <- get
638− x2 <- get
635+ 2 -> do x1x2 <- get
639− return (DCon x1 x2)
636+ return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
640− 3 -> do x1 <- get
641− x2 <- get
637+ 3 -> do x1x2 <- get
642− return (TCon x1 x2)
638+ return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
643 _ -> error "Corrupted binary data for NameType"
639 _ -> error "Corrupted binary data for NameType"
644
640
645
641