git.iko.soy/Idris-dev
on master help sign in
Shave a bit more off IBC size
commitdfc3e44890e383dede29b0d965a96b2df70b7b8b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 Jan 2014, 12:18 (13 years ago) parentba15257
3 files changed+21−23
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+4−4 src/Idris/Core/ProofState.hs+4−2 src/Idris/IBC.hs+13−17
src/Idris/AbsSyntax.hs+4−4
@@ -1068,7 +1068,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
10681068 imps top env (PPi (Imp l _ doc _) n ty sc)
10691069 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
10701070 (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,
10721072 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10731073 imps True (n:env) sc
10741074 imps top env (PPi (Exp l _ doc _) n ty sc)
@@ -1076,7 +1076,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
10761076 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
10771077 _ -> [])
10781078 (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,
10801080 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10811081 imps True (n:env) sc
10821082 imps top env (PPi (Constraint l _ doc) n ty sc)
@@ -1084,7 +1084,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
10841084 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
10851085 _ -> [])
10861086 (decls, ns) <- get -- ignore decls in HO types
1087− put (PConstraint 10 l ty doc : decls,
1087+ put (PConstraint 10 l Placeholder doc : decls,
10881088 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10891089 imps True (n:env) sc
10901090 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) $
10921092 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
10931093 _ -> [])
10941094 (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,
10961096 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10971097 imps True (n:env) sc
10981098 imps top env (PEq _ l r)
src/Idris/Core/ProofState.hs+4−2
@@ -739,11 +739,13 @@ keepGiven du (u@(n, _) : us) hs
739739 | n `elem` du = u : keepGiven du us hs
740740keepGiven du (u : us) hs = keepGiven du us hs
741741
742−updateSolved [] x = x
743742updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
744743 updateSolved' xs x
744+updateSolved' [] x = x
745745updateSolved' xs (Bind n (Hole ty) t)
746− | Just v <- lookup n xs = psubst n v (updateSolved' xs t)
746+ | Just v <- lookup n xs = case xs of
747+ [_] -> psubst n v t
748+ _ -> psubst n v (updateSolved' xs t)
747749updateSolved' xs (Bind n b t)
748750 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
749751updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
src/Idris/IBC.hs+13−17
@@ -24,7 +24,7 @@ import Debug.Trace
2424import Paths_idris
2525
2626ibcVersion :: Word8
27−ibcVersion = 51
27+ibcVersion = 52
2828
2929data IBCFile = IBCFile { ver :: Word8,
3030 sourcefile :: FilePath,
@@ -208,7 +208,9 @@ pImports fs
208208pImps :: [(Name, [PArg])] -> Idris ()
209209pImps imps = mapM_ (\ (n, imp) ->
210210 do i <- getIState
211− putIState (i { idris_implicits
211+ case lookupDefAcc n False (tt_ctxt i) of
212+ [(n, Hidden)] -> return ()
213+ _ -> putIState (i { idris_implicits
212214 = addDef n imp (idris_implicits i) }))
213215 imps
214216
@@ -371,13 +373,11 @@ instance Binary CGInfo where
371373instance Binary FC where
372374 put (FC x1 x2 x3)
373375 = do put x1
374− put x2
375− put x3
376+ put (x2 * 65536 + x3)
376377 get
377378 = do x1 <- get
378− x2 <- get
379− x3 <- get
380− return (FC x1 x2 x3)
379+ x2x3 <- get
380+ return (FC x1 (x2x3 `div` 65536) (x2x3 `mod` 65536))
381381
382382
383383instance Binary Name where
@@ -624,22 +624,18 @@ instance Binary NameType where
624624 Bound -> putWord8 0
625625 Ref -> putWord8 1
626626 DCon x1 x2 -> do putWord8 2
627− put x1
628− put x2
627+ put (x1 * 65536 + x2)
629628 TCon x1 x2 -> do putWord8 3
630− put x1
631− put x2
629+ put (x1 * 65536 + x2)
632630 get
633631 = do i <- getWord8
634632 case i of
635633 0 -> return Bound
636634 1 -> return Ref
637− 2 -> do x1 <- get
638− x2 <- get
639− return (DCon x1 x2)
640− 3 -> do x1 <- get
641− x2 <- get
642− return (TCon x1 x2)
635+ 2 -> do x1x2 <- get
636+ return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
637+ 3 -> do x1x2 <- get
638+ return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
643639 _ -> error "Corrupted binary data for NameType"
644640
645641