module LambdaCube.SystemFw_.Elaborator ( elaborate , elaborateType , elaborateKind ) where import Data.List (elemIndex) import qualified Data.Text as Text import LambdaCube.SystemFw_.Ast elaborate :: ExtLCTerm -> LCTerm elaborate :: ExtLCTerm -> LCTerm elaborate = [Text] -> ExtLCTerm -> LCTerm go [] where go :: [Text] -> ExtLCTerm -> LCTerm go [Text] l (ExtLCVar Text x) | Just Int n <- Text x Text -> [Text] -> Maybe Int forall a. Eq a => a -> [a] -> Maybe Int `elemIndex` [Text] l = Int -> LCTerm LCVar Int n | Bool otherwise = [Char] -> LCTerm forall a. HasCallStack => [Char] -> a error ([Char] -> LCTerm) -> [Char] -> LCTerm forall a b. (a -> b) -> a -> b $ [Char] "Term variable " [Char] -> [Char] -> [Char] forall a. Semigroup a => a -> a -> a <> Text -> [Char] Text.unpack Text x [Char] -> [Char] -> [Char] forall a. Semigroup a => a -> a -> a <> [Char] " is not in scope" go [Text] l (ExtLCLam Text x ExtLCType t ExtLCTerm b) = LCType -> LCTerm -> LCTerm LCLam (ExtLCType -> LCType elaborateType ExtLCType t) (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ [Text] -> ExtLCTerm -> LCTerm go (Text x Text -> [Text] -> [Text] forall a. a -> [a] -> [a] : [Text] l) ExtLCTerm b go [Text] l (ExtLCApp ExtLCTerm f ExtLCTerm a) = [Text] -> ExtLCTerm -> LCTerm go [Text] l ExtLCTerm f LCTerm -> LCTerm -> LCTerm `LCApp` [Text] -> ExtLCTerm -> LCTerm go [Text] l ExtLCTerm a go [Text] _ (ExtLCMVar [Char] _) = [Char] -> LCTerm forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer" elaborateType :: ExtLCType -> LCType elaborateType :: ExtLCType -> LCType elaborateType = [Text] -> ExtLCType -> LCType go [] where go :: [Text] -> ExtLCType -> LCType go [Text] _ ExtLCType ExtLCBase = LCType LCBase go [Text] l (ExtLCTVar Text p) | Just Int n <- Text p Text -> [Text] -> Maybe Int forall a. Eq a => a -> [a] -> Maybe Int `elemIndex` [Text] l = Int -> LCType LCTVar Int n | Bool otherwise = [Char] -> LCType forall a. HasCallStack => [Char] -> a error ([Char] -> LCType) -> [Char] -> LCType forall a b. (a -> b) -> a -> b $ [Char] "Type variable " [Char] -> [Char] -> [Char] forall a. Semigroup a => a -> a -> a <> Text -> [Char] Text.unpack Text p [Char] -> [Char] -> [Char] forall a. Semigroup a => a -> a -> a <> [Char] " is not in scope" go [Text] l (ExtLCArr ExtLCType a ExtLCType b) = [Text] -> ExtLCType -> LCType go [Text] l ExtLCType a LCType -> LCType -> LCType `LCArr` [Text] -> ExtLCType -> LCType go [Text] l ExtLCType b go [Text] l (ExtLCTTLam Text p ExtLCKind k ExtLCType b) = LCKind -> LCType -> LCType LCTTLam (ExtLCKind -> LCKind elaborateKind ExtLCKind k) (LCType -> LCType) -> LCType -> LCType forall a b. (a -> b) -> a -> b $ [Text] -> ExtLCType -> LCType go (Text p Text -> [Text] -> [Text] forall a. a -> [a] -> [a] : [Text] l) ExtLCType b go [Text] l (ExtLCTTApp ExtLCType f ExtLCType a) = [Text] -> ExtLCType -> LCType go [Text] l ExtLCType f LCType -> LCType -> LCType `LCTTApp` [Text] -> ExtLCType -> LCType go [Text] l ExtLCType a go [Text] _ (ExtLCMTVar [Char] _) = [Char] -> LCType forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer" elaborateKind :: ExtLCKind -> LCKind elaborateKind :: ExtLCKind -> LCKind elaborateKind = ExtLCKind -> LCKind go where go :: ExtLCKind -> LCKind go ExtLCKind ExtLCStar = LCKind LCStar go (ExtLCKArr ExtLCKind a ExtLCKind b) = ExtLCKind -> LCKind go ExtLCKind a LCKind -> LCKind -> LCKind `LCKArr` ExtLCKind -> LCKind go ExtLCKind b go (ExtLCMKVar [Char] _) = [Char] -> LCKind forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer"