git.iko.soy/Idris-dev
on master help sign in
Special-case prim__believe_me

Because the unification of primitive ops required that primitives only work on constants, believe_me needs to be special in both the evaluator and the executor.

commit656f219e80752589aaa4119a123653c949f20f2c authorDavid Christiansen <david@davidchristiansen.dk> dateThu 27 Jun 2013, 12:54 (13 years ago) parentfc79985
3 files changed+19−12
compare with master
unifiedsplit
src/Core/Execute.hs+1 src/Idris/ElabDecls.hs+17 src/Idris/Primitives.hs+1−12
src/Core/Execute.hs+1
@@ -320,6 +320,7 @@ execApp' env ctxt f args = return (mkEApp f args)
320320
321321-- | Look up primitive operations in the global table and transform them into ExecVal functions
322322getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
323+getOp (UN "prim__believe_me") [_, _, x] = Just (return x)
323324getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
324325 Just $ do line <- execIO getLine
325326 return (EConstant (Str line))
src/Idris/ElabDecls.hs+17
@@ -13,6 +13,7 @@ import Idris.Coverage
1313import Idris.DataOpts
1414import Idris.Providers
1515import Idris.Primitives
16+import IRTS.Lang
1617import Paths_idris
1718
1819import Core.TT
@@ -218,6 +219,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
218219 (map (PData "" defaultSyntax (FC "builtin" 0) False)
219220 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
220221 mapM_ elabPrim primitives
222+ -- Special case prim__believe_me because it doesn't work on just constants
223+ elabBelieveMe
221224 where elabPrim :: Prim -> Idris ()
222225 elabPrim (Prim n ty i def sc tot)
223226 = do updateContext (addOperator n ty i (valuePrim def))
@@ -232,6 +235,20 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
232235 getConst _ = Nothing
233236
234237
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+
235252-- | Elaborate a type provider
236253elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
237254elabProvider info syn fc n ty tm
src/Idris/Primitives.hs+1−12
@@ -24,11 +24,6 @@ ty :: [Const] -> Const -> Type
2424ty [] x = Constant x
2525ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
2626
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−
3227total, partial :: Totality
3328total = Total []
3429partial = Partial NotCovering
@@ -178,9 +173,7 @@ primitives =
178173 (0, LVMPtr) total,
179174 -- Streams
180175 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
181− (0, LStdIn) partial,
182− Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
183− (3, LNoOp) partial -- ahem
176+ (0, LStdIn) partial
184177 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]
185178
186179intOps :: IntTy -> [Prim]
@@ -229,10 +222,6 @@ iCoerce from to op impl irop =
229222 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)
230223 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total
231224
232−p_believeMe :: [a] -> Maybe a
233−p_believeMe [_,_,x] = Just x
234−p_believeMe _ = Nothing
235−
236225iUn :: (Int -> Int) -> [Const] -> Maybe Const
237226iUn op [I x] = Just $ I (op x)
238227iUn _ _ = Nothing