git.iko.soy/Idris-dev
on master help sign in
Merge pull request #335 from david-christiansen/providers-work

Updates to type provider infrastructure

commitb91563534847c553288209d1505b54e071c3c73e authorEdwin Brady <edwin.brady@gmail.com> dateThu 20 Jun 2013, 01:24 (13 years ago) parent06a7456b906162
2 files changed+12−2
compare with master
unifiedsplit
src/Core/Execute.hs+11−1 test/test026/test026.idr+1−1
src/Core/Execute.hs+11−1
@@ -274,6 +274,16 @@ execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f arg
274274 Just r -> return (mkEApp r (drop (length argTs) xs))
275275 | otherwise = return (mkEApp f args)
276276
277+execApp' env ctxt c@(EP (DCon _ arity) n _) args =
278+ do args' <- mapM tryForce (take arity args)
279+ let restArgs = drop arity args
280+ execApp' env ctxt (mkEApp c args') restArgs
281+
282+execApp' env ctxt c@(EP (TCon _ arity) n _) args =
283+ do args' <- mapM tryForce (take arity args)
284+ let restArgs = drop arity args
285+ execApp' env ctxt (mkEApp c args') restArgs
286+
277287execApp' env ctxt f@(EP _ n _) args =
278288 do let val = lookupDef n ctxt
279289 case val of
@@ -350,7 +360,7 @@ execApp' env ctxt f@(EP _ n _) args =
350360 return (EConstant (Str line))
351361 getOp (UN "prim__readString") [EHandle h] =
352362 Just $ do contents <- execIO $ hGetLine h
353− return (EConstant (Str contents))
363+ return (EConstant (Str (contents ++ "\n")))
354364 getOp (UN "prim__shLInt") [EConstant (I i1), EConstant (I i2)] =
355365 primRes I (shiftL i1 i2)
356366 getOp (UN "prim__shRInt") [EConstant (I i1), EConstant (I i2)] =
test/test026/test026.idr+1−1
@@ -13,7 +13,7 @@ strToType _ = Nat
1313-- If the file contains "Int", provide Int as a type, otherwise provide Nat
1414fromFile : String -> IO (Provider Type)
1515fromFile fname = do str <- readFile fname
16− return (Provide (strToType str))
16+ return (Provide (strToType (trim str)))
1717
1818%provide (T1 : Type) with fromFile "theType"
1919%provide (T2 : Type) with fromFile "theOtherType"