39e4eb0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

IO primitives tweak to support JS

...and probably other things, since not everything will have stdin/stdout. There are now IO primitives for JS, so basic JS back end stuff will work, but there's still no support for the new style FFI.

commit39e4eb081784f46a1c84a138c0f921281bea778d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 19 Jan 2015, 22:31 (12 years ago) parent2170b9a

12 files changed+94−33

compare with master

unifiedsplit

libs/base/Debug/Trace.idr+1−1 libs/prelude/IO.idr+9−2 libs/prelude/Prelude.idr+2−2 src/IRTS/CodegenC.hs+8−3 src/IRTS/CodegenJavaScript.hs+4−8 src/IRTS/Lang.hs+1−1 src/Idris/Core/Elaborate.hs+15−3 src/Idris/Core/Execute.hs+14−4 src/Idris/Core/ProofState.hs+22−1 src/Idris/ElabTerm.hs+7−3 src/Idris/Primitives.hs+10−4 src/Idris/ProofSearch.hs+1−1

libs/base/Debug/Trace.idr+1−1

@@ -4,6 +4,6 @@ module Debug.Trace

44||| @ msg what to print

55||| @ result the final result

66trace : (msg : String) -> (result : a) -> a

7−trace x val = unsafePerformIO (do putStrLn x; return val)

7+trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; return val)

libs/prelude/IO.idr+9−2

@@ -96,12 +96,19 @@ unsafePerformIO : IO' ffi a -> a

9696unsafePerformIO (MkIO f) = unsafePerformPrimIO

9797 (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))

9898

99+prim_read : IO' l String

100+prim_read = MkIO (\w => prim_io_return (prim__readString (world w)))

101+

102+prim_write : String -> IO' l Int

103+prim_write s

104+ = MkIO (\w => prim_io_return (prim__writeString (world w) s))

105+

99106prim_fread : Ptr -> IO' l String

100−prim_fread h = MkIO (\w => prim_io_return (prim__readString (world w) h))

107+prim_fread h = MkIO (\w => prim_io_return (prim__readFile (world w) h))

101108

102109prim_fwrite : Ptr -> String -> IO' l Int

103110prim_fwrite h s

104− = MkIO (\w => prim_io_return (prim__writeString (world w) h s))

111+ = MkIO (\w => prim_io_return (prim__writeFile (world w) h s))

105112

106113--------- The C FFI

107114

libs/prelude/Prelude.idr+2−2

@@ -435,7 +435,7 @@ uniformB64x2 x = prim__mkB64x2 x x

435435

436436||| Output a string to stdout without a trailing newline

437437putStr : String -> IO' l ()

438−putStr x = do prim_fwrite prim__stdout x

438+putStr x = do prim_write x

439439 return ()

440440

441441||| Output a string to stdout with a trailing newline

@@ -450,7 +450,7 @@ print x = putStrLn (show x)

450450||| Read one line of input from stdin

451451partial

452452getLine : IO' l String

453−getLine = prim_fread prim__stdin

453+getLine = prim_read

454454

455455||| Write a single character to stdout

456456partial

src/IRTS/CodegenC.hs+8−3

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

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

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

433433

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

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

436− ++ "),GETSTR("

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

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

436+ ++ ",GETSTR("

437437 ++ creg s ++ "))))"

438438

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

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

441+ ++ "),GETSTR("

442+ ++ creg s ++ "))))"

443+

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

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

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

src/IRTS/CodegenJavaScript.hs+4−8

@@ -541,14 +541,6 @@ jsTAILCALL _ n =

541541

542542jsFOREIGN :: CompileInfo -> Reg -> String -> [(FType, Reg)] -> JS

543543jsFOREIGN _ reg n args

544− | n == "putStr"

545− , [(FString, arg)] <- args =

546− JSAssign (

547− translateReg reg

548− ) (

549− JSApp (JSIdent "i$putStr") [translateReg arg]

550− )

551−

552544 | n == "isNull"

553545 , [(FPtr, arg)] <- args =

554546 JSAssign (

@@ -687,6 +679,10 @@ jsOP _ reg op args = JSAssign (translateReg reg) jsOP'

687679 jsOP'

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

689681

682+ | LWriteStr <- op,

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

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

685+

690686 | (LZExt (ITFixed IT8) ITNative) <- op = jsUnPackBits $ translateReg (last args)

691687 | (LZExt (ITFixed IT16) ITNative) <- op = jsUnPackBits $ translateReg (last args)

692688 | (LZExt (ITFixed IT32) ITNative) <- op = jsUnPackBits $ translateReg (last args)

src/IRTS/Lang.hs+1−1

@@ -55,7 +55,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

5555 | LStrConcat | LStrLt | LStrEq | LStrLen

5656 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

5757 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

58− | LReadStr | LWriteStr

58+ | LReadStr | LWriteStr | LReadFile | LWriteFile

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

6060

src/Idris/Core/Elaborate.hs+15−3

@@ -314,6 +314,12 @@ attack = processTactic' Attack

314314claim :: Name -> Raw -> Elab' aux ()

315315claim n t = processTactic' (Claim n t)

316316

317+claimFn :: Name -> Name -> Raw -> Elab' aux ()

318+claimFn n bn t = processTactic' (ClaimFn n bn t)

319+

320+unifyGoal :: Raw -> Elab' aux ()

321+unifyGoal t = processTactic' (UnifyGoal t)

322+

317323exact :: Raw -> Elab' aux ()

318324exact t = processTactic' (Exact t)

319325

@@ -667,8 +673,8 @@ checkPiGoal n

667673 solve

668674 focus f

669675

670−simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

671−simple_app fun arg appstr =

676+simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

677+simple_app infer fun arg app0str =

672678 do a <- getNameFrom (sMN 0 "argTy")

673679 b <- getNameFrom (sMN 0 "retTy")

674680 f <- getNameFrom (sMN 0 "f")

@@ -678,18 +684,24 @@ simple_app fun arg appstr =

678684 claim f (RBind (sMN 0 "aX") (Pi Nothing (Var a) RType) (Var b))

679685 tm <- get_term

680686 start_unify s

687+ -- if 'infer' is set, we're assuming it's a simply typed application

688+ -- so safe to unify with the goal type (as there'll be no dependencies)

689+ when infer $ unifyGoal (Var b)

690+ hs <- get_holes

681691 claim s (Var a)

682692 prep_fill f [s]

683693 focus f; fun

684694 focus s; arg

685695 tm <- get_term

686696 ps <- get_probs

687− complete_fill

697+ ty <- goal

688698 hs <- get_holes

699+ complete_fill

689700 env <- get_env

690701 -- We don't need a and b in the hole queue any more since they were

691702 -- just for checking f, so move them to the end. If they never end up

692703 -- getting solved, we'll get an 'Incomplete term' error.

704+ hs <- get_holes

693705 when (a `elem` hs) $ do movelast a

694706 when (b `elem` hs) $ do movelast b

695707 end_unify

src/Idris/Core/Execute.hs+14−4

@@ -402,6 +402,8 @@ toFDesc _ = FUnknown

402402deNS (NS n _) = n

403403deNS n = n

404404

405+prf = sUN "prim__readFile"

406+pwf = sUN "prim__writeFile"

405407prs = sUN "prim__readString"

406408pws = sUN "prim__writeString"

407409pbm = sUN "prim__believe_me"

@@ -417,20 +419,28 @@ force = sUN "Force"

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

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

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

422+getOp fn [_, EConstant (Str n)]

423+ | fn == pws =

424+ Just $ do execIO $ putStr n

425+ return (EConstant (I 0))

426+getOp fn [_]

427+ | fn == prs =

428+ Just $ do line <- execIO getLine

429+ return (EConstant (Str line))

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

421− | fn == pws && fn' == pstdout =

431+ | fn == pwf && fn' == pstdout =

422432 Just $ do execIO $ putStr n

423433 return (EConstant (I 0))

424434getOp fn [_, EP _ fn' _]

425− | fn == prs && fn' == pstdin =

435+ | fn == prf && fn' == pstdin =

426436 Just $ do line <- execIO getLine

427437 return (EConstant (Str line))

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

429− | fn == prs =

439+ | fn == pwf =

430440 Just $ do execIO $ hPutStr h n

431441 return (EConstant (I 0))

432442getOp fn [_, EHandle h]

433− | fn == prs =

443+ | fn == prf =

434444 Just $ do contents <- execIO $ hGetLine h

435445 return (EConstant (Str (contents ++ "\n")))

436446getOp n args = getPrim n primitives >>= flip applyPrim args

src/Idris/Core/ProofState.hs+22−1

@@ -50,6 +50,7 @@ data ProofState = PS { thname :: Name,

5050

5151data Tactic = Attack

5252 | Claim Name Raw

53+ | ClaimFn Name Name Raw

5354 | Reorder Name

5455 | Exact Raw

5556 | Fill Raw

@@ -87,6 +88,7 @@ data Tactic = Attack

8788 | MoveLast Name

8889 | MatchProblems Bool

8990 | UnifyProblems

91+ | UnifyGoal Raw

9092 | ProofState

9193 | Undo

9294 | QED

@@ -340,7 +342,18 @@ claim n ty ctxt env t =

340342 lift $ isType ctxt env tyt

341343 action (\ps -> let (g:gs) = holes ps in

342344 ps { holes = g : n : gs } )

343− return $ Bind n (Hole tyv) t -- (weakenTm 1 t)

345+ return $ Bind n (Hole tyv) t

346+

347+-- If the current goal is 'retty', make a claim which is a function that

348+-- can compute a retty from argty (i.e a claim 'argty -> retty')

349+claimFn :: Name -> Name -> Raw -> RunTactic

350+claimFn n bn argty ctxt env t@(Bind x (Hole retty) sc) =

351+ do (tyv, tyt) <- lift $ check ctxt env argty

352+ lift $ isType ctxt env tyt

353+ action (\ps -> let (g:gs) = holes ps in

354+ ps { holes = g : n : gs } )

355+ return $ Bind n (Hole (Bind bn (Pi Nothing tyv tyt) retty)) t

356+claimFn _ _ _ ctxt env _ = fail "Can't make function type here"

344357

345358reorder_claims :: RunTactic

346359reorder_claims ctxt env t

@@ -440,6 +453,12 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

440453regret ctxt env (Bind x (Hole t) _)

441454 = fail $ show x ++ " : " ++ show t ++ " is not solved..."

442455

456+unifyGoal :: Raw -> RunTactic

457+unifyGoal tm ctxt env h@(Bind x b sc) =

458+ do (tmv, _) <- lift $ check ctxt env tm

459+ ns' <- unify' ctxt env (binderTy b) tmv

460+ return h

461+

443462exact :: Raw -> RunTactic

444463exact guess ctxt env (Bind x (Hole ty) sc) =

445464 do (val, valty) <- lift $ check ctxt env guess

@@ -961,6 +980,7 @@ process EndUnify _

961980process t h = tactic (Just h) (mktac t)

962981 where mktac Attack = attack

963982 mktac (Claim n r) = claim n r

983+ mktac (ClaimFn n bn r) = claimFn n bn r

964984 mktac (Exact r) = exact r

965985 mktac (Fill r) = fill r

966986 mktac (MatchFill r) = match_fill r

@@ -992,3 +1012,4 @@ process t h = tactic (Just h) (mktac t)

9921012 mktac (AutoArg n) = autoArg n

9931013 mktac (SetInjective n) = setinj n

9941014 mktac (MoveLast n) = movelast n

1015+ mktac (UnifyGoal r) = unifyGoal r

src/Idris/ElabTerm.hs+7−3

@@ -622,7 +622,7 @@ elab ist info emode opts fn tm

622622 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

623623 if (f `elem` map fst env && length args == 1 && length args_in == 1)

624624 then -- simple app, as below

625− do simple_app (elabE ina (Just fc) (PRef fc f))

625+ do simple_app False (elabE ina (Just fc) (PRef fc f))

626626 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

627627 (show tm)

628628 solve

@@ -746,9 +746,13 @@ elab ist info emode opts fn tm

746746

747747 elab' ina _ tm@(PApp fc f [arg])

748748 = erun fc $

749− do simple_app (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

750− (show tm)

749+ do simple_app (not $ headRef f)

750+ (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

751+ (show tm)

751752 solve

753+ where headRef (PRef _ _) = True

754+ headRef (PApp _ f _) = headRef f

755+ headRef _ = False

752756 elab' ina fc Placeholder

753757 = do (h : hs) <- get_holes

754758 movelast h

src/Idris/Primitives.hs+10−4

@@ -166,10 +166,16 @@ primitives =

166166 (2, LStrIndex) partial,

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

168168 (1, LStrRev) total,

169− Prim (sUN "prim__readString") (ty [WorldType,PtrType] StrType) 2 (p_cantreduce)

170− (2, LReadStr) total, -- total is okay, because we have 'WorldType'

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

172− (3, LWriteStr) total,

169+

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+

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

174180 (0, LVMPtr) total,

175181 -- Streams

src/Idris/ProofSearch.hs+1−1

@@ -171,7 +171,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

171171 tryLocalArg d n a

172172

173173 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)

174− tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))

174+ tryLocalArg d n i = simple_app False (tryLocalArg d n (i - 1))

175175 (psRec True d) "proof search local apply"

176176

177177 -- Like type class resolution, but searching with constructors