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

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

compare with master

unifiedsplit

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

4||| @ msg what to print

5||| @ result the final result

6trace : (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)

8

9

libs/prelude/IO.idr+9−2

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

96unsafePerformIO (MkIO f) = unsafePerformPrimIO

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

98

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+

99prim_fread : Ptr -> IO' l String

106prim_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))

101

108

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

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

103prim_fwrite h s

110prim_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))

105

112

106--------- The C FFI

113--------- The C FFI

107

114

libs/prelude/Prelude.idr+2−2

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

435

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

437putStr : String -> IO' l ()

438−putStr x = do prim_fwrite prim__stdout x

438+putStr x = do prim_write x

439 return ()

440

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

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

450||| Read one line of input from stdin

451partial

452getLine : IO' l String

453−getLine = prim_fread prim__stdin

453+getLine = prim_read

454

455||| Write a single character to stdout

456partial

src/IRTS/CodegenC.hs+8−3

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

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

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

433

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

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

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

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

436− ++ "),GETSTR("

436+ ++ ",GETSTR("

437 ++ creg s ++ "))))"

438

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+

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

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

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

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

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

446doOp 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 =

541

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

543jsFOREIGN _ 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−

552 | n == "isNull"

544 | n == "isNull"

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

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

554 JSAssign (

546 JSAssign (

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

687 jsOP'

679 jsOP'

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

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

689

681

682+ | LWriteStr <- op,

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

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

685+

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

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

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

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

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

688 | (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

55 | LStrConcat | LStrLt | LStrEq | LStrLen

56 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

57 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

58− | LReadStr | LWriteStr

58+ | LReadStr | LWriteStr | LReadFile | LWriteFile

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

60

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

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

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

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

316

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+

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

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

318exact t = processTactic' (Exact t)

324exact t = processTactic' (Exact t)

319

325

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

667 solve

673 solve

668 focus f

674 focus f

669

675

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

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

671−simple_app fun arg appstr =

677+simple_app infer fun arg app0str =

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

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

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

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

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

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

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

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

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

679 tm <- get_term

685 tm <- get_term

680 start_unify s

686 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

681 claim s (Var a)

691 claim s (Var a)

682 prep_fill f [s]

692 prep_fill f [s]

683 focus f; fun

693 focus f; fun

684 focus s; arg

694 focus s; arg

685 tm <- get_term

695 tm <- get_term

686 ps <- get_probs

696 ps <- get_probs

687− complete_fill

697+ ty <- goal

688 hs <- get_holes

698 hs <- get_holes

699+ complete_fill

689 env <- get_env

700 env <- get_env

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

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

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

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

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

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

704+ hs <- get_holes

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

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

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

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

695 end_unify

707 end_unify

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

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

402deNS (NS n _) = n

403deNS n = n

404

405+prf = sUN "prim__readFile"

406+pwf = sUN "prim__writeFile"

405prs = sUN "prim__readString"

407prs = sUN "prim__readString"

406pws = sUN "prim__writeString"

408pws = sUN "prim__writeString"

407pbm = sUN "prim__believe_me"

409pbm = sUN "prim__believe_me"

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

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

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

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

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

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

421getOp 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))

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

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

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

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

422 Just $ do execIO $ putStr n

432 Just $ do execIO $ putStr n

423 return (EConstant (I 0))

433 return (EConstant (I 0))

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

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

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

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

426 Just $ do line <- execIO getLine

436 Just $ do line <- execIO getLine

427 return (EConstant (Str line))

437 return (EConstant (Str line))

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

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

429− | fn == prs =

439+ | fn == pwf =

430 Just $ do execIO $ hPutStr h n

440 Just $ do execIO $ hPutStr h n

431 return (EConstant (I 0))

441 return (EConstant (I 0))

432getOp fn [_, EHandle h]

442getOp fn [_, EHandle h]

433− | fn == prs =

443+ | fn == prf =

434 Just $ do contents <- execIO $ hGetLine h

444 Just $ do contents <- execIO $ hGetLine h

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

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

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

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

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

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

50

51data Tactic = Attack

52 | Claim Name Raw

53+ | ClaimFn Name Name Raw

53 | Reorder Name

54 | Reorder Name

54 | Exact Raw

55 | Exact Raw

55 | Fill Raw

56 | Fill Raw

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

87 | MoveLast Name

88 | MoveLast Name

88 | MatchProblems Bool

89 | MatchProblems Bool

89 | UnifyProblems

90 | UnifyProblems

91+ | UnifyGoal Raw

90 | ProofState

92 | ProofState

91 | Undo

93 | Undo

92 | QED

94 | QED

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

340 lift $ isType ctxt env tyt

342 lift $ isType ctxt env tyt

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

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

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

344 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"

344

357

345reorder_claims :: RunTactic

358reorder_claims :: RunTactic

346reorder_claims ctxt env t

359reorder_claims ctxt env t

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

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

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

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

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

442

455

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+

443exact :: Raw -> RunTactic

462exact :: Raw -> RunTactic

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

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

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

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

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

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

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

962 where mktac Attack = attack

981 where mktac Attack = attack

963 mktac (Claim n r) = claim n r

982 mktac (Claim n r) = claim n r

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

964 mktac (Exact r) = exact r

984 mktac (Exact r) = exact r

965 mktac (Fill r) = fill r

985 mktac (Fill r) = fill r

966 mktac (MatchFill r) = match_fill r

986 mktac (MatchFill r) = match_fill r

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

992 mktac (AutoArg n) = autoArg n

1012 mktac (AutoArg n) = autoArg n

993 mktac (SetInjective n) = setinj n

1013 mktac (SetInjective n) = setinj n

994 mktac (MoveLast n) = movelast n

1014 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

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

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

624 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))

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

627 (show tm)

628 solve

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

746

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

748 = erun fc $

749+ do simple_app (not $ headRef f)

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

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

750− (show tm)

751+ (show tm)

751 solve

752 solve

753+ where headRef (PRef _ _) = True

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

755+ headRef _ = False

752 elab' ina fc Placeholder

756 elab' ina fc Placeholder

753 = do (h : hs) <- get_holes

757 = do (h : hs) <- get_holes

754 movelast h

758 movelast h

src/Idris/Primitives.hs+10−4

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

166 (2, LStrIndex) partial,

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

168 (1, LStrRev) 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,

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

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

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

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

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

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

172− (3, LWriteStr) total,

177+ (2, LWriteStr) total,

178+

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

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

174 (0, LVMPtr) total,

180 (0, LVMPtr) total,

175 -- Streams

181 -- Streams

src/Idris/ProofSearch.hs+1−1

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

171 tryLocalArg d n a

172

173 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))

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

176

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