module LambdaCube.SystemF.Elaborator ( elaborate , elaborateType ) where import Data.List (elemIndex) import Data.Text (Text) import qualified Data.Text as Text import LambdaCube.SystemF.Ast elaborate :: ExtLCTerm -> LCTerm elaborate :: ExtLCTerm -> LCTerm elaborate = [Text] -> [Text] -> ExtLCTerm -> LCTerm go [] [] where go :: [Text] -> [Text] -> ExtLCTerm -> LCTerm go [Text] _ [Text] vl (ExtLCVar Text x) | Just Int n <- Text x Text -> [Text] -> Maybe Int forall a. Eq a => a -> [a] -> Maybe Int `elemIndex` [Text] vl = 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] tl [Text] vl (ExtLCLam Text x ExtLCType t ExtLCTerm b) = LCType -> LCTerm -> LCTerm LCLam ([Text] -> ExtLCType -> LCType elaborateType [Text] tl ExtLCType t) (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ [Text] -> [Text] -> ExtLCTerm -> LCTerm go [Text] tl (Text x Text -> [Text] -> [Text] forall a. a -> [a] -> [a] : [Text] vl) ExtLCTerm b go [Text] tl [Text] vl (ExtLCApp ExtLCTerm f ExtLCTerm a) = [Text] -> [Text] -> ExtLCTerm -> LCTerm go [Text] tl [Text] vl ExtLCTerm f LCTerm -> LCTerm -> LCTerm `LCApp` [Text] -> [Text] -> ExtLCTerm -> LCTerm go [Text] tl [Text] vl ExtLCTerm a go [Text] tl [Text] vl (ExtLCTLam Text p ExtLCTerm b) = LCTerm -> LCTerm LCTLam (LCTerm -> LCTerm) -> LCTerm -> LCTerm forall a b. (a -> b) -> a -> b $ [Text] -> [Text] -> ExtLCTerm -> LCTerm go (Text p Text -> [Text] -> [Text] forall a. a -> [a] -> [a] : [Text] tl) [Text] vl ExtLCTerm b go [Text] tl [Text] vl (ExtLCTApp ExtLCTerm f ExtLCType t) = [Text] -> [Text] -> ExtLCTerm -> LCTerm go [Text] tl [Text] vl ExtLCTerm f LCTerm -> LCType -> LCTerm `LCTApp` [Text] -> ExtLCType -> LCType elaborateType [Text] tl ExtLCType t go [Text] _ [Text] _ (ExtLCMVar [Char] _) = [Char] -> LCTerm forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer" elaborateType :: [Text] -> ExtLCType -> LCType elaborateType :: [Text] -> 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 (ExtLCUniv Text p ExtLCType a) = LCType -> LCType LCUniv (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 a go [Text] _ (ExtLCMTVar [Char] _) = [Char] -> LCType forall a. HasCallStack => [Char] -> a error [Char] "invalid TemplateHaskell code splicer"