fc02362 · Idris-dev · git.iko.soy

CHANGELOG+10

@@ -1,5 +1,15 @@

11New in 0.9.18:

22--------------

3+* Strings are now UTF8 encoded in the default back end

4+* Some reorganisation of primitives:

5+ + Buffer and BitVector primitives have been removed (they were not

6+ tested sufficiently, and lack a maintainer)

7+ + Float has been renamed 'Double' (Float is defined in the Prelude for

8+ compatibility)

9+ + Externally defined primitives and operations now supported with

10+ '%extern' directive, allowing back ends to define their own special

11+ purpose primitives

12+ + Ptr and ManagedPtr have been removed and replaced with external primitives

313* Syntax rules no longer perform variable capture. Users of effects will

414 need to explicitly name results in dependent effect signatures instead

515 of using the default name "result".

libs/prelude/Builtins.idr+20

@@ -154,3 +154,23 @@ really_believe_me x = prim__believe_me _ _ x

154154Float : Type

155155Float = Double

156156

157+-- Pointers as external primitive; there's no literals for these, so no

158+-- need for them to be part of the compiler.

159+

160+abstract data Ptr : Type

161+abstract data ManagedPtr : Type

162+

163+%extern prim__readFile : prim__WorldType -> Ptr -> String

164+%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int

165+%extern prim__readString : prim__WorldType -> String

166+%extern prim__writeString : prim__WorldType -> String -> Int

167+

168+%extern prim__vm : Ptr

169+%extern prim__stdin : Ptr

170+%extern prim__stdout : Ptr

171+%extern prim__stderr : Ptr

172+

173+%extern prim__null : Ptr

174+%extern prim__registerPtr : Ptr -> Int -> ManagedPtr

175+

176+

src/IRTS/CodegenC.hs+28−19

@@ -451,16 +451,6 @@ doOp v (LIntStr (ITFixed _)) [x] = v ++ "idris_castBitsStr(vm, " ++ creg x ++ ")

451451doOp v LFloatStr [x] = v ++ "idris_castFloatStr(vm, " ++ creg x ++ ")"

452452doOp v LStrFloat [x] = v ++ "idris_castStrFloat(vm, " ++ creg x ++ ")"

453453

454−doOp v LReadStr [_] = v ++ "idris_readStr(vm, stdin)"

455−doOp v LWriteStr [_,s] = v ++ "MKINT((i_int)(idris_writeStr(stdout"

456− ++ ",GETSTR("

457− ++ creg s ++ "))))"

458−

459−doOp v LReadFile [_,x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

460−doOp v LWriteFile [_,x,s] = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x

461− ++ "),GETSTR("

462− ++ creg s ++ "))))"

463−

464454doOp v (LSLt (ATInt (ITFixed ty))) [x, y] = bitOp v "SLt" ty [x, y]

465455doOp v (LSLe (ATInt (ITFixed ty))) [x, y] = bitOp v "SLte" ty [x, y]

466456doOp v (LEq (ATInt (ITFixed ty))) [x, y] = bitOp v "Eq" ty [x, y]

@@ -552,16 +542,8 @@ doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y

552542doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

553543doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

554544

555−doOp v LStdIn [] = v ++ "MKPTR(vm, stdin)"

556−doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)"

557−doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

558−

559545doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

560546doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

561−doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

562−doOp v LNullPtr [] = v ++ "MKPTR(vm, NULL)"

563−doOp v LRegisterPtr [p, i] = v ++ "MKMPTR(vm, GETPTR(" ++ creg p ++

564− "), GETINT(" ++ creg i ++ "))"

565547doOp v (LChInt ITNative) args = v ++ creg (last args)

566548doOp v (LChInt ITChar) args = doOp v (LChInt ITNative) args

567549doOp v (LIntCh ITNative) args = v ++ creg (last args)

@@ -569,7 +551,34 @@ doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

569551

570552doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

571553doOp v LNoOp args = v ++ creg (last args)

572−doOp _ op args = error "doOp of (" ++ show op ++ ") not implemented, arguments (" ++ show args ++ ")"

554+

555+-- Pointer primitives (declared as %extern in Builtins.idr)

556+doOp v (LExternal rs) [_]

557+ | rs == sUN "prim__readString" = v ++ "idris_readStr(vm, stdin)"

558+doOp v (LExternal ws) [_,s]

559+ | ws == sUN "prim__writeString"

560+ = v ++ "MKINT((i_int)(idris_writeStr(stdout"

561+ ++ ",GETSTR("

562+ ++ creg s ++ "))))"

563+

564+doOp v (LExternal rf) [_,x]

565+ | rf == sUN "prim__readFile"

566+ = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

567+doOp v (LExternal wf) [_,x,s]

568+ | wf == sUN "prim__writeFile"

569+ = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x

570+ ++ "),GETSTR("

571+ ++ creg s ++ "))))"

572+doOp v (LExternal vm) [] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

573+doOp v (LExternal si) [] | si == sUN "prim__stdin" = v ++ "MKPTR(vm, stdin)"

574+doOp v (LExternal so) [] | so == sUN "prim__stdout" = v ++ "MKPTR(vm, stdout)"

575+doOp v (LExternal se) [] | se == sUN "prim__stderr" = v ++ "MKPTR(vm, stderr)"

576+

577+doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"

578+doOp v (LExternal rp) [p, i] | rp == sUN "prim__registerPtr"

579+ = v ++ "MKMPTR(vm, GETPTR(" ++ creg p ++ "), GETINT(" ++ creg i ++ "))"

580+

581+doOp _ op args = error $ "doOp not implemented (" ++ show (op, args) ++ ")"

573582

574583flUnOp :: String -> String -> String

575584flUnOp name val = "MKFLOAT(vm, " ++ name ++ "(GETFLOAT(" ++ val ++ ")))"

src/IRTS/CodegenJavaScript.hs+4−2

@@ -680,7 +680,8 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

680680 jsOP'

681681 | LNoOp <- op = translateReg (last args)

682682

683− | LWriteStr <- op,

683+ | (LExternal ws) <- op,

684+ ws == sUN "prim__writeString",

684685 (_:str:_) <- args = JSAssign (translateReg reg)

685686 (JSApp (JSIdent "i$putStr") [translateReg str])

686687

@@ -1269,7 +1270,8 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

12691270

12701271 | LSystemInfo <- op

12711272 , (arg:_) <- args = jsCall "i$systemInfo" [translateReg arg]

1272− | LNullPtr <- op

1273+ | LExternal nul <- op

1274+ , nul == sUN "prim__null"

12731275 , (_) <- args = JSNull

12741276 | otherwise = JSError $ "Not implemented: " ++ show op

12751277 where

src/IRTS/Compiler.hs+14−3

@@ -185,7 +185,7 @@ isCon _ = False

185185build :: (Name, Def) -> Idris (Name, LDecl)

186186build (n, d)

187187 = do i <- getIState

188− case lookup n (idris_scprims i) of

188+ case getPrim n i of

189189 Just (ar, op) ->

190190 let args = map (\x -> sMN x "op") [0..] in

191191 return (n, (LFun [] n (take ar args)

@@ -193,6 +193,12 @@ build (n, d)

193193 _ -> do def <- mkLDecl n d

194194 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def

195195 return (n, def)

196+ where getPrim n i

197+ | Just (ar, op) <- lookup n (idris_scprims i)

198+ = Just (ar, op)

199+ | Just ar <- lookup n (S.toList (idris_externs i))

200+ = Just (ar, LExternal n)

201+ getPrim n i = Nothing

196202

197203declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x

198204declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

@@ -225,7 +231,9 @@ data VarInfo = VI

225231type Vars = M.Map Name VarInfo

226232

227233irTerm :: Vars -> [Name] -> Term -> Idris LExp

228−irTerm vs env tm@(App f a) = case unApply tm of

234+irTerm vs env tm@(App f a) = do

235+ ist <- getIState

236+ case unApply tm of

229237 (P _ (UN m) _, args)

230238 | m == txt "mkForeignPrim"

231239 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits

@@ -359,9 +367,12 @@ irTerm vs env tm@(App f a) = case unApply tm of

359367 -- type constructor

360368 (P (TCon t a) n _, args) -> return LNothing

361369

370+ -- an external name applied to arguments

371+ (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do

372+ LOp (LExternal n) <$> mapM (irTerm vs env) args

373+

362374 -- a name applied to arguments

363375 (P _ n _, args) -> do

364− ist <- getIState

365376 case lookup n (idris_scprims ist) of

366377 -- if it's a primitive that is already saturated,

367378 -- compile to the corresponding op here already to save work

src/IRTS/Lang.hs+1−5

@@ -69,14 +69,12 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

6969 | LStrConcat | LStrLt | LStrEq | LStrLen

7070 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

7171 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

72− | LReadStr | LWriteStr | LReadFile | LWriteFile

7372 | LBitCast ArithTy ArithTy -- Only for values of equal width

7473

7675 | LFSqrt | LFFloor | LFCeil | LFNegate

7776

79− | LStdIn | LStdOut | LStdErr

8078

8179 -- system info

8280 | LSystemInfo

@@ -84,9 +82,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

8482 | LFork

8583 | LPar -- evaluate argument anywhere, possibly on another

8684 -- core or another machine. 'id' is a valid implementation

87− | LVMPtr

88− | LNullPtr

89− | LRegisterPtr

85+ | LExternal Name

9086 | LNoOp

9187 deriving (Show, Eq)

9288

src/Idris/AbsSyntax.hs+3−3

@@ -1013,13 +1013,13 @@ expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)

10131013 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

10141014 else --trace (show (n, expandParams dec ps ns ty)) $

10151015 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)

1016−expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

1016+expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc o n ty)

10171017 = if n `elem` ns && (not rhsonly)

10181018 then -- trace (show (n, expandParams dec ps ns ty)) $

1019− PPostulate doc syn fc o (dec n) (piBind ps

1019+ PPostulate e doc syn fc o (dec n) (piBind ps

10201020 (expandParams dec ps ns [] ty))

10211021 else --trace (show (n, expandParams dec ps ns ty)) $

1022− PPostulate doc syn fc o n (expandParams dec ps ns [] ty)

1022+ PPostulate e doc syn fc o n (expandParams dec ps ns [] ty)

10231023expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

10241024 = let n' = if n `elem` ns then dec n else n in

10251025 PClauses fc opts n' (map expandParamsC cs)

src/Idris/AbsSyntaxTree.hs+8−5

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

226226 module_aliases :: M.Map [T.Text] [T.Text],

227227 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?

228228 idris_postulates :: S.Set Name,

229+ idris_externs :: S.Set (Name, Int),

229230 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used

230231 idris_whocalls :: Maybe (M.Map Name [Name]),

231232 idris_callswho :: Maybe (M.Map Name [Name]),

@@ -300,6 +301,7 @@ data IBCWrite = IBCFix FixDecl

300301 | IBCErrorHandler Name

301302 | IBCFunctionErrorHandler Name Name Name

302303 | IBCPostulate Name

304+ | IBCExtern (Name, Int)

303305 | IBCTotCheckErr FC String

304306 | IBCParsedRegion FC

305307 | IBCModDocs Name -- ^ The name is the special name used to track module docs

@@ -317,7 +319,7 @@ idrisInit = IState initContext S.empty []

317319 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

318320 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

320− AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty []

322+ AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty []

321323

322324-- | The monad for the main REPL - reading and processing files and updating

323325-- global state (hence the IO inner monad).

@@ -594,7 +596,8 @@ type ProvideWhat = ProvideWhat' PTerm

594596data PDecl' t

595597 = PFix FC Fixity [String] -- ^ Fixity declaration

596598 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

597− | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

599+ | PPostulate Bool -- external def if true

600+ (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

598601 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

599602 | PCAF FC Name t -- ^ Top level constant

600603 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

@@ -694,7 +697,7 @@ type PClause = PClause' PTerm

694697declared :: PDecl -> [Name]

695698declared (PFix _ _ _) = []

696699declared (PTy _ _ _ _ _ n t) = [n]

697−declared (PPostulate _ _ _ _ n t) = [n]

700+declared (PPostulate _ _ _ _ _ n t) = [n]

698701declared (PClauses _ _ n _) = [] -- not a declaration

699702declared (PCAF _ n _) = [n]

700703declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

@@ -714,7 +717,7 @@ declared (PDirective _) = []

714717tldeclared :: PDecl -> [Name]

715718tldeclared (PFix _ _ _) = []

716719tldeclared (PTy _ _ _ _ _ n t) = [n]

717−tldeclared (PPostulate _ _ _ _ n t) = [n]

720+tldeclared (PPostulate _ _ _ _ _ n t) = [n]

718721tldeclared (PClauses _ _ n _) = [] -- not a declaration

719722tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]

720723tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

@@ -729,7 +732,7 @@ tldeclared _ = []

729732defined :: PDecl -> [Name]

730733defined (PFix _ _ _) = []

731734defined (PTy _ _ _ _ _ n t) = []

732−defined (PPostulate _ _ _ _ n t) = []

735+defined (PPostulate _ _ _ _ _ n t) = []

733736defined (PClauses _ _ n _) = [n] -- not a declaration

734737defined (PCAF _ n _) = [n]

735738defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

src/Idris/Core/Execute.hs+39−30

@@ -251,6 +251,9 @@ execApp env ctxt c@(EP (TCon _ arity) n _) args =

251251 let restArgs = drop arity args

252252 execApp env ctxt (mkEApp c args') restArgs

253253

254+execApp env ctxt f@(EP _ n _) args

255+ | Just (res, rest) <- getOp n args = do r <- res

256+ execApp env ctxt r rest

254257execApp env ctxt f@(EP _ n _) args =

255258 do let val = lookupDef n ctxt

256259 case val of

@@ -260,9 +263,9 @@ execApp env ctxt f@(EP _ n _) args =

260263 if length args >= arity

261264 then let args' = take arity args in

262265 case getOp n args' of

263− Just res -> do r <- res

264− execApp env ctxt r (drop arity args)

265− Nothing -> return (mkEApp f args)

266+ Just (res, []) -> do r <- res

267+ execApp env ctxt r (drop arity args)

268+ _ -> return (mkEApp f args)

266269 else return (mkEApp f args)

267270 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

268271 do rhs <- doExec env ctxt tm

@@ -418,41 +421,47 @@ upio = sUN "unsafePerformPrimIO"

418421delay = sUN "Delay"

419422force = sUN "Force"

420423

421−-- | Look up primitive operations in the global table and transform them into ExecVal functions

422−getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

423−getOp fn [_, _, x] | fn == pbm = Just (return x)

424−getOp fn [_, EConstant (Str n)]

424+-- | Look up primitive operations in the global table and transform

425+-- them into ExecVal functions

426+getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])

427+getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)

428+getOp fn (_ : EConstant (Str n) : xs)

425429 | fn == pws =

426− Just $ do execIO $ putStr n

427− return (EConstant (I 0))

428−getOp fn [_]

430+ Just (do execIO $ putStr n

431+ return (EConstant (I 0)), xs)

432+getOp fn (_:xs)

429433 | fn == prs =

430− Just $ do line <- execIO getLine

431− return (EConstant (Str line))

432−getOp fn [_, EP _ fn' _, EConstant (Str n)]

434+ Just (do line <- execIO getLine

435+ return (EConstant (Str line)), xs)

436+getOp fn (_ : EP _ fn' _ : EConstant (Str n) : xs)

433437 | fn == pwf && fn' == pstdout =

434− Just $ do execIO $ putStr n

435− return (EConstant (I 0))

436−getOp fn [_, EP _ fn' _]

438+ Just (do execIO $ putStr n

439+ return (EConstant (I 0)), xs)

440+getOp fn (_ : EP _ fn' _ : xs)

437441 | fn == prf && fn' == pstdin =

438− Just $ do line <- execIO getLine

439− return (EConstant (Str line))

440−getOp fn [_, EHandle h, EConstant (Str n)]

442+ Just (do line <- execIO getLine

443+ return (EConstant (Str line)), xs)

444+getOp fn (_ : EHandle h : EConstant (Str n) : xs)

441445 | fn == pwf =

442− Just $ do execIO $ hPutStr h n

443− return (EConstant (I 0))

444−getOp fn [_, EHandle h]

446+ Just (do execIO $ hPutStr h n

447+ return (EConstant (I 0)), xs)

448+getOp fn (_ : EHandle h : xs)

445449 | fn == prf =

446− Just $ do contents <- execIO $ hGetLine h

447− return (EConstant (Str (contents ++ "\n")))

448−getOp fn [_, arg]

450+ Just (do contents <- execIO $ hGetLine h

451+ return (EConstant (Str (contents ++ "\n"))), xs)

452+getOp fn (_ : arg : xs)

449453 | fn == prf =

450− Just $ execFail (Msg "Can't use prim__readFile on a raw pointer in the executor.")

451−getOp n args = getPrim n primitives >>= flip applyPrim args

452− where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)

454+ Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)

455+getOp n args = do (arity, prim) <- getPrim n primitives

456+ if (length args >= arity)

457+ then do res <- applyPrim prim (take arity args)

458+ Just (res, drop arity args)

459+ else Nothing

460+ where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)

453461 getPrim n [] = Nothing

454− getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def

455− | otherwise = getPrim n prims

462+ getPrim n ((Prim pn _ arity def _ _) : prims)

463+ | n == pn = Just (arity, execPrim def)

464+ | otherwise = getPrim n prims

456465

457466 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal

458467 execPrim f args = EConstant <$> (mapM getConst args >>= f)

src/Idris/DeepSeq.hs+2−2

@@ -132,9 +132,9 @@ instance (NFData t) => NFData (PDecl' t) where

132132 = rnf x1 `seq`

133133 rnf x2 `seq`

134134 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

135− rnf (PPostulate x1 x2 x3 x4 x5 x6)

135+ rnf (PPostulate x1 x2 x3 x4 x5 x6 x7)

136136 = rnf x1 `seq`

137− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

137+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

138138 rnf (PClauses x1 x2 x3 x4)

139139 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

140140 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

src/Idris/Elab/Type.hs+16−1

@@ -1,5 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Elab.Type (buildType, elabType, elabType', elabPostulate) where

2+module Idris.Elab.Type (buildType, elabType, elabType',

3+ elabPostulate, elabExtern) where

34

45import Idris.AbsSyntax

56import Idris.ASTUtils

@@ -229,5 +230,19 @@ elabPostulate info syn doc fc opts n ty = do

229230 -- remove it from the deferred definitions list

230231 solveDeferred n

231232

233+elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

234+ FC -> FnOpts -> Name -> PTerm -> Idris ()

235+elabExtern info syn doc fc opts n ty = do

236+ cty <- elabType info syn doc [] fc opts n ty

237+ ist <- getIState

238+ let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))

239+

240+ putIState . (\ist -> ist{ idris_externs = S.insert (n, arity) (idris_externs ist) }) =<< getIState

241+ updateContext (addOperator n cty arity (\x -> Nothing))

242+ addIBC (IBCExtern (n, arity))

243+

244+ -- remove it from the deferred definitions list

245+ solveDeferred n

246+

232247

233248

src/Idris/ElabDecls.hs+4−2

@@ -160,10 +160,12 @@ elabDecl' what info (PTy doc argdocs s f o n ty)

160160 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

161161 elabType info s doc argdocs f o n ty

162162 return ()

163−elabDecl' what info (PPostulate doc s f o n ty)

163+elabDecl' what info (PPostulate b doc s f o n ty)

164164 | what /= EDefns

165165 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

166− elabPostulate info s doc f o n ty

166+ if b

167+ then elabExtern info s doc f o n ty

168+ else elabPostulate info s doc f o n ty

167169elabDecl' what info (PData doc argDocs s f co d)

168170 | what /= ETypes

169171 = do iLOG $ "Elaborating " ++ show (d_name d)

src/Idris/Erasure.hs+9−4

@@ -77,9 +77,10 @@ performUsageAnalysis roots = do

7777 cg <- idris_callgraph <$> getIState

7878 opt <- idris_optimisation <$> getIState

7979 used <- idris_erasureUsed <$> getIState

80+ externs <- idris_externs <$> getIState

8081

8182 -- Build the dependency graph.

82− let depMap = buildDepMap ci used ctx main

83+ let depMap = buildDepMap ci used (S.toList externs) ctx main

8384

8485 -- Search for reachable nodes in the graph.

8586 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap

@@ -174,9 +175,10 @@ forwardChain deps

174175

175176-- Build the dependency graph,

176177-- starting the depth-first search from a list of Names.

177−buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> [Name] -> Deps

178−buildDepMap ci used ctx startNames = addPostulates used $

179− dfs S.empty M.empty startNames

178+buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->

179+ Context -> [Name] -> Deps

180+buildDepMap ci used externs ctx startNames

181+ = addPostulates used $ dfs S.empty M.empty startNames

180182 where

181183 -- mark the result of Main.main as used with the empty assumption

182184 addPostulates :: [(Name, Int)] -> Deps -> Deps

@@ -226,6 +228,9 @@ buildDepMap ci used ctx startNames = addPostulates used $

226228 -- in general, all other primitives use all their arguments

227229 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]

228230

231+ -- %externs are assumed to use all their arguments

232+ , [(n, Arg i) | (n,arity) <- externs, i <- [0..arity-1]]

233+

229234 -- mkForeign* functions are special-cased below

230235 ]

231236 ]

src/Idris/IBC.hs+18−6

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

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 101

40+ibcVersion = 102

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

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

7979 ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],

8080 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

8181 ibc_postulates :: ![Name],

82+ ibc_externs :: ![(Name, Int)],

8283 ibc_parsedSpan :: !(Maybe FC),

8384 ibc_usage :: ![(Name, Int)],

8485 ibc_exports :: ![Name]

@@ -89,7 +90,7 @@ deriving instance Binary IBCFile

8990!-}

9091

9192initIBC :: IBCFile

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

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

9394

9495loadIBC :: Bool -- ^ True = reexport, False = make everything private

9596 -> FilePath -> Idris ()

@@ -228,6 +229,7 @@ ibc i (IBCMetavar n) f =

228229 Nothing -> return f

229230 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

230231ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

232+ibc i (IBCExtern n) f = return f { ibc_externs = n : ibc_externs f }

231233ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

232234ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }

233235ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

@@ -290,6 +292,7 @@ process reexp i fn

290292 pFunctionErrorHandlers $ force (ibc_function_errorhandlers i)

291293 pMetavars $ force (ibc_metavars i)

292294 pPostulates $ force (ibc_postulates i)

295+ pExterns $ force (ibc_externs i)

293296 pParsedSpan $ force (ibc_parsedSpan i)

294297 pUsage $ force (ibc_usage i)

295298 pExports $ force (ibc_exports i)

@@ -306,6 +309,11 @@ pPostulates ns = do

306309 i <- getIState

307310 putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

308311

312+pExterns :: [(Name, Int)] -> Idris ()

313+pExterns ns = do

314+ i <- getIState

315+ putIState i{ idris_externs = idris_externs i `S.union` S.fromList ns }

316+

309317pParsedSpan :: Maybe FC -> Idris ()

310318pParsedSpan fc = do ist <- getIState

311319 putIState ist { idris_parsedSpan = fc }

@@ -934,7 +942,7 @@ instance Binary MetaInformation where

934942 _ -> error "Corrupted binary data for MetaInformation"

935943

936944instance Binary IBCFile where

937− 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 x41 x42 x43)

945+ 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 x41 x42 x43 x44)

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

939947 do put x1

940948 put x2

@@ -979,6 +987,7 @@ instance Binary IBCFile where

979987 put x41

980988 put x42

981989 put x43

990+ put x44

982991

983992 get

984993 = do x1 <- get

@@ -1025,7 +1034,8 @@ instance Binary IBCFile where

10251034 x41 <- get

10261035 x42 <- get

10271036 x43 <- get

1028− 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 x41 x42 x43)

1037+ x44 <- get

1038+ 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 x41 x42 x43 x44)

10291039 else return (initIBC { ver = x1 })

10301040

10311041instance Binary DataOpt where

@@ -1271,7 +1281,7 @@ instance (Binary t) => Binary (PDecl' t) where

12711281 PMutual x1 x2 -> do putWord8 11

12721282 put x1

12731283 put x2

1274− PPostulate x1 x2 x3 x4 x5 x6

1284+ PPostulate x1 x2 x3 x4 x5 x6 x7

12751285 -> do putWord8 12

12761286 put x1

12771287 put x2

@@ -1279,6 +1289,7 @@ instance (Binary t) => Binary (PDecl' t) where

12791289 put x4

12801290 put x5

12811291 put x6

1292+ put x7

12821293 PSyntax x1 x2 -> do putWord8 13

12831294 put x1

12841295 put x2

@@ -1376,7 +1387,8 @@ instance (Binary t) => Binary (PDecl' t) where

13761387 x4 <- get

13771388 x5 <- get

13781389 x6 <- get

1379− return (PPostulate x1 x2 x3 x4 x5 x6)

1390+ x7 <- get

1391+ return (PPostulate x1 x2 x3 x4 x5 x6 x7)

13801392 13 -> do x1 <- get

13811393 x2 <- get

13821394 return (PSyntax x1 x2)

src/Idris/ParseExpr.hs+2−7

@@ -1158,19 +1158,14 @@ constants =

11581158 , ("Char", AType (ATInt ITChar))

11591159 , ("Double", AType ATFloat)

11601160 , ("String", StrType)

1161− , ("Ptr", PtrType)

1162− , ("ManagedPtr", ManagedPtrType)

1161+-- , ("Ptr", PtrType)

1162+-- , ("ManagedPtr", ManagedPtrType)

11631163 , ("prim__WorldType", WorldType)

11641164 , ("prim__TheWorld", TheWorld)

1165−-- , ("prim__UnsafeBuffer", BufferType)

11661165 , ("Bits8", AType (ATInt (ITFixed IT8)))

11671166 , ("Bits16", AType (ATInt (ITFixed IT16)))

11681167 , ("Bits32", AType (ATInt (ITFixed IT32)))

11691168 , ("Bits64", AType (ATInt (ITFixed IT64)))

1170−-- , ("Bits8x16", AType (ATInt (ITVec IT8 16)))

1171−-- , ("Bits16x8", AType (ATInt (ITVec IT16 8)))

1172−-- , ("Bits32x4", AType (ATInt (ITVec IT32 4)))

1173−-- , ("Bits64x2", AType (ATInt (ITVec IT64 2)))

11741169 ]

11751170

11761171constant :: IdrisParser Idris.Core.TT.Const

src/Idris/Parser.hs+7−5

@@ -500,10 +500,11 @@ Postulate ::=

500500@

501501-}

502502postulate :: SyntaxInfo -> IdrisParser PDecl

503−postulate syn = do doc <- try $ do (doc, _) <- docstring syn

503+postulate syn = do (doc, ext)

504+ <- try $ do (doc, _) <- docstring syn

504505 pushIndent

505− reserved "postulate"

506− return doc

506+ ext <- ppostDecl

507+ return (doc, ext)

507508 ist <- get

508509 let initOpts = if default_total ist

509510 then [TotalFn]

@@ -518,9 +519,10 @@ postulate syn = do doc <- try $ do (doc, _) <- docstring syn

518519 fc <- getFC

519520 terminator

520521 addAcc n acc

521− return (PPostulate doc syn fc opts' n ty)

522+ return (PPostulate ext doc syn fc opts' n ty)

522523 <?> "postulate"

523−

524+ where ppostDecl = do reserved "postulate"; return False

525+ <|> do lchar '%'; reserved "extern"; return True

524526{- | Parses a using declaration

525527

526528@

src/Idris/Primitives.hs+23−23

@@ -167,29 +167,29 @@ primitives =

167167 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

168168 (1, LStrRev) total,

169169

170− Prim (sUN "prim__readFile") (ty [WorldType,PtrType] StrType) 2 (p_cantreduce)

171− (2, LReadFile) total, -- total is okay, because we have 'WorldType'

172− Prim (sUN "prim__writeFile") (ty [WorldType,PtrType,StrType] (AType (ATInt ITNative))) 3 (p_cantreduce)

173− (3, LWriteFile) total,

174− Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

175− (1, LReadStr) total, -- total is okay, because we have 'WorldType'

176− Prim (sUN "prim__writeString") (ty [WorldType,StrType] (AType (ATInt ITNative))) 2 (p_cantreduce)

177− (2, LWriteStr) total,

178−

179− Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

180− (0, LVMPtr) total,

181− -- Streams

182− Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

183− (0, LStdIn) total,

184− Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

185− (0, LStdOut) total,

186− Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

187− (0, LStdErr) total,

188− Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

189− (0, LNullPtr) total,

190− -- Managed pointer registration

191− Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)

192− (2, LRegisterPtr) total,

170+-- Prim (sUN "prim__readFile") (ty [WorldType,PtrType] StrType) 2 (p_cantreduce)

171+-- (2, LReadFile) total, -- total is okay, because we have 'WorldType'

172+-- Prim (sUN "prim__writeFile") (ty [WorldType,PtrType,StrType] (AType (ATInt ITNative))) 3 (p_cantreduce)

173+-- (3, LWriteFile) total,

174+-- Prim (sUN "prim__readString") (ty [WorldType] StrType) 1 (p_cantreduce)

175+-- (1, LReadStr) total, -- total is okay, because we have 'WorldType'

176+-- Prim (sUN "prim__writeString") (ty [WorldType,StrType] (AType (ATInt ITNative))) 2 (p_cantreduce)

177+-- (2, LWriteStr) total,

178+--

179+-- Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

180+-- (0, LVMPtr) total,

181+-- -- Streams

182+-- Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

183+-- (0, LStdIn) total,

184+-- Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

185+-- (0, LStdOut) total,

186+-- Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

187+-- (0, LStdErr) total,

188+-- Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

189+-- (0, LNullPtr) total,

190+-- -- Managed pointer registration

191+-- Prim (sUN "prim__registerPtr") (ty [PtrType, AType (ATInt ITNative)] ManagedPtrType) 2 (p_cantreduce)

192+-- (2, LRegisterPtr) total,

193193 Prim (sUN "prim__systemInfo") (ty [AType (ATInt ITNative)] StrType) 1 (p_cantreduce)

194194 (1, LSystemInfo) total

195195 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]