git.iko.soy/Idris-dev
on master help sign in
Special-case prim__believe_me
656f219David Christiansen
src/Core/Execute.hs+1
compare with master
unifiedsplit
@@ -320,6 +320,7 @@ execApp' env ctxt f args = return (mkEApp f args)
320
320
321-- | Look up primitive operations in the global table and transform them into ExecVal functions
321-- | Look up primitive operations in the global table and transform them into ExecVal functions
322getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
322getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
323+getOp (UN "prim__believe_me") [_, _, x] = Just (return x)
323getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
324getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
324 Just $ do line <- execIO getLine
325 Just $ do line <- execIO getLine
325 return (EConstant (Str line))
326 return (EConstant (Str line))
src/Idris/ElabDecls.hs+17
@@ -13,6 +13,7 @@ import Idris.Coverage
13import Idris.DataOpts
13import Idris.DataOpts
14import Idris.Providers
14import Idris.Providers
15import Idris.Primitives
15import Idris.Primitives
16+import IRTS.Lang
16import Paths_idris
17import Paths_idris
17
18
18import Core.TT
19import Core.TT
@@ -218,6 +219,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
218 (map (PData "" defaultSyntax (FC "builtin" 0) False)
219 (map (PData "" defaultSyntax (FC "builtin" 0) False)
219 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
220 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
220 mapM_ elabPrim primitives
221 mapM_ elabPrim primitives
222+ -- Special case prim__believe_me because it doesn't work on just constants
223+ elabBelieveMe
221 where elabPrim :: Prim -> Idris ()
224 where elabPrim :: Prim -> Idris ()
222 elabPrim (Prim n ty i def sc tot)
225 elabPrim (Prim n ty i def sc tot)
223 = do updateContext (addOperator n ty i (valuePrim def))
226 = do updateContext (addOperator n ty i (valuePrim def))
@@ -232,6 +235,20 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
232 getConst _ = Nothing
235 getConst _ = Nothing
233
236
234
237
238+ p_believeMe [_,_,x] = Just x
239+ p_believeMe _ = Nothing
240+ believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
241+ (Bind (UN "b") (Pi (TType (UVar (-2))))
242+ (Bind (UN "x") (Pi (V 1)) (V 1)))
243+ elabBelieveMe = do let prim__believe_me = (UN "prim__believe_me")
244+ updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
245+ setTotality prim__believe_me (Partial NotCovering)
246+ i <- getIState
247+ putIState i {
248+ idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
249+ }
250+
251+
235-- | Elaborate a type provider
252-- | Elaborate a type provider
236elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
253elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
237elabProvider info syn fc n ty tm
254elabProvider info syn fc n ty tm
src/Idris/Primitives.hs+1−12
@@ -24,11 +24,6 @@ ty :: [Const] -> Const -> Type
24ty [] x = Constant x
24ty [] x = Constant x
25ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
25ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
26
26
27−believeTy :: Type
28−believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))
29− (Bind (UN "b") (Pi (TType (UVar (-2))))
30− (Bind (UN "x") (Pi (V 1)) (V 1)))
31−
32total, partial :: Totality
27total, partial :: Totality
33total = Total []
28total = Total []
34partial = Partial NotCovering
29partial = Partial NotCovering
@@ -178,9 +173,7 @@ primitives =
178 (0, LVMPtr) total,
173 (0, LVMPtr) total,
179 -- Streams
174 -- Streams
180 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
175 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
181− (0, LStdIn) partial,
176+ (0, LStdIn) partial
182− Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
183− (3, LNoOp) partial -- ahem
184 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
177 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
185
178
186intOps :: IntTy -> [Prim]
179intOps :: IntTy -> [Prim]
@@ -229,10 +222,6 @@ iCoerce from to op impl irop =
229 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
222 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
230 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
223 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
231
224
232−p_believeMe :: [a] -> Maybe a
233−p_believeMe [_,_,x] = Just x
234−p_believeMe _ = Nothing
235−
236iUn :: (Int -> Int) -> [Const] -> Maybe Const
225iUn :: (Int -> Int) -> [Const] -> Maybe Const
237iUn op [I x] = Just $ I (op x)
226iUn op [I x] = Just $ I (op x)
238iUn _ _ = Nothing
227iUn _ _ = Nothing