diff options
Diffstat (limited to 'pkgs/profpatsch/xmonad/DhallTypedInput.hs')
-rw-r--r-- | pkgs/profpatsch/xmonad/DhallTypedInput.hs | 181 |
1 files changed, 181 insertions, 0 deletions
diff --git a/pkgs/profpatsch/xmonad/DhallTypedInput.hs b/pkgs/profpatsch/xmonad/DhallTypedInput.hs new file mode 100644 index 00000000..0e3ee06d --- /dev/null +++ b/pkgs/profpatsch/xmonad/DhallTypedInput.hs @@ -0,0 +1,181 @@ +{-# language RecordWildCards, NamedFieldPuns, OverloadedStrings, ScopedTypeVariables, KindSignatures, DataKinds, ScopedTypeVariables, RankNTypes, GADTs, TypeApplications, AllowAmbiguousTypes, LambdaCase #-} +module DhallTypedInput +( inputWithTypeArgs, TypeArg(..), TypeArgError(..), TypeArgEx(..), typeArg +) +where + +import Control.Monad.Trans.State.Strict as State +import GHC.TypeLits (KnownSymbol, Symbol, symbolVal) +import Data.Proxy (Proxy(Proxy)) +import Data.List (foldl') + +import Control.Exception (Exception) +import qualified Control.Exception + +import Dhall (Type(..), InvalidType(..), InputSettings(..), EvaluateSettings(..), rootDirectory, startingContext, normalizer, standardVersion, sourceName, defaultEvaluateSettings, Interpret(..), auto) +import Dhall.TypeCheck (X) +import Dhall.Core +import Dhall.Parser (Src(..)) +import qualified Dhall.Import +import qualified Dhall.Pretty +import qualified Dhall.TypeCheck +import qualified Dhall.Parser + +import Lens.Family (LensLike', set, view) + +import qualified Data.Text as Text + +import Data.Text.Prettyprint.Doc (Pretty) +import qualified Data.Text.Prettyprint.Doc as Pretty +import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty +import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty + + +data TypeArg (sym :: Symbol) t = TypeArg + +-- | existential wrapper of a type arg +data TypeArgEx + where TypeArgEx :: (KnownSymbol sym, Interpret t) => TypeArg sym t -> TypeArgEx + +typeArg :: forall sym t. (KnownSymbol sym, Interpret t) => TypeArgEx +typeArg = TypeArgEx (TypeArg :: TypeArg sym t) + +data TypeArgError + = WrongLabel Text.Text + | NoLambda + +applyTypeArg + :: forall sym t. (KnownSymbol sym, Interpret t) + => Expr Src X + -> TypeArg sym t + -> Either TypeArgError (Expr Src X) +applyTypeArg expr ta@(TypeArg) = case expr of + (Lam label (Const Dhall.Core.Type) _) + -> let expectedLabel = getLabel ta + in if label /= getLabel ta + then Left (WrongLabel expectedLabel) + else let expr' = (normalize (App expr tExpect)) + in Right expr' + where + Dhall.Type _ tExpect = Dhall.auto :: Dhall.Type t + expr -> Left NoLambda + +getLabel :: forall sym t. (KnownSymbol sym) => TypeArg sym t -> Text.Text +getLabel _ = Text.pack $ symbolVal (Proxy :: (Proxy :: Symbol -> *) sym) + +instance (KnownSymbol sym) => Show (TypeArg sym t) where + show TypeArg = + "TypeArg " + ++ (symbolVal (Proxy :: (Proxy :: Symbol -> *) sym)) + +inputWithTypeArgs + :: InputSettings + -> [TypeArgEx] + -> Dhall.Type a + -> Text.Text + -> IO a +inputWithTypeArgs settings typeArgs (Dhall.Type {extract, expected}) txt = do + expr <- throws (Dhall.Parser.exprFromText (view sourceName settings) txt) + + -- TODO: evaluateSettings not exposed + -- let evSettings = view evaluateSettings settings + let evSettings :: EvaluateSettings = defaultEvaluateSettings + + let transform = + set Dhall.Import.standardVersion + (view standardVersion evSettings) + . set Dhall.Import.normalizer + (view normalizer evSettings) + . set Dhall.Import.startingContext + (view startingContext evSettings) + + let status = transform (Dhall.Import.emptyStatus + (view rootDirectory settings)) + + expr' <- State.evalStateT (Dhall.Import.loadWith expr) status + + let skipNote e f = case e of + Note n e -> Note n $ f e + e -> f e + + let + stripTypeArg :: Expr Src X -> TypeArgEx -> Expr Src X + stripTypeArg e (TypeArgEx ta) = skipNote e $ \e' -> case e' of + (Lam label _ _) -> + case applyTypeArg e' ta of + Right e'' -> e'' + -- TODO obvously + Left (WrongLabel l) -> + error $ "Wrong label, should have been `" ++ Text.unpack l ++ "` but was `" ++ Text.unpack label ++ "`" + Left NoLambda -> error $ "I expected a lambda of the form λ(" ++ Text.unpack label ++ ": Type) → but got: " ++ show e + e' -> error $ show e' + + let expr'' = foldl' stripTypeArg expr' typeArgs + + -- - check first arg is \(label: Type) lambda + -- - type-check expression + -- - apply the type we label to signify to expression + -- - type-check the new normalized expression + -- - TODO: check if the error message makes sense to the user + let suffix = prettyToStrictText expected + let annot = case expr'' of + Note (Src begin end bytes) _ -> + -- Note (Src begin end bytes') (Annot expr'' expected) + Annot expr'' expected + where + bytes' = bytes <> " : " <> suffix + _ -> + Annot expr'' expected + print annot + _ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) annot) + case extract (Dhall.Core.normalizeWith (Dhall.Core.getReifiedNormalizer (view normalizer settings)) expr'') of + Just x -> return x + Nothing -> Control.Exception.throwIO InvalidType + +prettyToStrictText :: Pretty a => a -> Text.Text +prettyToStrictText = docToStrictText . Pretty.pretty + +docToStrictText :: Pretty.Doc ann -> Text.Text +docToStrictText = Pretty.renderStrict . Pretty.layoutPretty options + where + options = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded } + +throws :: Exception e => Either e a -> IO a +throws (Left e) = Control.Exception.throwIO e +throws (Right r) = return r + +-- data WrongTypeLabel = WrongTypeLabel deriving (Typeable) + +-- _ERROR :: String +-- _ERROR = "\ESC[1;31mError\ESC[0m" + +-- instance Show WrongTypeLabel where +-- show WrongTypeLabel = +-- _ERROR <> ": Mislabelled type lambda +-- \ \n\ +-- \Expected your t provide an extract function that succeeds if an expression \n\ +-- \matches the expected type. You provided a Type that disobeys this contract \n" + +-- instance (KnownSymbol s, D.Interpret t, D.Interpret a) +-- => D.Interpret (TypeArg s t a) +-- where +-- autoWith opts = D.Type +-- { D.extract = extr +-- -- TODO: the symbolVal is ignored for the type check; +-- -- yet, if the type check succeeds, we cannot fail +-- -- in the extract function (even if the label is wrong) +-- , D.expected = DC.Pi (T.pack expectedLabel) (DC.Const DC.Type) aExpect +-- } +-- where +-- expectedLabel = symbolVal (Proxy :: (Proxy :: Symbol -> *) s) +-- D.Type aExtr aExpect = D.autoWith opts :: D.Type a +-- D.Type tExtr tExpect = D.autoWith opts :: D.Type t +-- extr expr@(DC.Lam label (DC.Const DC.Type) _) +-- | label == T.pack (symbolVal (Proxy :: (Proxy :: Symbol -> *) s)) +-- = Just (case aExtr (DC.normalize (DC.App expr tExpect)) of +-- Just a -> TypeArg a +-- Nothing -> error $ show (DC.normalize (DC.App expr tExpect) :: DC.Expr () DCT.X)) +-- -- TODO: nice error message?! +-- | otherwise = error ("Wrong type label; expected " +-- ++ expectedLabel ++ ", was " ++ T.unpack label) +-- extr _ = Nothing |