ddced5c · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

250 test/reg050/run

251 test/reg050/*.idr

252 test/reg050/expected

253+ test/reg051/run

254+ test/reg051/*.idr

255+ test/reg051/expected

253

256

254 test/basic001/run

257 test/basic001/run

255 test/basic001/*.idr

258 test/basic001/*.idr

src/Idris/AbsSyntax.hs+3

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

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

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

134

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

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

137+

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

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

136setAccessibility n a

139setAccessibility n a

137 = do i <- getIState

140 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+11−1

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

158 idris_calledgraph :: Ctxt [Name],

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

160 idris_tyinfodata :: Ctxt TIData,

161+ idris_fninfo :: Ctxt FnInfo,

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

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

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

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

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

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

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

260 | IBCMetaInformation Name MetaInformation

261 | IBCMetaInformation Name MetaInformation

261 | IBCTotal Name Totality

262 | IBCTotal Name Totality

262 | IBCFlags Name [FnOpt]

263 | IBCFlags Name [FnOpt]

264+ | IBCFnInfo Name FnInfo

263 | IBCTrans (Term, Term)

265 | IBCTrans (Term, Term)

264 | IBCErrRev (Term, Term)

266 | IBCErrRev (Term, Term)

265 | IBCCG Name

267 | IBCCG Name

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

280idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

282idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

281 emptyContext emptyContext emptyContext emptyContext

283 emptyContext emptyContext emptyContext emptyContext

282 emptyContext emptyContext emptyContext emptyContext

284 emptyContext emptyContext emptyContext emptyContext

283− emptyContext emptyContext

285+ emptyContext emptyContext emptyContext

284 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

286 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

285 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

287 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

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

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

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

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

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

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

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

495+ | Constructor -- Data constructor type

493 deriving (Show, Eq)

496 deriving (Show, Eq)

494{-!

497{-!

495deriving instance Binary FnOpt

498deriving instance Binary FnOpt

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

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

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

906 deriving Show

909 deriving Show

907

910

911+-- | Miscellaneous information about functions

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

913+ deriving Show

914+{-!

915+deriving instance Binary FnInfo

916+!-}

917+

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

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

909 detaggable :: Bool }

919 detaggable :: Bool }

910 deriving Show

920 deriving Show

src/Idris/Elab/Clause.hs−49

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

422 | Ref <- y = True

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

424

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−

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

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

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

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

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

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

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

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

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

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

201 = 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)

203 ctxt <- getContext

204 let cty' = normalise ctxt [] cty

205

src/Idris/Elab/Type.hs+10

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

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

94 addIBC (IBCImp n)

95

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+

96 return (cty, ty, inacc)

102 return (cty, ty, inacc)

97 where

103 where

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

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

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

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

100 patToImp t = t

106 patToImp t = t

101

107

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 = []

102

112

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

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

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

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

src/Idris/Elab/Utils.hs+54

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

1+{-# LANGUAGE PatternGuards #-}

1module Idris.Elab.Utils where

2module Idris.Elab.Utils where

2

3

3import Idris.AbsSyntax

4import Idris.AbsSyntax

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

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

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

150pvars ist _ = []

151pvars ist _ = []

151

152

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)

31import Util.Zlib (decompressEither)

32

33ibcVersion :: Word8

34−ibcVersion = 77

34+ibcVersion = 78

35

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

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

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

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

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

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

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

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

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

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

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

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

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

79!-}

80!-}

80

81

81initIBC :: IBCFile

82initIBC :: IBCFile

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

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

83

84

84loadIBC :: FilePath -> Idris ()

85loadIBC :: FilePath -> Idris ()

85loadIBC fp = do imps <- getImported

86loadIBC fp = do imps <- getImported

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

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

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

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

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

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

231ibc 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 }

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

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

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

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

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

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

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

278 pPatdefs (ibc_patdefs i)

280 pPatdefs (ibc_patdefs i)

279 pAccess (ibc_access i)

281 pAccess (ibc_access i)

280 pFlags (ibc_flags i)

282 pFlags (ibc_flags i)

283+ pFnInfo (ibc_fninfo i)

281 pTotal (ibc_total i)

284 pTotal (ibc_total i)

282 pTotCheckErr (ibc_totcheckfail i)

285 pTotCheckErr (ibc_totcheckfail i)

283 pCG (ibc_cg i)

286 pCG (ibc_cg i)

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

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

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

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

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

468

471

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

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

474+

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

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

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

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

471 do i <- getIState

477 do i <- getIState

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

837 return (DataMI x1)

843 return (DataMI x1)

838

844

839instance Binary IBCFile where

845instance 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)

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

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

842 do put x1

848 do put x1

843 put x2

849 put x2

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

878 put x37

884 put x37

879 put x38

885 put x38

880 put x39

886 put x39

887+ put x40

881

888

882 get

889 get

883 = do x1 <- get

890 = do x1 <- get

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

920 x37 <- get

927 x37 <- get

921 x38 <- get

928 x38 <- get

922 x39 <- get

929 x39 <- get

930+ x40 <- 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)

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)

924 else return (initIBC { ver = x1 })

932 else return (initIBC { ver = x1 })

925

933

926instance Binary DataOpt where

934instance Binary DataOpt where

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

953 ErrorReverse -> putWord8 10

961 ErrorReverse -> putWord8 10

954 CoveringFn -> putWord8 11

962 CoveringFn -> putWord8 11

955 NoImplicit -> putWord8 12

963 NoImplicit -> putWord8 12

964+ Constructor -> putWord8 13

956 get

965 get

957 = do i <- getWord8

966 = do i <- getWord8

958 case i of

967 case i of

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

970 10 -> return ErrorReverse

979 10 -> return ErrorReverse

971 11 -> return CoveringFn

980 11 -> return CoveringFn

972 12 -> return NoImplicit

981 12 -> return NoImplicit

982+ 13 -> return Constructor

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

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

974

984

975instance Binary Fixity where

985instance Binary Fixity where

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

1829 x2 <- get

1839 x2 <- get

1830 return (Optimise x1 x2)

1840 return (Optimise x1 x2)

1831

1841

1842+instance Binary FnInfo where

1843+ put (FnInfo x1)

1844+ = put x1

1845+ get

1846+ = do x1 <- get

1847+ return (FnInfo x1)

1848+

1832instance Binary TypeInfo where

1849instance Binary TypeInfo where

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

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

1834 put x2

1851 put x2

src/Idris/REPL.hs+2

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

920 let cg' = lookupCtxtName n (idris_callgraph i)

921 sc <- checkSizeChange n

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

923+ let fn = lookupCtxtName n (idris_fninfo i)

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

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

924 iputStrLn (show cg')

925 iputStrLn (show cg')

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

925process fn (Search t) = searchByType t

927process fn (Search t) = searchByType t

926process fn (CaseSplitAt updatefile l n)

928process fn (CaseSplitAt updatefile l n)

927 = caseSplitAt fn updatefile l n

929 = 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