Interpreter.hs

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}

module Boilerplate.Interpreter (interpretRule) where

import Boilerplate.Types
import Data.List (intersect)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Text (Text)
import qualified Data.Text as T
import HsInspect.Types (Type(..))

data Ctx = G -- ^^ global context
         | P Text [(Maybe Text, Text, TyCtx)] -- ^^ product-like thing: cons [(maybe fieldname, param type, typarams)]
         | F Text Int (Maybe Text) Text TyCtx -- ^^ field in a product-like: cons idx fieldname param type typarams
         | T Text -- ^^ type parameter field
  deriving (Eq, Show)

data TyCtx = Poly | Higher | Concrete
  deriving (Eq, Show)

interpretRule :: Rule -> Type -> Map Text Custom -> Either Text Text
interpretRule (Rule atoms) tpe options = T.strip <$> interpretTree G atoms
  where
    interpretTree :: Ctx -> Tree -> Either Text Text
    interpretTree ctx t = T.concat <$> traverse (interpret ctx) t

    -- Several codepaths are impossible because of the way the Rule is parsed. We
    -- could have done some fancy type magic to avoid having to consider these
    -- cases, but it is far easier and simpler to just take the hit in the
    -- interpreter.
    impossible :: String -> a
    impossible ctx = error $ "impossible " <> ctx

    showt :: Show a => a -> Text
    showt = T.pack . show

    param :: Int -> Int -> Text
    param n p = "p_" <> showt n <> "_" <> showt p

    tyCtx :: [Text] -> Text -> [Text] -> TyCtx
    tyCtx type_params tpe tpe_params =
      if elem tpe type_params
      then Poly
      else if not . null $ intersect type_params tpe_params
      then Higher
      else Concrete

    -- no context interpreter
    interpret ctx = \case
      Raw txt -> Right txt
      Type -> Right $ case tpe of
        ProductType tn _ _ _ _ -> tn
        RecordType tn _ _ _ _ -> tn
        SumType tn _ _ -> tn
      TParams empty prefix els sep suffix ->
        if null tparams
        then interpretTree G empty
        else (\p b -> p <> b <> suffix) <$> interpretTree G prefix <*> body
        where
          tparams = T <$> case tpe of
            ProductType _ tps _ _ _ -> tps
            RecordType _ tps _ _ _ -> tps
            SumType _ tps _ -> tps
          body = T.intercalate sep <$> traverse (flip interpretTree els) tparams
      TParam -> case ctx of
        T p -> Right p
        _ -> impossible "TParam"
      Product els ->
        let interpret' c ps = interpretTree (P c ps) els
         in case tpe of
        SumType _ _ _ -> Right T.empty
        ProductType _ tps _ cons params -> interpret' cons $ (\(tpe, tys) -> (Nothing, tpe, tyCtx tps tpe tys)) <$> params
        RecordType _ tps _ cons params -> interpret' cons $ (\(nme, tpe, tys) -> (Just nme, tpe, tyCtx tps tpe tys)) <$> params
      Sum prefix els sep suffix -> case tpe of
        ProductType _ _ _ _ _ -> Right T.empty
        RecordType _ _ _ _ _ -> Right T.empty
        SumType _ tps tags -> (\b -> prefix <> b <> suffix) <$> body
          where
            tags' = (\(cons, tpes) -> P cons ((\(tpe, tys) -> (Nothing, tpe, tyCtx tps tpe tys)) <$> tpes)) <$> tags
            body = T.intercalate sep <$> traverse (flip interpretTree els) tags'
      Uncons n -> case ctx of
        P cons [] -> Right cons
        P cons ps -> Right $ "(" <> body <> ")"
          where
            body = T.intercalate " " $ cons : ((param n . fst) <$> zip [1..] ps)
        _ -> impossible "Uncons"
      Cons -> case ctx of
        P cons _ -> Right cons
        F cons _ _ _ _ -> Right cons
        _ -> impossible "Cons"
      Field empty prefix els sep suffix -> case ctx of
        P _ [] -> interpretTree ctx empty
        P cons ps -> (\p b -> p <> b <> suffix) <$> interpretTree ctx prefix <*> body
          where
            fields = (\(n, (f, t, tc)) -> F cons n f t tc) <$> zip [1..] ps
            body = T.intercalate sep <$> traverse (flip interpretTree els) fields
        _ -> impossible "Field"
      Param n ->  case ctx of
        F _ p _ _ _ -> Right $ param n p
        _ -> impossible "Param"
      FieldName -> case ctx of
        F _ _ n _ _ -> maybe (Left "field names are required") Right n
        _ -> impossible "FieldName"
      FieldType -> case ctx of
        F _ _ _ t _ -> Right t
        _ -> impossible "FieldType"
      TyCase poly higher concrete -> case ctx of
        F _ _ _ _ ty -> interpretTree ctx $ case ty of
          Poly -> poly
          Higher -> higher
          Concrete -> concrete
        _ -> impossible "TyCase"
      Custom sym fallback ->
        let err = Left $ "missing required option '" <> sym <> "' which should be " <> ctx'
            ctx' = case ctx of
              G -> "a global value"
              T _ -> "a global value"
              P cons _ -> "a mapping for the data constructors of " <> cons
              F cons _ _ _ _ -> "an indexed sequence for fields of the data constructor " <> cons
         in case (M.lookup sym options, ctx) of
          (Just (Global txt), _) -> Right txt
          (Just (Indexed vs), F _ p _ _ _) -> maybe err Right $ atMay (p - 1) vs
          (Just (Named vs), F _ _ (Just f) _ _) -> maybe err Right $ M.lookup f vs
          (Just (NamedIndexed vs), F cons p _ _ _) -> maybe err Right $ atMay (p - 1) =<< M.lookup cons vs
          (Just (Named vs), P cons _) -> maybe err Right $ M.lookup cons vs
          _ -> case fallback of
            Nothing -> err
            Just t -> interpretTree ctx t
      Sugar sugar -> interpretTree ctx $ case sugar of
        Instance tc ->
          [Raw "instance ",
           TParams [] [Raw "("] [Raw tc, Raw " ", TParam] ", " ") => ", Raw tc, Raw " ",
           TParams [Type] [Raw "(", Type, Raw " "] [TParam] " " ")", Raw " where"]
        Data tree ->
          [Product tree, Sum "" tree "" ""]

atMay :: Int -> [a] -> Maybe a
atMay i as | i < 0 = Nothing
        | otherwise = f i as
    where f 0 (x : _) = Just x
          f i' (_ : as') = f (i' - 1) as'
          f _ [] = Nothing