ddced5c · Idris-dev · git.iko.soy

idris.cabal+3

@@ -250,6 +250,9 @@ Extra-source-files:

250250 test/reg050/run

251251 test/reg050/*.idr

252252 test/reg050/expected

253+ test/reg051/run

254+ test/reg051/*.idr

255+ test/reg051/expected

253256

254257 test/basic001/run

255258 test/basic001/*.idr

src/Idris/AbsSyntax.hs+3

@@ -132,6 +132,9 @@ clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }

132132setFlags :: Name -> [FnOpt] -> Idris ()

133133setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }

134134

135+setFnInfo :: Name -> FnInfo -> Idris ()

136+setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }

137+

135138setAccessibility :: Name -> Accessibility -> Idris ()

136139setAccessibility n a

137140 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+11−1

@@ -158,6 +158,7 @@ data IState = IState {

158158 idris_calledgraph :: Ctxt [Name],

159159 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),

160160 idris_tyinfodata :: Ctxt TIData,

161+ idris_fninfo :: Ctxt FnInfo,

161162 idris_totcheck :: [(FC, Name)], -- names to check totality on

162163 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

163164 idris_totcheckfail :: [(FC, String)],

@@ -260,6 +261,7 @@ data IBCWrite = IBCFix FixDecl

260261 | IBCMetaInformation Name MetaInformation

261262 | IBCTotal Name Totality

262263 | IBCFlags Name [FnOpt]

264+ | IBCFnInfo Name FnInfo

263265 | IBCTrans (Term, Term)

264266 | IBCErrRev (Term, Term)

265267 | IBCCG Name

@@ -280,7 +282,7 @@ idrisInit :: IState

280282idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

281283 emptyContext emptyContext emptyContext emptyContext

282284 emptyContext emptyContext emptyContext emptyContext

283− emptyContext emptyContext

285+ emptyContext emptyContext emptyContext

284286 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

285287 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

286288 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

@@ -490,6 +492,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

490492 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

491493 | Reflection -- a reflecting function, compile-time only

492494 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

495+ | Constructor -- Data constructor type

493496 deriving (Show, Eq)

494497{-!

495498deriving instance Binary FnOpt

@@ -905,6 +908,13 @@ data TIData = TIPartial -- ^ a function with a partially defined type

905908 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

906909 deriving Show

907910

911+-- | Miscellaneous information about functions

912+data FnInfo = FnInfo { fn_params :: [Int] }

913+ deriving Show

914+{-!

915+deriving instance Binary FnInfo

916+!-}

917+

908918data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting

909919 detaggable :: Bool }

910920 deriving Show

src/Idris/Elab/Clause.hs−49

@@ -422,55 +422,6 @@ checkPossible info fc tcgen fname lhs_in

422422 | Ref <- y = True

423423 | otherwise = False -- name is different, unrecoverable

424424

425−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

426− = nub $ getFixedInType i env [] t ++

427− getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

428−getFixedInType i env (_ : is) (Bind n (Pi t) sc)

429− = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

430−getFixedInType i env is tm@(App f a)

431− | (P _ tn _, args) <- unApply tm

432− = case lookupCtxt tn (idris_datatypes i) of

433− [t] -> nub $ paramNames args env (param_pos t) ++

434− getFixedInType i env is f ++

435− getFixedInType i env is a

436− [] -> nub $ getFixedInType i env is f ++

437− getFixedInType i env is a

438− | otherwise = nub $ getFixedInType i env is f ++

439− getFixedInType i env is a

440−getFixedInType i _ _ _ = []

441−

442−getFlexInType i env ps (Bind n (Pi t) sc)

443− = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

444− getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

445−getFlexInType i env ps tm@(App f a)

446− | (P _ tn _, args) <- unApply tm

447− = case lookupCtxt tn (idris_datatypes i) of

448− [t] -> nub $ paramNames args env [x | x <- [0..length args],

449− not (x `elem` param_pos t)]

450− ++ getFlexInType i env ps f ++

451− getFlexInType i env ps a

452− [] -> nub $ getFlexInType i env ps f ++

453− getFlexInType i env ps a

454− | otherwise = nub $ getFlexInType i env ps f ++

455− getFlexInType i env ps a

456−getFlexInType i _ _ _ = []

457−

458−-- Treat a name as a parameter if it appears in parameter positions in

459−-- types, and never in a non-parameter position in a (non-param) argument type.

460−

461−getParamsInType i env ps t = let fix = getFixedInType i env ps t

462− flex = getFlexInType i env fix t in

463− [x | x <- fix, not (x `elem` flex)]

464−

465−paramNames args env [] = []

466−paramNames args env (p : ps)

467− | length args > p = case args!!p of

468− P _ n _ -> if n `elem` env

469− then n : paramNames args env ps

470− else paramNames args env ps

471− _ -> paramNames args env ps

472− | otherwise = paramNames args env ps

473−

474425propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

475426propagateParams i ps t tm@(PApp _ (PRef fc n) args)

476427 = PApp fc (PRef fc n) (addP t args)

src/Idris/Elab/Data.hs+1−1

@@ -199,7 +199,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

199199 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

200200elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

201201 = do checkUndefined fc n

202− (cty, t, inacc) <- buildType info syn fc [] n (if codata then mkLazy t_in else t_in)

202+ (cty, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

203203 ctxt <- getContext

204204 let cty' = normalise ctxt [] cty

205205

src/Idris/Elab/Type.hs+10

@@ -93,12 +93,22 @@ buildType info syn fc opts n ty' = do

9393 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

9494 addIBC (IBCImp n)

9595

96+ when (Constructor `notElem` opts) $ do

97+ let pnames = getParamsInType i [] impls cty

98+ let fninfo = FnInfo (param_pos 0 pnames cty)

99+ setFnInfo n fninfo

100+ addIBC (IBCFnInfo n fninfo)

101+

96102 return (cty, ty, inacc)

97103 where

98104 patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)

99105 patToImp (Bind n b sc) = Bind n b (patToImp sc)

100106 patToImp t = t

101107

108+ param_pos i ns (Bind n (Pi t) sc)

109+ | n `elem` ns = i : param_pos (i + 1) ns sc

110+ | otherwise = param_pos (i + 1) ns sc

111+ param_pos i ns t = []

102112

103113-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

104114elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

src/Idris/Elab/Utils.hs+54

@@ -1,3 +1,4 @@

1+{-# LANGUAGE PatternGuards #-}

12module Idris.Elab.Utils where

23

34import Idris.AbsSyntax

@@ -149,3 +150,56 @@ psolve tm = return ()

149150pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

150151pvars ist _ = []

151152

153+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

154+ = nub $ getFixedInType i env [] t ++

155+ getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

156+getFixedInType i env (_ : is) (Bind n (Pi t) sc)

157+ = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

158+getFixedInType i env is tm@(App f a)

159+ | (P _ tn _, args) <- unApply tm

160+ = case lookupCtxt tn (idris_datatypes i) of

161+ [t] -> nub $ paramNames args env (param_pos t) ++

162+ getFixedInType i env is f ++

163+ getFixedInType i env is a

164+ [] -> nub $ getFixedInType i env is f ++

165+ getFixedInType i env is a

166+ | otherwise = nub $ getFixedInType i env is f ++

167+ getFixedInType i env is a

168+getFixedInType i _ _ _ = []

169+

170+getFlexInType i env ps (Bind n (Pi t) sc)

171+ = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

172+ getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

173+getFlexInType i env ps tm@(App f a)

174+ | (P _ tn _, args) <- unApply tm

175+ = case lookupCtxt tn (idris_datatypes i) of

176+ [t] -> nub $ paramNames args env [x | x <- [0..length args],

177+ not (x `elem` param_pos t)]

178+ ++ getFlexInType i env ps f ++

179+ getFlexInType i env ps a

180+ [] -> let ppos = case lookupCtxt tn (idris_fninfo i) of

181+ [fi] -> fn_params fi

182+ [] -> [] in

183+ nub $ paramNames args env [x | x <- [0..length args],

184+ not (x `elem` ppos)]

185+ ++ getFlexInType i env ps f ++

186+ getFlexInType i env ps a

187+ | otherwise = nub $ getFlexInType i env ps f ++

188+ getFlexInType i env ps a

189+getFlexInType i _ _ _ = []

190+

191+-- Treat a name as a parameter if it appears in parameter positions in

192+-- types, and never in a non-parameter position in a (non-param) argument type.

193+

194+getParamsInType i env ps t = let fix = getFixedInType i env ps t

195+ flex = getFlexInType i env fix t in

196+ [x | x <- fix, not (x `elem` flex)]

197+

198+paramNames args env [] = []

199+paramNames args env (p : ps)

200+ | length args > p = case args!!p of

201+ P _ n _ -> if n `elem` env

202+ then n : paramNames args env ps

203+ else paramNames args env ps

204+ _ -> paramNames args env ps

205+ | otherwise = paramNames args env ps

src/Idris/IBC.hs+21−4

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

3131import Util.Zlib (decompressEither)

3232

3333ibcVersion :: Word8

34−ibcVersion = 77

34+ibcVersion = 78

3535

3636data IBCFile = IBCFile { ver :: Word8,

3737 sourcefile :: FilePath,

@@ -57,6 +57,7 @@ data IBCFile = IBCFile { ver :: Word8,

5757 ibc_total :: [(Name, Totality)],

5858 ibc_totcheckfail :: [(FC, String)],

5959 ibc_flags :: [(Name, [FnOpt])],

60+ ibc_fninfo :: [(Name, FnInfo)],

6061 ibc_cg :: [(Name, CGInfo)],

6162 ibc_defs :: [(Name, Def)],

6263 ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],

@@ -79,7 +80,7 @@ deriving instance Binary IBCFile

7980!-}

8081

8182initIBC :: IBCFile

82−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

83+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

8384

8485loadIBC :: FilePath -> Idris ()

8586loadIBC fp = do imps <- getImported

@@ -228,6 +229,7 @@ ibc i (IBCCG n) f = case lookupCtxt n (idris_callgraph i) of

228229ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

229230ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

230231ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

232+ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }

231233ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

232234ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

233235ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

@@ -278,6 +280,7 @@ process i fn

278280 pPatdefs (ibc_patdefs i)

279281 pAccess (ibc_access i)

280282 pFlags (ibc_flags i)

283+ pFnInfo (ibc_fninfo i)

281284 pTotal (ibc_total i)

282285 pTotCheckErr (ibc_totcheckfail i)

283286 pCG (ibc_cg i)

@@ -466,6 +469,9 @@ pAccess ds = mapM_ (\ (n, a) ->

466469pFlags :: [(Name, [FnOpt])] -> Idris ()

467470pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

468471

472+pFnInfo :: [(Name, FnInfo)] -> Idris ()

473+pFnInfo ds = mapM_ (\ (n, a) -> setFnInfo n a) ds

474+

469475pTotal :: [(Name, Totality)] -> Idris ()

470476pTotal ds = mapM_ (\ (n, a) ->

471477 do i <- getIState

@@ -837,7 +843,7 @@ instance Binary MetaInformation where

837843 return (DataMI x1)

838844

839845instance Binary IBCFile where

840− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39)

846+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40)

841847 = {-# SCC "putIBCFile" #-}

842848 do put x1

843849 put x2

@@ -878,6 +884,7 @@ instance Binary IBCFile where

878884 put x37

879885 put x38

880886 put x39

887+ put x40

881888

882889 get

883890 = do x1 <- get

@@ -920,7 +927,8 @@ instance Binary IBCFile where

920927 x37 <- get

921928 x38 <- get

922929 x39 <- get

923− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39)

930+ x40 <- get

931+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40)

924932 else return (initIBC { ver = x1 })

925933

926934instance Binary DataOpt where

@@ -953,6 +961,7 @@ instance Binary FnOpt where

953961 ErrorReverse -> putWord8 10

954962 CoveringFn -> putWord8 11

955963 NoImplicit -> putWord8 12

964+ Constructor -> putWord8 13

956965 get

957966 = do i <- getWord8

958967 case i of

@@ -970,6 +979,7 @@ instance Binary FnOpt where

970979 10 -> return ErrorReverse

971980 11 -> return CoveringFn

972981 12 -> return NoImplicit

982+ 13 -> return Constructor

973983 _ -> error "Corrupted binary data for FnOpt"

974984

975985instance Binary Fixity where

@@ -1829,6 +1839,13 @@ instance Binary OptInfo where

18291839 x2 <- get

18301840 return (Optimise x1 x2)

18311841

1842+instance Binary FnInfo where

1843+ put (FnInfo x1)

1844+ = put x1

1845+ get

1846+ = do x1 <- get

1847+ return (FnInfo x1)

1848+

18321849instance Binary TypeInfo where

18331850 put (TI x1 x2 x3 x4 x5) = do put x1

18341851 put x2

src/Idris/REPL.hs+2

@@ -920,8 +920,10 @@ process fn (DebugInfo n)

920920 let cg' = lookupCtxtName n (idris_callgraph i)

921921 sc <- checkSizeChange n

922922 iputStrLn $ "Size change: " ++ show sc

923+ let fn = lookupCtxtName n (idris_fninfo i)

923924 when (not (null cg')) $ do iputStrLn "Call graph:\n"

924925 iputStrLn (show cg')

926+ when (not (null fn)) $ iputStrLn (show fn)

925927process fn (Search t) = searchByType t

926928process fn (CaseSplitAt updatefile l n)

927929 = caseSplitAt fn updatefile l n

test/reg051/expectednew file

No changes to the content.

test/reg051/reg051.idrnew file+99

@@ -0,0 +1,99 @@

1+-- Test for problem with parameter propagation in fromState'

2+

3+data StateTy : Type where

4+ STInt : StateTy

5+ STString : StateTy

6+ STMaybe : StateTy -> StateTy

7+ STList : StateTy -> StateTy

8+

9+interpSTy : StateTy -> Type

10+interpSTy STInt = Int

11+interpSTy STString = String

12+interpSTy (STMaybe a) = Maybe (interpSTy a)

13+interpSTy (STList a) = List (interpSTy a)

14+

15+data State : StateTy -> Type where

16+ MkState : (t : StateTy) -> Ptr -> State t

17+

18+abstract

19+data StateC : StateTy -> Type where

20+ MkStateC : Int -> (t : StateTy) -> Ptr -> StateC t

21+

22+isObj : Ptr -> IO Bool

23+isObj p = do

24+ "object" <- mkForeign (FFun "typeof %0" [FPtr] FString) p

25+ | _ => pure False

26+ pure True

27+

28+stateVarName : String

29+stateVarName = "__IDR__IQUERY__STATE__"

30+

31+stateVarExists : IO Bool

32+stateVarExists = do

33+ o <- mkForeign (FFun ("typeof " ++ stateVarName) [] FString)

34+ pure $ if o == "object" then True else False

35+

36+initStateVar : IO Ptr

37+initStateVar = mkForeign (FFun (stateVarName ++ " = {count: 0}") [] FPtr)

38+

39+getStateVar : IO (Maybe Ptr)

40+getStateVar = case !stateVarExists of

41+ True => map Just $ mkForeign (FFun stateVarName [] FPtr)

42+ False => pure Nothing

43+

44+getStateVar' : IO Ptr

45+getStateVar' = case !getStateVar of

46+ Just s => pure s

47+ Nothing => initStateVar

48+

49+stateCExists : Ptr -> Int -> IO Bool

50+stateCExists c n = do

51+ r <- mkForeign (FFun "typeof %0[%1]" [FPtr,FInt] FString) c n

52+ pure $ if r == "object" then True else False

53+

54+incCount : Ptr -> IO Int

55+incCount c = do

56+ n <- mkForeign (FFun "%0.count" [FPtr] FInt) c

57+ mkForeign (FFun "%0.count++" [FPtr] FUnit) c

58+ pure n

59+

60+infixl 5 =>>

61+public

62+(=>>) : IO (Maybe (State a)) -> (State a -> IO (Maybe b))

63+ -> IO (Maybe b)

64+s =>> f = do

65+ (Just s') <- s

66+ | Nothing => pure Nothing

67+ f s'

68+

69+infixl 5 :=>

70+public

71+(:=>) : IO (Maybe (State a)) -> (State a -> IO ()) -> IO Bool

72+(:=>) s f = do

73+ (Just s') <- s

74+ | Nothing => pure False

75+ f s'

76+ pure True

77+

78+public

79+access : Nat -> State (STList t) -> IO (Maybe (State t))

80+access n (MkState (STList t) p) = do

81+ r <- mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p (fromNat n)

82+ True <- isObj r

83+ | False => pure Nothing

84+ pure $ Just $ MkState t r

85+

86+fromState' : State t -> IO (interpSTy t)

87+fromState' (MkState STInt p) = mkForeign (FFun "%0.val" [FPtr] FInt) p

88+fromState' (MkState STString p) = mkForeign (FFun "%0.val" [FPtr] FString) p

89+fromState' (MkState (STMaybe a) p) = do

90+ isNull <- (mkForeign (FFun "(%0.val == null).toString()" [FPtr] FString) p)

91+ case isNull == "true" of

92+ True => pure Nothing

93+ False => pure $ Just !(fromState' (MkState a p))

94+fromState' (MkState (STList a) p) = do

95+ n <- mkForeign (FFun "%0.val.length" [FPtr] FInt) p

96+ ps <- sequence $ map

97+ (\n => mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p n) [0..(n-1)]

98+ sequence $ map (\p' => fromState' (MkState a p')) ps

99+

test/reg051/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg051.idr --check

3+rm -f *.ibc