git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Providers.hs
42 lines 1.7 kB history raw
1{-# LANGUAGE PatternGuards, DeriveFunctor #-}
2module Idris.Providers (providerTy, getProvided, Provided(..)) where
4import Idris.Core.TT
5import Idris.Core.Evaluate
6import Idris.AbsSyntax
7import Idris.AbsSyntaxTree
8import Idris.Error
10-- | Wrap a type provider in the type of type providers
11providerTy :: FC -> PTerm -> PTerm
12providerTy fc tm
13 = PApp fc (PRef fc $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]
15ioret :: Name
16ioret = sUN "prim_io_return"
18ermod :: Name
19ermod = sNS (sUN "Error") ["Providers", "Prelude"]
21prmod :: Name
22prmod = sNS (sUN "Provide") ["Providers", "Prelude"]
24data Provided a = Provide a
25 deriving (Show, Eq, Functor)
27-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.
28getProvided :: FC -> TT Name -> Idris (Provided (TT Name))
29getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm
30 , (P _ nm _, [_, err]) <- unApply result
31 , pioret == ioret && nm == ermod
32 = case err of
33 Constant (Str msg) -> ierror . At fc . ProviderError $ msg
34 _ -> ifail "Internal error in type provider, non-normalised error"
35 | (P _ pioret _, [tp, result]) <- unApply tm
36 , (P _ nm _, [_, res]) <- unApply result
37 , pioret == ioret && nm == prmod
38 = return . Provide $ res
39 | otherwise = ifail $ "Internal type provider error: result was not " ++
40 "IO (Provider a), or perhaps missing normalisation." ++
41 "Term: " ++ take 1000 (show tm)