git.iko.soy/Idris-dev
on 08ddbaa help sign in
Idris-dev/src/Idris/Providers.hs
44 lines 1.8 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
10import Debug.Trace
12-- | Wrap a type provider in the type of type providers
13providerTy :: FC -> PTerm -> PTerm
14providerTy fc tm
15 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]
17ioret = sUN "prim_io_return"
18ermod = sNS (sUN "Error") ["Providers"]
19prmod = sNS (sUN "Provide") ["Providers"]
20posmod = sNS (sUN "Postulate") ["Providers"]
22data Provided a = Provide a
23 | Postulate
24 deriving (Show, Eq, Functor)
26-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.
27getProvided :: FC -> TT Name -> Idris (Provided (TT Name))
28getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm
29 , (P _ nm _, [_, err]) <- unApply result
30 , pioret == ioret && nm == ermod
31 = case err of
32 Constant (Str msg) -> ierror . At fc . ProviderError $ msg
33 _ -> ifail "Internal error in type provider, non-normalised error"
34 | (P _ pioret _, [tp, result]) <- unApply tm
35 , (P _ nm _, [_, res]) <- unApply result
36 , pioret == ioret && nm == prmod
37 = return . Provide $ res
38 | (P _ pioret _, [tp, result]) <- unApply tm
39 , (P _ nm _, [_]) <- unApply result
40 , pioret == ioret && nm == posmod
41 = return Postulate
42 | otherwise = ifail $ "Internal type provider error: result was not " ++
43 "IO (Provider a), or perhaps missing normalisation."