From 11e303679fa95b36c4696867d89a5ad9331f494c Mon Sep 17 00:00:00 2001 From: Jakob Naucke Date: Wed, 10 Apr 2024 23:57:41 +0200 Subject: [PATCH] Initial strict runtime check --- agda2hs.cabal | 1 + lib/Haskell/Extra/Dec/Instances.agda | 80 ++++++ src/Agda2Hs/Compile.hs | 66 ++--- src/Agda2Hs/Compile/Data.hs | 49 +++- src/Agda2Hs/Compile/Function.hs | 39 ++- src/Agda2Hs/Compile/Name.hs | 9 +- src/Agda2Hs/Compile/Record.hs | 61 +++-- src/Agda2Hs/Compile/RuntimeCheckUtils.hs | 234 ++++++++++++++++++ src/Agda2Hs/Compile/Types.hs | 13 +- src/Agda2Hs/Compile/Utils.hs | 25 +- src/Agda2Hs/HsUtils.hs | 3 + src/Agda2Hs/Render.hs | 50 ++-- src/Main.hs | 9 +- test/AllFailTests.agda | 2 + test/AllRuntimeCheckFailTests.agda | 5 + test/AllRuntimeCheckTests.agda | 4 + test/AllTests.agda | 3 + test/Fail/PostRtc.agda | 2 + test/Fail/RuntimeCheckArg.agda | 7 + test/Fail/RuntimeCheckClass.agda | 16 ++ test/Fail/RuntimeCheckGo.agda | 7 + test/Fail/RuntimeCheckInline.agda | 11 + test/Fail/RuntimeCheckSc.agda | 11 + test/Fail/RuntimeCheckTransparent.agda | 11 + test/Fail/RuntimeCheckUnboxed.agda | 11 + test/Fail/RuntimeCheckUp.agda | 7 + test/Makefile | 15 +- test/RuntimeCheckCallFeatures.agda | 10 + test/RuntimeCheckFeatures.agda | 56 +++++ test/RuntimeCheckUseCases.agda | 13 + test/golden/AllRuntimeCheckTests.hs | 4 + test/golden/AllRuntimeCheckTests/PostRtc.hs | 2 + test/golden/AllTests.hs | 3 + test/golden/PostRtc.err | 1 + test/golden/RuntimeCheckArg.err | 2 + test/golden/RuntimeCheckCallFeatures.hs | 7 + .../RuntimeCheckCallFeatures/PostRtc.hs | 8 + test/golden/RuntimeCheckClass.err | 2 + test/golden/RuntimeCheckFeatures.hs | 66 +++++ test/golden/RuntimeCheckFeatures/PostRtc.hs | 31 +++ test/golden/RuntimeCheckGo.err | 2 + test/golden/RuntimeCheckInline.err | 2 + test/golden/RuntimeCheckSc.err | 2 + test/golden/RuntimeCheckTransparent.err | 2 + test/golden/RuntimeCheckUnboxed.err | 2 + test/golden/RuntimeCheckUp.err | 2 + test/golden/RuntimeCheckUseCases.hs | 20 ++ test/golden/RuntimeCheckUseCases/PostRtc.hs | 11 + 48 files changed, 902 insertions(+), 97 deletions(-) create mode 100644 lib/Haskell/Extra/Dec/Instances.agda create mode 100644 src/Agda2Hs/Compile/RuntimeCheckUtils.hs create mode 100644 test/AllRuntimeCheckFailTests.agda create mode 100644 test/AllRuntimeCheckTests.agda create mode 100644 test/Fail/PostRtc.agda create mode 100644 test/Fail/RuntimeCheckArg.agda create mode 100644 test/Fail/RuntimeCheckClass.agda create mode 100644 test/Fail/RuntimeCheckGo.agda create mode 100644 test/Fail/RuntimeCheckInline.agda create mode 100644 test/Fail/RuntimeCheckSc.agda create mode 100644 test/Fail/RuntimeCheckTransparent.agda create mode 100644 test/Fail/RuntimeCheckUnboxed.agda create mode 100644 test/Fail/RuntimeCheckUp.agda create mode 100644 test/RuntimeCheckCallFeatures.agda create mode 100644 test/RuntimeCheckFeatures.agda create mode 100644 test/RuntimeCheckUseCases.agda create mode 100644 test/golden/AllRuntimeCheckTests.hs create mode 100644 test/golden/AllRuntimeCheckTests/PostRtc.hs create mode 100644 test/golden/PostRtc.err create mode 100644 test/golden/RuntimeCheckArg.err create mode 100644 test/golden/RuntimeCheckCallFeatures.hs create mode 100644 test/golden/RuntimeCheckCallFeatures/PostRtc.hs create mode 100644 test/golden/RuntimeCheckClass.err create mode 100644 test/golden/RuntimeCheckFeatures.hs create mode 100644 test/golden/RuntimeCheckFeatures/PostRtc.hs create mode 100644 test/golden/RuntimeCheckGo.err create mode 100644 test/golden/RuntimeCheckInline.err create mode 100644 test/golden/RuntimeCheckSc.err create mode 100644 test/golden/RuntimeCheckTransparent.err create mode 100644 test/golden/RuntimeCheckUnboxed.err create mode 100644 test/golden/RuntimeCheckUp.err create mode 100644 test/golden/RuntimeCheckUseCases.hs create mode 100644 test/golden/RuntimeCheckUseCases/PostRtc.hs diff --git a/agda2hs.cabal b/agda2hs.cabal index b8343909..720d4a0f 100644 --- a/agda2hs.cabal +++ b/agda2hs.cabal @@ -47,6 +47,7 @@ executable agda2hs Agda2Hs.Compile.Name, Agda2Hs.Compile.Postulate, Agda2Hs.Compile.Record, + Agda2Hs.Compile.RuntimeCheckUtils, Agda2Hs.Compile.Term, Agda2Hs.Compile.Type, Agda2Hs.Compile.TypeDefinition, diff --git a/lib/Haskell/Extra/Dec/Instances.agda b/lib/Haskell/Extra/Dec/Instances.agda new file mode 100644 index 00000000..9c016f0a --- /dev/null +++ b/lib/Haskell/Extra/Dec/Instances.agda @@ -0,0 +1,80 @@ +module Haskell.Extra.Dec.Instances where + +open import Haskell.Prelude +open import Haskell.Prim +open import Haskell.Extra.Dec +open import Haskell.Extra.Refinement + +variable + ℓ' : Level + A : Set ℓ + B : A → Set ℓ' + x : A + xs : List A + p : Bool + +instance + decIsTrue : Dec (IsTrue p) + decIsTrue {False} = False ⟨ (λ ()) ⟩ + decIsTrue {True} = True ⟨ IsTrue.itsTrue ⟩ + -- could specify transparent but this is incompatible with the instance search result + {-# COMPILE AGDA2HS decIsTrue #-} + + decIsFalse : Dec (IsFalse p) + decIsFalse {False} = True ⟨ IsFalse.itsFalse ⟩ + decIsFalse {True} = False ⟨ (λ ()) ⟩ + {-# COMPILE AGDA2HS decIsFalse #-} + + decNonEmpty : {xs : List a} → Dec (NonEmpty xs) + decNonEmpty {xs = []} = False ⟨ (λ ()) ⟩ + decNonEmpty {xs = _ ∷ _} = True ⟨ NonEmpty.itsNonEmpty ⟩ + {-# COMPILE AGDA2HS decNonEmpty #-} + +allNoHead : (B x → ⊥) → All B (x ∷ xs) → ⊥ +allNoHead ni allCons = ni it + +allNoTail : (All B xs → ⊥) → All B (x ∷ xs) → ⊥ +allNoTail np allCons = np it + +interleaved mutual + instance + -- must name these variables explicitly or Agda2Hs gets confused + decAll : ∀ {a : Set ℓ} {B : a → Set ℓ'} {xs} ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (All B xs) + + decAllTail : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {@0 xs} ⦃ @0 i : B x ⦄ → Dec (All B xs) → Dec (All B (x ∷ xs)) + decAllTail (False ⟨ p ⟩) = False ⟨ allNoTail p ⟩ + decAllTail (True ⟨ p ⟩) = True ⟨ allCons ⦃ is = p ⦄ ⟩ + + decAllHead : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {xs} → ⦃ Dec (B x) ⦄ → ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (All B (x ∷ xs)) + decAllHead ⦃ False ⟨ i ⟩ ⦄ = False ⟨ allNoHead i ⟩ + decAllHead ⦃ True ⟨ i ⟩ ⦄ = decAllTail ⦃ i = i ⦄ decAll + + decAll {_} {_} {_} {_} {[]} = True ⟨ allNil ⟩ + decAll {_} {_} {_} {_} {x ∷ xs} = decAllHead + + {-# COMPILE AGDA2HS decAll #-} + {-# COMPILE AGDA2HS decAllTail #-} + {-# COMPILE AGDA2HS decAllHead #-} + +anyNone : (B x → ⊥) → (Any B xs → ⊥) → Any B (x ∷ xs) → ⊥ +anyNone notHere _ anyHere = notHere it +anyNone _ notThere anyThere = notThere it + +interleaved mutual + instance + decAny : ∀ {a : Set ℓ} {B : a → Set ℓ'} {xs} ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (Any B xs) + + decAnyTail : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {@0 xs} (@0 i : B x → ⊥) → Dec (Any B xs) → Dec (Any B (x ∷ xs)) + decAnyTail i (False ⟨ p ⟩) = False ⟨ anyNone i p ⟩ + decAnyTail _ (True ⟨ p ⟩) = True ⟨ anyThere ⦃ is = p ⦄ ⟩ + + decAnyHead : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {xs} → ⦃ Dec (B x) ⦄ → ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (Any B (x ∷ xs)) + decAnyHead ⦃ False ⟨ i ⟩ ⦄ = decAnyTail i decAny + decAnyHead ⦃ True ⟨ i ⟩ ⦄ = True ⟨ anyHere ⦃ i = i ⦄ ⟩ + + decAny {_} {_} {_} {_} {[]} = False ⟨ (λ ()) ⟩ + decAny {_} {_} {_} {_} {x ∷ xs} = decAnyHead + + {-# COMPILE AGDA2HS decAny #-} + {-# COMPILE AGDA2HS decAnyTail #-} + {-# COMPILE AGDA2HS decAnyHead #-} diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs index da239051..ba3c3c29 100644 --- a/src/Agda2Hs/Compile.hs +++ b/src/Agda2Hs/Compile.hs @@ -3,7 +3,7 @@ module Agda2Hs.Compile where import Control.Monad.Trans.RWS.CPS ( evalRWST ) import Control.Monad.State ( gets ) import Control.Arrow ((>>>)) -import Data.Functor +import Data.Bifunctor ( Bifunctor(bimap) ) import Data.List ( isPrefixOf ) import qualified Data.Map as M @@ -15,7 +15,7 @@ import Agda.Syntax.Common.Pretty ( prettyShow ) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Monad.Signature ( isInlineFun ) import Agda.Utils.Null -import Agda.Utils.Monad ( whenM, anyM ) +import Agda.Utils.Monad ( whenM, anyM, when ) import qualified Language.Haskell.Exts.Extension as Hs @@ -24,26 +24,28 @@ import Agda2Hs.Compile.Data ( compileData ) import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma ) import Agda2Hs.Compile.Postulate ( compilePostulate ) import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma ) +import Agda2Hs.Compile.RuntimeCheckUtils ( importDec ) import Agda2Hs.Compile.Types -import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName ) +import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, tellNoErased, primModules, isClassName ) import Agda2Hs.Pragma -initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv -initCompileEnv tlm rewrites = CompileEnv +initCompileEnv :: TopLevelModuleName -> Bool -> SpecialRules -> CompileEnv +initCompileEnv tlm rtc rewrites = CompileEnv { currModule = tlm , minRecordName = Nothing , locals = [] , compilingLocal = False , copatternsEnabled = False + , rtc = rtc , rewrites = rewrites } initCompileState :: CompileState initCompileState = CompileState { lcaseUsed = 0 } -runC :: TopLevelModuleName -> SpecialRules -> C a -> TCM (a, CompileOutput) -runC tlm rewrites c = evalRWST c (initCompileEnv tlm rewrites) initCompileState +runC :: TopLevelModuleName -> Bool -> SpecialRules -> C a -> TCM (a, CompileOutput) +runC tlm rtc rewrites c = evalRWST c (initCompileEnv tlm rtc rewrites) initCompileState moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes) moduleSetup _ _ m _ = do @@ -60,20 +62,22 @@ moduleSetup _ _ m _ = do compile :: Options -> ModuleEnv -> IsMain -> Definition - -> TCM (CompiledDef, CompileOutput) -compile opts tlm _ def = + -> TCM ((CompiledDef, CompiledDef), CompileOutput) +compile opts tlm _ def = do + when rtc importDec withCurrentModule (qnameModule qname) - $ runC tlm (optRewrites opts) + $ runC tlm rtc (optRewrites opts) $ setCurrentRangeQ qname $ compileAndTag <* postCompile where qname = defName def + rtc = optRtc opts tag [] = [] tag code = [(nameBindingSite $ qnameName qname, code)] - compileAndTag :: C CompiledDef - compileAndTag = tag <$> do + compileAndTag :: C (CompiledDef, CompiledDef) + compileAndTag = bimap tag tag <$> do p <- processPragma qname reportSDoc "agda2hs.compile" 5 $ text "Compiling definition:" <+> prettyTCM qname @@ -85,24 +89,26 @@ compile opts tlm _ def = reportSDoc "agda2hs.compile" 15 $ text "Is instance?" <+> prettyTCM isInstance case (p , theDef def) of - (NoPragma , _ ) -> return [] - (ExistingClassPragma , _ ) -> return [] - (UnboxPragma s , Record{} ) -> [] <$ checkUnboxPragma def - (TransparentPragma , Function{}) -> [] <$ checkTransparentPragma def - (InlinePragma , Function{}) -> [] <$ checkInlinePragma def - - (ClassPragma ms , Record{} ) -> pure <$> compileRecord (ToClass ms) def - (NewTypePragma ds , Record{} ) -> pure <$> compileRecord (ToRecord True ds) def - (NewTypePragma ds , Datatype{}) -> compileData True ds def - (DefaultPragma ds , Datatype{}) -> compileData False ds def - (DerivePragma s , _ ) | isInstance -> pure <$> compileInstance (ToDerivation s) def - (DefaultPragma _ , Axiom{} ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def - (DefaultPragma _ , _ ) | isInstance -> pure <$> compileInstance ToDefinition def - (DefaultPragma _ , Axiom{} ) -> compilePostulate def - (DefaultPragma _ , Function{}) -> compileFun True def - (DefaultPragma ds , Record{} ) -> pure <$> compileRecord (ToRecord False ds) def - - _ -> genericDocError =<< text "Don't know how to compile" <+> prettyTCM (defName def) + (NoPragma, _) -> return ([], []) + (ExistingClassPragma, _) -> return ([], []) + (DefaultPragma _, Function {}) | not isInstance -> compileFun True def + (NewTypePragma ds, Datatype {}) -> compileData True ds def + (DefaultPragma ds, Datatype {}) -> compileData False ds def + (ClassPragma ms, Record {}) -> compileRecord (ToClass ms) def + (NewTypePragma ds, Record {}) -> compileRecord (ToRecord True ds) def + (DefaultPragma ds , Record {}) -> compileRecord (ToRecord False ds) def + -- ^ Names that may induce runtime checks + _ -> do + tellNoErased $ prettyShow $ qnameName $ defName def + (,[]) <$> case (p, theDef def) of + (UnboxPragma s , Record {} ) -> [] <$ checkUnboxPragma def + (TransparentPragma, Function {}) -> [] <$ checkTransparentPragma def + (InlinePragma , Function {}) -> [] <$ checkInlinePragma def + (DerivePragma s , _ ) | isInstance -> pure <$> compileInstance (ToDerivation s) def + (DefaultPragma _ , Axiom {} ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def + (DefaultPragma _ , _ ) | isInstance -> pure <$> compileInstance ToDefinition def + (DefaultPragma _ , Axiom {} ) -> compilePostulate def + _ -> genericDocError =<< text "Don't know how to compile" <+> prettyTCM (defName def) postCompile :: C () postCompile = whenM (gets $ lcaseUsed >>> (> 0)) $ tellExtension Hs.LambdaCase diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs index d205102d..f74a5d4d 100644 --- a/src/Agda2Hs/Compile/Data.hs +++ b/src/Agda2Hs/Compile/Data.hs @@ -1,8 +1,12 @@ module Agda2Hs.Compile.Data where -import qualified Language.Haskell.Exts.Syntax as Hs +import qualified Language.Haskell.Exts as Hs import Control.Monad ( when ) +import Data.Bifunctor ( bimap, second ) +import Data.Either ( partitionEithers ) +import Data.List ( intercalate ) +import Data.Maybe ( mapMaybe ) import Agda.Compiler.Backend import Agda.Syntax.Common import Agda.Syntax.Internal @@ -14,8 +18,10 @@ import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) +import Agda.Utils.Monad ( ifM ) -import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds ) +import Agda2Hs.Compile.RuntimeCheckUtils +import Agda2Hs.Compile.Type import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils @@ -26,9 +32,10 @@ checkNewtype name cs = do case head cs of Hs.QualConDecl () _ _ (Hs.ConDecl () cName types) -> checkNewtypeCon cName types -compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()] +compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C ([Hs.Decl ()], [Hs.Decl ()]) compileData newtyp ds def = do - let d = hsName $ prettyShow $ qnameName $ defName def + let prettyName = prettyShow $ qnameName $ defName def + d = hsName prettyName checkValidTypeName d let Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} = theDef def TelV tel t <- telViewUpTo n (defType def) @@ -37,14 +44,23 @@ compileData newtyp ds def = do let params = teleArgs tel addContext tel $ do binds <- compileTeleBinds tel - cs <- mapM (compileConstructor params) cs - let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds + chkdCs <- mapM (compileConstructor params) cs + + chks <- ifM (emitsRtc $ defName def) (do + let (noneErased, chks) = second concat $ partitionEithers $ mapMaybe snd chkdCs + -- Always export data type name + tellNoErased $ prettyName ++ "(" ++ intercalate ", " noneErased ++ ")" + return chks) + $ return [] + + let cs = map fst chkdCs + hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds let target = if newtyp then Hs.NewType () else Hs.DataType () when newtyp (checkNewtype d cs) - return [Hs.DataDecl () target Nothing hd cs ds] + return ([Hs.DataDecl () target Nothing hd cs ds], chks) where allIndicesErased :: Type -> C () allIndicesErased t = reduce (unEl t) >>= \case @@ -55,17 +71,30 @@ compileData newtyp ds def = do DomForall{} -> genericDocError =<< text "Not supported: indexed datatypes" _ -> return () -compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ()) +compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl (), +{- optional exportable cons/checker function -} Maybe (Either String [Hs.Decl ()])) compileConstructor params c = do reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c reportSDoc "agda2hs.data.con" 20 $ text " params = " <+> prettyTCM params ty <- (`piApplyM` params) . defType =<< getConstInfo c reportSDoc "agda2hs.data.con" 20 $ text " ty = " <+> prettyTCM ty TelV tel _ <- telView ty - let conName = hsName $ prettyShow $ qnameName c + let conString = prettyShow $ qnameName c + conName = hsName conString + smartQName <- smartConstructor c True + checkValidConName conName args <- compileConstructorArgs tel - return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args + chk <- ifM (emitsRtc c) (do + sig <- Hs.TypeSig () [hsName $ prettyShow $ qnameName smartQName] <$> compileType (unEl ty) + -- export constructor name when no erased, provide signature for smart constructor if it exists + checkRtc tel smartQName (hsVar conString) >>= \case + NoneErased -> return $ Just $ Left conString + Uncheckable -> return Nothing + Checkable ds -> return $ Just $ Right $ sig : ds) + $ return Nothing + + return (Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args, chk) compileConstructorArgs :: Telescope -> C [Hs.Type ()] compileConstructorArgs EmptyTel = return [] diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs index 4d9714df..78da7bb5 100644 --- a/src/Agda2Hs/Compile/Function.hs +++ b/src/Agda2Hs/Compile/Function.hs @@ -24,7 +24,7 @@ import Agda.Syntax.Scope.Monad ( isDatatypeModule ) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Substitute -import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM ) +import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM, splitTelescopeAt ) import Agda.TypeChecking.Sort ( ifIsSort ) import Agda.TypeChecking.Datatypes ( getConType, isDataOrRecord ) import Agda.TypeChecking.Records ( getDefType ) @@ -40,6 +40,7 @@ import Agda.Utils.Size ( Sized(size) ) import Agda2Hs.AgdaUtils import Agda2Hs.Compile.Name ( compileQName ) +import Agda2Hs.Compile.RuntimeCheckUtils import Agda2Hs.Compile.Term ( compileTerm, usableDom ) import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType ) import Agda2Hs.Compile.TypeDefinition ( compileTypeDef ) @@ -107,7 +108,7 @@ compileLitNatPat = \case compileFun, compileFun' :: Bool -- ^ Whether the type signature shuuld also be generated - -> Definition -> C [Hs.Decl ()] + -> Definition -> C ([Hs.Decl ()], [Hs.Decl ()]) compileFun withSig def@Defn{..} = setCurrentRangeQ defName @@ -125,7 +126,7 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do ifM (endsInSort defType) -- if the function type ends in Sort, it's a type alias! - (ensureNoLocals err >> compileTypeDef x def) + ((, []) <$> (ensureNoLocals err >> compileTypeDef x def)) -- otherwise, we have to compile clauses. $ do tel <- lookupSection m @@ -162,12 +163,22 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do =<< text "Functions defined with absurd patterns exclusively are not supported." <+> text "Use function `error` from the Haskell.Prelude instead." - return $ sig ++ [Hs.FunBind () cs] + let def = sig ++ [Hs.FunBind () cs] + chk <- ifM (emitsRtc defName) (do + typeTel <- theTel <$> telView defType + let success = hsVar $ prettyShow m ++ ".PostRtc." ++ Hs.prettyPrint x + checkRtc typeTel defName success >>= \case + NoneErased -> do tellNoErased nStr; return [] + Uncheckable -> return [] + Checkable ds -> return $ sig ++ ds) + $ return [] + return (def, chk) where Function{..} = theDef m = qnameModule defName n = qnameName defName - x = hsName $ prettyShow n + nStr = prettyShow n + x = hsName nStr err = "Not supported: type definition with `where` clauses" addPats :: [Hs.Pat ()] -> Hs.Match () -> Hs.Match () @@ -242,7 +253,7 @@ compileClause' curModule projName x ty c@Clause{..} = do let rhs = Hs.UnGuardedRhs () hsBody whereBinds | null whereDecls = Nothing - | otherwise = Just $ Hs.BDecls () (concat whereDecls) + | otherwise = Just $ Hs.BDecls () (concatMap fst whereDecls) match = case (x, ps) of (Hs.Symbol{}, p : q : ps) -> Hs.InfixMatch () p x (q : ps) rhs whereBinds _ -> Hs.Match () x ps rhs whereBinds @@ -376,13 +387,19 @@ withClauseLocals curModule c@Clause{..} k = do -- | Ensure a definition can be defined as transparent. checkTransparentPragma :: Definition -> C () -checkTransparentPragma def = compileFun False def >>= \case +checkTransparentPragma def = do + whenM (emitsRtc (defName def) <&> (&& not (checkNoneErased tele))) $ genericDocError =<< + "Cannot make function" <+> prettyTCM (defName def) <+> "transparent." <+> + "Transparent functions cannot have erased arguments with runtime checking." + compileFun False def >>= (\case [Hs.FunBind _ cls] -> mapM_ checkTransparentClause cls [Hs.TypeDecl _ hd b] -> checkTransparentTypeDef hd b - _ -> __IMPOSSIBLE__ + _ -> __IMPOSSIBLE__) . fst where + tele = theTel $ telView' $ defType def + checkTransparentClause :: Hs.Match () -> C () checkTransparentClause = \case Hs.Match _ _ [p] (Hs.UnGuardedRhs _ e) _ | patToExp p == Just e -> return () @@ -399,8 +416,12 @@ checkTransparentPragma def = compileFun False def >>= \case -- | Ensure a definition can be defined as inline. checkInlinePragma :: Definition -> C () -checkInlinePragma def@Defn{defName = f} = do +checkInlinePragma def@Defn{defName = f, defType = ty} = do let Function{funClauses = cs} = theDef def + typeTel <- theTel <$> telView ty + whenM (emitsRtc f <&> (&& not (checkNoneErased typeTel))) $ genericDocError =<< + "Cannot make function" <+> prettyTCM (defName def) <+> "inlinable." <+> + "Inline functions cannot have erased arguments with runtime checking." case filter (isJust . clauseBody) cs of [c] -> unlessM (allowedPats (namedClausePats c)) $ genericDocError =<< diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index b481e414..00fe6ec0 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -34,6 +34,7 @@ import Agda.TypeChecking.Records ( isRecordConstructor ) import qualified Agda.Utils.List1 as List1 import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM ) +import Agda.Utils.Monad ( ifM ) import Agda2Hs.AgdaUtils import Agda2Hs.Compile.Types @@ -102,9 +103,13 @@ compileQName f parent <- parentName f par <- traverse (compileName . qnameName) parent let mod0 = qnameModule $ fromMaybe f parent - mod <- compileModuleName mod0 + mod' <- compileModuleName mod0 + mod <- ifM (emitsRtc f) (case mod' of + Hs.ModuleName () s -> do + return $ Hs.ModuleName () $ s ++ ".PostRtc") + $ return mod' currMod <- hsTopLevelModuleName <$> asks currModule - let skipModule = mod == currMod + let skipModule = mod' == currMod || isJust mimpBuiltin || prettyShow mod0 `elem` primMonadModules qual <- if | skipModule -> return Unqualified diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs index a605ee92..60fb10ec 100644 --- a/src/Agda2Hs/Compile/Record.hs +++ b/src/Agda2Hs/Compile/Record.hs @@ -4,10 +4,12 @@ module Agda2Hs.Compile.Record where import Control.Monad ( unless, when ) import Control.Monad.Reader ( MonadReader(local) ) -import Data.List ( (\\), nub ) +import Data.Functor ( (<&>) ) +import Data.List ( (\\), intercalate, nub ) import Data.List.NonEmpty ( NonEmpty(..) ) import Data.Map ( Map ) import qualified Data.Map as Map +import Data.Maybe ( maybeToList ) import qualified Language.Haskell.Exts as Hs @@ -23,10 +25,12 @@ import Agda.TypeChecking.Telescope import Agda.Utils.Singleton import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) +import Agda.Utils.Monad ( ifM, whenM ) import Agda2Hs.AgdaUtils import Agda2Hs.Compile.ClassInstance import Agda2Hs.Compile.Function ( compileFun ) +import Agda2Hs.Compile.RuntimeCheckUtils import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) ) import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils @@ -50,7 +54,7 @@ compileMinRecord fieldNames m = do -- * it has an explicit dictionary argument -- * it's using the fields and definitions from the minimal record and not the parent record compiled <- withMinRecord m $ addContext (defaultDom rtype) $ compileLocal $ - fmap concat $ traverse (compileFun False) defaults + concat <$> traverse (fmap (uncurry (++)) . compileFun False) defaults let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ] return (definedFields, declMap) @@ -91,7 +95,7 @@ compileMinRecords def sls = do return ([minPragma | not (null prims)] ++ Map.elems decls) -compileRecord :: RecordTarget -> Definition -> C (Hs.Decl ()) +compileRecord :: RecordTarget -> Definition -> C ([Hs.Decl ()], [Hs.Decl ()]) compileRecord target def = do TelV tel _ <- telViewUpTo recPars (defType def) addContext tel $ do @@ -101,24 +105,41 @@ compileRecord target def = do let fieldTel = snd $ splitTelescopeAt recPars recTel case target of ToClass ms -> do - (classConstraints, classDecls) <- compileRecFields classDecl recFields fieldTel + whenM (emitsRtc (defName def) <&> (&& not (checkNoneErased fieldTel))) $ genericDocError =<< + "Cannot compile" <+> prettyTCM (defName def) <+> "to class." <+> + "Classes cannot have erased arguments with runtime checking." + (classConstraints, classDecls, _) <- compileRecFields classDecl recFields fieldTel let context = case classConstraints of [] -> Nothing [asst] -> Just (Hs.CxSingle () asst) assts -> Just (Hs.CxTuple () assts) defaultDecls <- compileMinRecords def ms - return $ Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls)) + return ([Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls))], []) ToRecord newtyp ds -> do + smartQName <- smartConstructor (defName def) False + checkValidConName cName - (constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel + (constraints, fieldDecls, fieldStrings) <- compileRecFields fieldDecl recFields fieldTel + + chk <- ifM (emitsRtc $ defName def) (do + (noneErasedCons, chk) <- checkRtc fieldTel smartQName (hsVar conString) >>= \case + NoneErased -> return ([conString], []) + Uncheckable -> return ([], []) + Checkable ds -> return ([], ds) + -- Always export record name and field names. Export constructor when it has no erased types. + tellNoErased $ rString ++ "(" ++ intercalate ", " (fieldStrings ++ noneErasedCons) ++ ")" + return chk) + $ return [] + when newtyp $ checkNewtypeCon cName fieldDecls let target = if newtyp then Hs.NewType () else Hs.DataType () - compileDataRecord constraints fieldDecls target hd ds - + (\c -> ([c], chk)) <$> compileDataRecord constraints fieldDecls target hd ds where - rName = hsName $ prettyShow $ qnameName $ defName def - cName | recNamedCon = hsName $ prettyShow $ qnameName $ conName recConHead - | otherwise = rName -- Reuse record name for constructor if no given name + rString = prettyShow $ qnameName $ defName def + rName = hsName rString + conString | recNamedCon = prettyShow $ qnameName $ conName recConHead + | otherwise = rString + cName = hsName conString -- In Haskell, projections live in the same scope as the record type, so check here that the -- record module has been opened. @@ -138,23 +159,24 @@ compileRecord target def = do fieldDecl n = Hs.FieldDecl () [n] compileRecFields :: (Hs.Name () -> Hs.Type () -> b) - -> [Dom QName] -> Telescope -> C ([Hs.Asst ()], [b]) + -> [Dom QName] -> Telescope -> C ([Hs.Asst ()], [b], [String]) compileRecFields decl ns tel = case (ns, tel) of - (_ , EmptyTel ) -> return ([], []) + (_ , EmptyTel ) -> return ([], [], []) (n:ns, ExtendTel dom tel') -> do hsDom <- compileDomType (absName tel') dom - (hsAssts, hsFields) <- underAbstraction dom tel' $ compileRecFields decl ns + (hsAssts, hsFields, fieldStrings) <- underAbstraction dom tel' $ compileRecFields decl ns case hsDom of DomType s hsA -> do - let fieldName = hsName $ prettyShow $ qnameName $ unDom n + let fieldString = prettyShow $ qnameName $ unDom n + fieldName = hsName fieldString fieldType <- addTyBang s hsA checkValidFunName fieldName - return (hsAssts, decl fieldName fieldType : hsFields) + return (hsAssts, decl fieldName fieldType : hsFields, fieldString : fieldStrings) DomConstraint hsA -> case target of - ToClass{} -> return (hsA : hsAssts , hsFields) + ToClass{} -> return (hsA : hsAssts, hsFields, fieldStrings) ToRecord{} -> genericError $ "Not supported: record/class with constraint fields" - DomDropped -> return (hsAssts , hsFields) + DomDropped -> return (hsAssts, hsFields, fieldStrings) DomForall{} -> __IMPOSSIBLE__ (_, _) -> __IMPOSSIBLE__ @@ -185,6 +207,9 @@ checkUnboxPragma def = do addContext tel $ do pars <- getContextArgs let fieldTel = recTel `apply` pars + whenM (emitsRtc (defName def) <&> (&& not (checkNoneErased fieldTel))) $ genericDocError =<< + "Cannot make record" <+> prettyTCM (defName def) <+> "unboxed." <+> + "Unboxed records cannot have erased arguments in their fields with runtime checking." fields <- nonErasedFields fieldTel unless (length fields == 1) $ genericDocError =<< "Unboxed record" <+> prettyTCM (defName def) diff --git a/src/Agda2Hs/Compile/RuntimeCheckUtils.hs b/src/Agda2Hs/Compile/RuntimeCheckUtils.hs new file mode 100644 index 00000000..0038388a --- /dev/null +++ b/src/Agda2Hs/Compile/RuntimeCheckUtils.hs @@ -0,0 +1,234 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Agda2Hs.Compile.RuntimeCheckUtils (emitsRtc, importDec, checkNoneErased, smartConstructor, RtcResult (..), checkRtc) where + +import Agda.Syntax.Common +import Agda.Syntax.Common.Pretty (prettyShow) +import qualified Agda.Syntax.Concrete as AC +import Agda.Syntax.Concrete.Definitions (niceDeclarations) +import Agda.Syntax.Concrete.Definitions.Monad (NiceEnv (NiceEnv), runNice) +import qualified Agda.Syntax.Concrete.Name as AN +import Agda.Syntax.Internal +import Agda.Syntax.Position (noRange) +import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract)) +import Agda.TypeChecking.InstanceArguments (findInstance) +import Agda.TypeChecking.MetaVars (newInstanceMeta, newLevelMeta) +import Agda.TypeChecking.Monad +import Agda.TypeChecking.Pretty (PrettyTCM (prettyTCM), (<+>)) +import Agda.TypeChecking.Reduce (instantiate) +import Agda.TypeChecking.Substitute (telView', theTel) +import Agda.TypeChecking.Telescope (splitTelescopeAt) +import Agda.Utils.Impossible (__IMPOSSIBLE__) +import qualified Agda.Utils.List1 as List1 +import Agda.Utils.Monad (unless) +import Agda.Utils.Tuple (uncurry4) +import Agda2Hs.Compile.Term (compileTerm) +import Agda2Hs.Compile.Types (C, rtc) +import Agda2Hs.Compile.Utils +import Agda2Hs.HsUtils +import Control.Monad.Except (catchError) +import Control.Monad.Reader (asks) +import Data.List (intersect, partition, zip4) +import Data.Map (empty) +import Data.Maybe (catMaybes, isJust) +import qualified Language.Haskell.Exts as Hs + +-- Import Haskell.Extra.Dec{,.Instances} +importDec :: TCM () +importDec = do + let haskellExtra = AN.Qual (AC.simpleName "Haskell") . AN.Qual (AC.simpleName "Extra") + directives = ImportDirective noRange UseEverything [] [] Nothing + importDecl q = [AC.Import noRange (haskellExtra q) Nothing AC.DontOpen directives] + run ds = case fst $ runNice (NiceEnv True) $ niceDeclarations empty $ importDecl ds of + Left _ -> __IMPOSSIBLE__ + Right ds -> toAbstract ds + run $ AC.QName $ AC.simpleName "Dec" + run $ AN.Qual (AC.simpleName "Dec") $ AC.QName $ AC.simpleName "Instances" + return () + +-- Retrieve constructor name and generated smart constructor qname. +-- Takes extra argument whether one additional name should be stripped +smartConstructor :: QName -> Bool -> C QName +smartConstructor qname strip1 = do + checkNameConflict smartString + return smartQName + where + qnameList = qnameToList qname + -- e.g. data types need the name of the data type itself stripped + strip = if strip1 then 2 else 1 + qualifier = List1.take (length qnameList - strip) qnameList + name = List1.last qnameList + smartString = "sc" ++ prettyShow name + smartName = mkName (nameBindingSite name) (nameId name) smartString + smartQName = qnameFromList $ List1.prependList qualifier $ smartName List1.:| [] + +-- Runtime checks are not supported for certain pragmas. Check that none are erased. +checkNoneErased :: Telescope -> Bool +checkNoneErased tel = null topLevelErased && all (checkNoneErased . snd) other + where + doms = telToList tel + (topLevelErased, other) = partition (uncurry checkTopLevelErased) $ zip doms $ telify doms + +-- External runtime check result +data RtcResult + = NoneErased + | Uncheckable + | Checkable [Hs.Decl ()] + +-- Internal runtime check result +data RtcResult' + = NoneErased' + | Uncheckable' + | -- The actual runtime check is assembled in the caller receiving an RtcResult', + -- because the logic at the top level is different, e.g. the declarations are + -- put in a `where` instead of being flattened. + Checkable' + { theirLhs :: [Hs.Pat ()], + theirChks :: [Hs.Exp ()], + theirRhs :: [Hs.Exp ()], + theirDecls :: [Hs.Decl ()] + } + +-- Check name induces no conflict +checkNameConflict :: String -> C () +checkNameConflict s = + testResolveStringName s >>= \case + Just _ -> errorNameConflict s + Nothing -> return () + +errorNameConflict :: String -> C () +errorNameConflict s = + genericDocError + =<< ("Illegal name" <+> prettyTCM s) + <> ", conflicts with name generated for runtime checks." + +-- Create runtime check. +-- Takes function name, lhs patterns, expressions for checks, expression on success, and optionally `where` binds +createRtc :: Hs.Name () -> [Hs.Pat ()] -> [Hs.Exp ()] -> Hs.Exp () -> Maybe (Hs.Binds ()) -> Hs.Decl () +createRtc n args [] success = createRtc' n args $ Hs.UnGuardedRhs () success +createRtc n args chks success = + createRtc' n args rhs + where + rhs = Hs.GuardedRhss () $ Hs.GuardedRhs () [Hs.Qualifier () andChks] success : errChks + andChks = foldr1 (\c -> Hs.InfixApp () c $ Hs.QVarOp () $ Hs.UnQual () $ Hs.Symbol () "&&") chks + errChks = + map + ( \chk -> + let msg = "Runtime check failed: " ++ Hs.prettyPrint chk + hsErr = Hs.App () (hsVar "error") $ Hs.Lit () $ Hs.String () msg msg + in Hs.GuardedRhs () [Hs.Qualifier () $ Hs.App () (hsVar "not") chk] hsErr + ) + chks + +createRtc' :: Hs.Name () -> [Hs.Pat ()] -> Hs.Rhs () -> Maybe (Hs.Binds ()) -> Hs.Decl () +createRtc' n args rhs binds = Hs.FunBind () [Hs.Match () n args rhs binds] + +-- Creates a runtime check if necessary and possible, informing C accordingly. +-- Takes telescope of type to check, name, and expression on success. +checkRtc :: Telescope -> QName -> Hs.Exp () -> C RtcResult +checkRtc tel name success = + checkRtc' tel "go" "a" >>= \case + NoneErased' -> return NoneErased + Uncheckable' -> return Uncheckable + Checkable' {..} -> do + tellAllCheckable name + let rhs = eApp success theirRhs + chkName = hsName $ prettyShow $ qnameName name + binds = if null theirDecls then Nothing else Just $ Hs.BDecls () theirDecls + chk = createRtc chkName theirLhs theirChks rhs binds + return $ Checkable [chk] + +-- Recursively check for runtime checkability in nested types. +-- Takes telescope of type to check, prefix for `go` function to create, and prefix for `a` argument to create. +checkRtc' :: Telescope -> String -> String -> C RtcResult' +checkRtc' tel goPrefix argPrefix = do + ourChks <- mapM (\(d, tUpTo, _, _) -> createGuardExp d tUpTo) topLevelErased + belows <- mapM (uncurry4 recurse) call + if all isJust belows && all isJust ourChks + then + let (theirLhs, theirRhs, decls) = unzip3 $ catMaybes belows + theirDecls = concat decls + theirChks = catMaybes ourChks + in if null theirDecls && null ourChks + then return NoneErased' + else do + return Checkable' {..} + else return Uncheckable' + where + -- Execute recursion. + -- Takes domain of type to consider for naming, telescope up to that point for context, + -- telescope at that point for recursing, and index of that type for unique names. + -- The third can be gathered from the first, but is computed earlier for other purposes. + -- If checkable, returns lhs and rhs at that point plus declarations from checks below. + recurse :: Dom (ArgName, a) -> Telescope -> Telescope -> Int -> C (Maybe (Hs.Pat (), Hs.Exp (), [Hs.Decl ()])) + recurse d tUpTo tAt i = do + let arg = nameArg d $ argPrefix ++ show i + goP = goPrefix ++ show i + ourLhs = hsPat arg + up = "up" + rtc <- addContext tUpTo $ checkRtc' tAt (goP ++ "_") $ argPrefix ++ show i ++ "_" + case rtc of + NoneErased' -> return $ Just (ourLhs, hsVar arg, []) + Uncheckable' -> return Nothing + Checkable' {..} -> do + let tAtNames = map (fst . unDom) $ telToList tAt + conflicts = tAtNames `intersect` [goP, arg, up] + unless (null conflicts) $ errorNameConflict $ head conflicts + let rhs = hsVar up `eApp` theirRhs + maybeRtc = createRtc (hsName goP) (hsPat up : theirLhs) theirChks rhs Nothing + (ourRhs, ourRtc) = + if null theirChks + then -- inline if nothing to check at this level + (Hs.Lambda () theirLhs $ hsVar arg `eApp` theirRhs, []) + else (hsVar goP `eApp` [hsVar arg], [maybeRtc]) + return $ Just (ourLhs, ourRhs, ourRtc ++ theirDecls) + + doms = telToList tel + rng = [0 .. length doms] + telsUpTo = map (\i -> fst $ splitTelescopeAt i tel) rng + bigZip = zip4 doms telsUpTo (telify doms) rng + -- Partition out arguments that are erased and at top level (those we will attempt to check) + (topLevelErased, call) = partition (\(d, _, tAt, _) -> checkTopLevelErased d tAt) bigZip + +---- Small single-mention convenience functions + +-- Gather telescopes from domains +telify :: [Dom' t (a, Type)] -> [Telescope] +telify = map $ theTel . telView' . snd . unDom + +-- Check a type is erased and at top level; in this case, it should be checked. +-- The latter information can be gathered from the former, but this simplifies the type. +checkTopLevelErased :: Dom a -> Telescope -> Bool +checkTopLevelErased dom telAt = case getQuantity dom of + Quantity0 _ -> null $ telToList telAt + _ -> False + +-- Replace unnamed arguments with default +nameArg :: Dom (ArgName, a) -> String -> String +nameArg d def = let name = fst $ unDom d in if name == "_" then def else name + +-- Turn a type into its Dec version +decify :: Type -> C Type +decify t = do + dec <- resolveStringName "Haskell.Extra.Dec.Dec" + level <- liftTCM newLevelMeta + let vArg = defaultArg + hArg = setHiding Hidden . vArg + return $ t {unEl = Def dec $ map Apply [hArg $ Level level, vArg $ unEl t]} + +-- Failably find instances for decidable terms +findDecInstances :: Type -> C (Maybe Term) +findDecInstances t = + liftTCM $ + do + (m, v) <- newInstanceMeta "" t + findInstance m Nothing + Just <$> instantiate v + `catchError` const (return Nothing) + +-- Create expression to be put in the guard +createGuardExp :: Dom' t (a, Type) -> Telescope -> C (Maybe (Hs.Exp ())) +createGuardExp dom telUpTo = + addContext (setHiding Hidden <$> telUpTo) $ do + dec <- decify $ snd $ unDom dom + findDecInstances dec >>= traverse (compileTerm dec) diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 587dd7a9..d07e3f85 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -62,6 +62,7 @@ data Options = Options , optOutDir :: Maybe FilePath , optConfigFile :: Maybe FilePath , optExtensions :: [Hs.Extension] + , optRtc :: Bool , optRewrites :: SpecialRules , optPrelude :: PreludeOptions } @@ -84,6 +85,8 @@ data CompileEnv = CompileEnv -- ^ whether we are currently compiling a where clause or pattern-matching lambda , copatternsEnabled :: Bool -- ^ whether copatterns should be allowed when compiling patterns + , rtc :: Bool + -- ^ whether runtime checks should be emitted (uncheckable names are wrapped away) , rewrites :: SpecialRules -- ^ Special compilation rules. } @@ -119,14 +122,18 @@ data CompileOutput = CompileOutput -- ^ Haskell import statements. , haskellExtensions :: [Hs.KnownExtension] -- ^ Required language extensions. + , noErased :: [String] + -- ^ Names that can be exported as is wrt runtime checks because they have no erased arguments + , allCheckable :: [QName] + -- ^ Names that can be exported wrt runtime checks because all erased arguments are checkable } instance Semigroup CompileOutput where - CompileOutput imps exts <> CompileOutput imps' exts' = - CompileOutput (imps <> imps') (exts <> exts') + CompileOutput imps exts ers checks <> CompileOutput imps' exts' ers' checks' = + CompileOutput (imps <> imps') (exts <> exts') (ers <> ers') (checks <> checks') instance Monoid CompileOutput where - mempty = CompileOutput mempty mempty + mempty = CompileOutput mempty mempty mempty mempty -- | State used while compiling a single module. newtype CompileState = CompileState diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index 4d712a34..abe8f0a8 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -7,6 +7,7 @@ import Control.Monad.Reader import Control.Monad.Writer ( tell ) import Control.Monad.State ( put, modify ) +import Data.Bifunctor ( Bifunctor(bimap) ) import Data.Maybe ( isJust ) import qualified Data.Map as M @@ -281,10 +282,16 @@ checkValidConName x = unless (validConName x) $ genericDocError =<< do text "Invalid name for Haskell constructor: " <+> text (Hs.prettyPrint x) tellImport :: Import -> C () -tellImport imp = tell $ CompileOutput [imp] [] +tellImport imp = tell $ CompileOutput [imp] [] [] [] tellExtension :: Hs.KnownExtension -> C () -tellExtension pr = tell $ CompileOutput [] [pr] +tellExtension pr = tell $ CompileOutput [] [pr] [] [] + +tellNoErased :: String -> C () +tellNoErased er = tell $ CompileOutput [] [] [er] [] + +tellAllCheckable :: QName -> C () +tellAllCheckable chk = tell $ CompileOutput [] [] [] [chk] addPatBang :: Strictness -> Hs.Pat () -> C (Hs.Pat ()) addPatBang Strict p = tellExtension Hs.BangPatterns >> @@ -312,7 +319,7 @@ checkFixityLevel name (Related lvl) = <+> text "for operator" <+> prettyTCM name else pure (Just (round lvl)) -maybePrependFixity :: QName -> Fixity -> C [Hs.Decl ()] -> C [Hs.Decl ()] +maybePrependFixity :: QName -> Fixity -> C ([Hs.Decl ()], [Hs.Decl ()]) -> C ([Hs.Decl ()], [Hs.Decl ()]) maybePrependFixity n f comp | f /= noFixity = do hsLvl <- checkFixityLevel n (fixityLevel f) let x = hsName $ prettyShow $ qnameName n @@ -320,7 +327,8 @@ maybePrependFixity n f comp | f /= noFixity = do NonAssoc -> Hs.AssocNone () LeftAssoc -> Hs.AssocLeft () RightAssoc -> Hs.AssocRight () - (Hs.InfixDecl () hsAssoc hsLvl [Hs.VarOp () x]:) <$> comp + let head = (Hs.InfixDecl () hsAssoc hsLvl [Hs.VarOp () x]:) + bimap head head <$> comp maybePrependFixity n f comp = comp @@ -354,3 +362,12 @@ resolveStringName :: String -> C QName resolveStringName s = do testResolveStringName s >>= \case Just aname -> return aname + Nothing -> genericDocError =<< text ("Couldn't find " ++ s) + +-- Check if runtime checks should be emitted, i.e. the feature is +-- enabled and the name is not in the trusted computing base. +-- This is not included in RuntimeCheckUtils for dependency reasons. +emitsRtc :: QName -> C Bool +emitsRtc qname = do + topName <- prettyTCM $ head $ mnameToList $ qnameModule qname + asks $ (show topName `notElem` ["Haskell", "Agda"] &&) . rtc diff --git a/src/Agda2Hs/HsUtils.hs b/src/Agda2Hs/HsUtils.hs index 1c4efae0..63717b7b 100644 --- a/src/Agda2Hs/HsUtils.hs +++ b/src/Agda2Hs/HsUtils.hs @@ -76,6 +76,9 @@ extToName = Ident () . show hsModuleName :: String -> ModuleName () hsModuleName = ModuleName () +hsPat :: String -> Pat () +hsPat = PVar () . hsName + isOp :: QName () -> Bool isOp (UnQual _ Symbol{}) = True isOp (Special _ Cons{}) = True diff --git a/src/Agda2Hs/Render.hs b/src/Agda2Hs/Render.hs index 4cd979d2..8bf6eace 100644 --- a/src/Agda2Hs/Render.hs +++ b/src/Agda2Hs/Render.hs @@ -1,15 +1,17 @@ +{-# LANGUAGE OverloadedStrings #-} + module Agda2Hs.Render where -import Control.Monad ( unless ) +import Control.Monad ( when, unless ) import Control.Monad.IO.Class ( MonadIO(liftIO) ) import Data.Function ( on ) -import Data.List ( sortBy, nub ) +import Data.List ( intercalate, sortBy, nub ) import Data.Maybe ( fromMaybe, isNothing ) import Data.Set ( Set ) import qualified Data.Set as Set -import System.FilePath ( takeDirectory, () ) +import System.FilePath ( takeDirectory, takeBaseName, joinPath, () ) import System.Directory ( createDirectoryIfMissing ) import qualified Language.Haskell.Exts.SrcLoc as Hs @@ -28,6 +30,7 @@ import Agda.Syntax.TopLevelModuleName import Agda.Syntax.Common.Pretty ( prettyShow ) import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) +import qualified Agda.Utils.List1 as List1 import Agda2Hs.Compile import Agda2Hs.Compile.Types @@ -128,21 +131,25 @@ prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) = (Hs.Ident _ _) -> rest writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName - -> [(CompiledDef, CompileOutput)] -> TCM ModuleRes + -> [((CompiledDef, CompiledDef), CompileOutput)] -> TCM ModuleRes writeModule opts _ isMain m outs = do code <- getForeignPragmas (optExtensions opts) - let mod = prettyShow m - (cdefs, impss, extss) = unzip3 $ flip map outs $ - \(cdef, CompileOutput imps exts) -> (cdef, imps, exts) - defs = concatMap defBlock cdefs ++ codeBlocks code - imps = concat impss - exts = concat extss + let mod = prettyShow m + defs = concatMap (defBlock . fst . fst) outs ++ codeBlocks code + chkdefs = concatMap (defBlock . snd . fst) outs + output = map snd outs + imps = concatMap imports output + exts = concatMap haskellExtensions output + safe = concatMap noErased output + chkd = map prettyShow $ concatMap allCheckable output unless (null code && null defs && isMain == NotMain) $ do let unlines' [] = [] unlines' ss = unlines ss ++ "\n" let preOpts@PreludeOpts{..} = optPrelude opts + nameParts = List1.toList $ rawModuleNameParts $ rawTopLevelModuleName m + rtc = optRtc opts && head nameParts `notElem` ["Agda", "Haskell"] -- if the prelude is supposed to be implicit, -- or the prelude imports have been fixed in the config file, @@ -163,15 +170,28 @@ writeModule opts _ isMain m outs = do -- The comments make it hard to generate and pretty print a full module hsFile <- moduleFileName opts m - - let output = concat + when (rtc && "PostRtc" `elem` nameParts) $ do + genericDocError =<< ("Illegal module name" <+> prettyTCM m) + <> ", conflicts with name generated for runtime checks." + let postFile = joinPath [takeDirectory hsFile, takeBaseName hsFile, "PostRtc.hs"] + renderedExps = intercalate ", " $ safe ++ chkd + + let preOutput = concat + [ "module " ++ mod ++ " (" ++ renderedExps ++ ") where\n\n" + , autoImports + , "import " ++ mod ++ ".PostRtc\n\n" + , renderBlocks chkdefs + ] + output = concat [ renderLangExts exts , renderBlocks $ codePragmas code - , "module " ++ mod ++ " where\n\n" + , "module " ++ mod ++ (if rtc then ".PostRtc" else "") ++ " where\n\n" , autoImports , renderBlocks defs ] reportSLn "" 1 $ "Writing " ++ hsFile - - liftIO $ ensureDirectory hsFile >> writeFile hsFile output + liftIO $ ensureDirectory hsFile >> writeFile hsFile (if rtc then preOutput else output) + when rtc $ do + reportSLn "" 1 $ "Writing " ++ postFile + liftIO $ ensureDirectory postFile >> writeFile postFile output diff --git a/src/Main.hs b/src/Main.hs index 59acf948..bf559c26 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -31,6 +31,7 @@ defaultOptions = Options , optOutDir = Nothing , optConfigFile = Nothing , optExtensions = [] + , optRtc = False , optPrelude = PreludeOpts False Nothing [] -- by default the Prelude is imported explicitly , optRewrites = defaultSpecialRules @@ -49,8 +50,11 @@ configOpt src opts = return opts { optConfigFile = Just src } extensionOpt :: String -> Flag Options extensionOpt ext opts = return opts { optExtensions = Hs.parseExtension ext : optExtensions opts } +rtcOpt :: Flag Options +rtcOpt opts = return opts { optRtc = True } -backend :: Backend' Options Options ModuleEnv ModuleRes (CompiledDef, CompileOutput) + +backend :: Backend' Options Options ModuleEnv ModuleRes ((CompiledDef, CompiledDef), CompileOutput) backend = Backend' { backendName = "agda2hs" , backendVersion = Just (showVersion version) @@ -64,6 +68,9 @@ backend = Backend' "Write Haskell code to DIR. (default: project root)" , Option ['X'] [] (ReqArg extensionOpt "EXTENSION") "Enable Haskell language EXTENSION. Affects parsing of Haskell code in FOREIGN blocks." + , Option [] ["runtime-check"] (NoArg rtcOpt) + "Enable runtime checking of erased arguments. \ + \Hides constructs with undecidable erased arguments away." , Option [] ["config"] (ReqArg configOpt "FILE") "Provide additional configuration to agda2hs with a YAML file." ] diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda index dc67796b..32a2fb40 100644 --- a/test/AllFailTests.agda +++ b/test/AllFailTests.agda @@ -1,6 +1,8 @@ {-# OPTIONS --guardedness #-} module AllFailTests where +import AllRuntimeCheckFailTests + import Fail.ClashingImport import Fail.Issue142 import Fail.MatchOnDelay diff --git a/test/AllRuntimeCheckFailTests.agda b/test/AllRuntimeCheckFailTests.agda new file mode 100644 index 00000000..8ede18e7 --- /dev/null +++ b/test/AllRuntimeCheckFailTests.agda @@ -0,0 +1,5 @@ +module AllRuntimeCheckFailTests where + +import Fail.RuntimeCheckClass +import Fail.RuntimeCheckInline +import Fail.PostRtc.RuntimeCheckModuleName diff --git a/test/AllRuntimeCheckTests.agda b/test/AllRuntimeCheckTests.agda new file mode 100644 index 00000000..a27965d0 --- /dev/null +++ b/test/AllRuntimeCheckTests.agda @@ -0,0 +1,4 @@ +module AllRuntimeCheckTests where + +import RuntimeCheckCallFeatures +import RuntimeCheckUseCases diff --git a/test/AllTests.agda b/test/AllTests.agda index c1a58587..0aa24b1e 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -161,4 +161,7 @@ import Issue145 import Issue264 import Issue301 import Issue305 + +import RuntimeCheckCallFeatures +import RuntimeCheckUseCases #-} diff --git a/test/Fail/PostRtc.agda b/test/Fail/PostRtc.agda new file mode 100644 index 00000000..9e0b48f9 --- /dev/null +++ b/test/Fail/PostRtc.agda @@ -0,0 +1,2 @@ +-- is an illegal module name in runtime checking +module Fail.PostRtc where diff --git a/test/Fail/RuntimeCheckArg.agda b/test/Fail/RuntimeCheckArg.agda new file mode 100644 index 00000000..7d45ac18 --- /dev/null +++ b/test/Fail/RuntimeCheckArg.agda @@ -0,0 +1,7 @@ +module Fail.RuntimeCheckArg where + +open import Haskell.Prelude + +conflict : (Nat → (a0 : Nat) ⦃@0 _ : IsTrue (a0 > 0)⦄ → Nat) → Nat +conflict _ = 0 +{-# COMPILE AGDA2HS conflict #-} diff --git a/test/Fail/RuntimeCheckClass.agda b/test/Fail/RuntimeCheckClass.agda new file mode 100644 index 00000000..2b299cb0 --- /dev/null +++ b/test/Fail/RuntimeCheckClass.agda @@ -0,0 +1,16 @@ +module Fail.RuntimeCheckClass where + +open import Haskell.Prelude + +record Class : Set where + field + theField : Nat +open Class public +{-# COMPILE AGDA2HS Class class #-} + +record NoClass : Set where + field + classFst : Nat + classSnd : ⦃@0 _ : IsTrue (classFst > 0)⦄ → Nat +open NoClass public +{-# COMPILE AGDA2HS NoClass class #-} diff --git a/test/Fail/RuntimeCheckGo.agda b/test/Fail/RuntimeCheckGo.agda new file mode 100644 index 00000000..23b988c8 --- /dev/null +++ b/test/Fail/RuntimeCheckGo.agda @@ -0,0 +1,7 @@ +module Fail.RuntimeCheckGo where + +open import Haskell.Prelude + +conflict : ((go0 : Nat) ⦃@0 _ : IsTrue (go0 > 0)⦄ → Nat) → Nat +conflict _ = 0 +{-# COMPILE AGDA2HS conflict #-} diff --git a/test/Fail/RuntimeCheckInline.agda b/test/Fail/RuntimeCheckInline.agda new file mode 100644 index 00000000..112bf373 --- /dev/null +++ b/test/Fail/RuntimeCheckInline.agda @@ -0,0 +1,11 @@ +module Fail.RuntimeCheckInline where + +open import Haskell.Prelude + +inlinable : Nat +inlinable = 0 +{-# COMPILE AGDA2HS inlinable inline #-} + +notInlinable : (x : Nat) → ⦃@0 _ : IsTrue (x > 0)⦄ → Nat +notInlinable _ = 0 +{-# COMPILE AGDA2HS notInlinable inline #-} diff --git a/test/Fail/RuntimeCheckSc.agda b/test/Fail/RuntimeCheckSc.agda new file mode 100644 index 00000000..c76a77b0 --- /dev/null +++ b/test/Fail/RuntimeCheckSc.agda @@ -0,0 +1,11 @@ +module Fail.RuntimeCheckSc where + +open import Haskell.Prelude + +data Dat : Set where + Conflict : ((x : Nat) ⦃@0 _ : IsTrue (x > 0)⦄ → Nat) → Dat +{-# COMPILE AGDA2HS Dat #-} + +scConflict : Nat +scConflict = 0 +{-# COMPILE AGDA2HS scConflict #-} diff --git a/test/Fail/RuntimeCheckTransparent.agda b/test/Fail/RuntimeCheckTransparent.agda new file mode 100644 index 00000000..cceb3574 --- /dev/null +++ b/test/Fail/RuntimeCheckTransparent.agda @@ -0,0 +1,11 @@ +module Fail.RuntimeCheckTransparent where + +open import Haskell.Prelude + +transparent : Nat → Nat +transparent n = n +{-# COMPILE AGDA2HS transparent transparent #-} + +noTransparent : (x : Nat) → ⦃@0 _ : IsTrue (x > 0)⦄ → Nat +noTransparent n = n +{-# COMPILE AGDA2HS noTransparent transparent #-} diff --git a/test/Fail/RuntimeCheckUnboxed.agda b/test/Fail/RuntimeCheckUnboxed.agda new file mode 100644 index 00000000..53272ab1 --- /dev/null +++ b/test/Fail/RuntimeCheckUnboxed.agda @@ -0,0 +1,11 @@ +module Fail.RuntimeCheckUnboxed where + +open import Haskell.Prelude + +record Unboxable : Set where + field unboxField : Nat +{-# COMPILE AGDA2HS Unboxable unboxed #-} + +record NoUnboxable : Set where + field noUnboxField : (@0 _ : IsTrue Bool.true) → Nat +{-# COMPILE AGDA2HS NoUnboxable unboxed #-} diff --git a/test/Fail/RuntimeCheckUp.agda b/test/Fail/RuntimeCheckUp.agda new file mode 100644 index 00000000..37b5450f --- /dev/null +++ b/test/Fail/RuntimeCheckUp.agda @@ -0,0 +1,7 @@ +module Fail.RuntimeCheckUp where + +open import Haskell.Prelude + +conflict : ((up : Nat) ⦃@0 _ : IsTrue (up > 0)⦄ → Nat) → Nat +conflict _ = 0 +{-# COMPILE AGDA2HS conflict #-} diff --git a/test/Makefile b/test/Makefile index d3868cd8..92b34b0a 100644 --- a/test/Makefile +++ b/test/Makefile @@ -2,6 +2,7 @@ AGDA2HS=./agda2hs +RTS -M2G -RTS ROOT=$(shell cd ..; pwd)/ MAIN=AllTests FAIL_MAIN=AllFailTests +MAIN_RTC=AllRuntimeCheckTests .PHONY : default allTests print-fail fail compare golden \ html renderTranslations clean force-recompile @@ -10,11 +11,12 @@ default : compare build/%.hs : %.agda *.agda Fail/*.agda Cubical/*.agda @echo == Compiling tests == - $(AGDA2HS) $< -o build + (rtc=$$(echo $< | grep RuntimeCheck); $(AGDA2HS) $${rtc:+--runtime-check} $< -o build) -allTests : build/$(MAIN).hs +allTests : build/$(MAIN).hs build/$(MAIN_RTC).hs @echo == Running ghc == - @(cd build && ghc -fno-code $(MAIN).hs) + @(cd build && ghc -fno-code $(MAIN).hs && \ + ghc -fno-code $(rtc) $(MAIN_RTC).hs) print-fail : @echo == Failing tests == @@ -23,14 +25,17 @@ fail : print-fail $(patsubst Fail/%.agda,build/%.err,$(wildcard Fail/*.agda)) build/%.err : Fail/%.agda force-recompile @echo Compiling $< - @($(AGDA2HS) $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@ + @(rtc=$$(echo $< | grep -E '(RuntimeCheck|PostRtc)'); $(AGDA2HS) $${rtc:+--runtime-check} $< -o build -v0 \ + && echo "UNEXPECTED SUCCESS" || true) \ + | sed -e 's:'$(ROOT)'::g' > $@ compare : allTests fail @echo == Comparing output == + @cp -r build/Haskell golden @diff -r build golden golden : - @cp build/*.hs build/Cubical/*.hs build/*.err golden + @cp -r build/* golden html : allTests fail html/index.html html/fail/index.html renderTranslations diff --git a/test/RuntimeCheckCallFeatures.agda b/test/RuntimeCheckCallFeatures.agda new file mode 100644 index 00000000..00834a38 --- /dev/null +++ b/test/RuntimeCheckCallFeatures.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --sized-types #-} + +module RuntimeCheckCallFeatures where + +open import Haskell.Prelude +open import RuntimeCheckFeatures + +externalFunCaller : Nat +externalFunCaller = simpleFun 1 +{-# COMPILE AGDA2HS externalFunCaller #-} diff --git a/test/RuntimeCheckFeatures.agda b/test/RuntimeCheckFeatures.agda new file mode 100644 index 00000000..47f99271 --- /dev/null +++ b/test/RuntimeCheckFeatures.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --sized-types #-} +module RuntimeCheckFeatures where + +open import Haskell.Prelude +open import Haskell.Extra.Delay + +noneErasedFun : Nat → Nat +noneErasedFun _ = 1 +{-# COMPILE AGDA2HS noneErasedFun #-} + +noDecInstance : (x : Nat) ⦃@0 _ : HasResult x (now x)⦄ → Nat +noDecInstance _ = 0 +{-# COMPILE AGDA2HS noDecInstance #-} + +simpleFun : (x : Nat) ⦃@0 _ : IsTrue (x > 0)⦄ → Nat +simpleFun _ = 0 +{-# COMPILE AGDA2HS simpleFun #-} + +simpleFunCaller : Nat +simpleFunCaller = simpleFun 1 +{-# COMPILE AGDA2HS simpleFunCaller #-} + +fun : (x : Nat) → ((y : Nat) ⦃@0 _ : IsTrue (y > x)⦄ ⦃@0 _ : IsTrue (y < 5)⦄ → Nat) → Nat +fun _ _ = 0 +{-# COMPILE AGDA2HS fun #-} + +-- If you want to deconstruct in Haskell, you have to write deconstructors in Agda. +-- Making the constructor available would enable bypassing the smart constructor. +data Dat : Set where + Con : (((x : Nat) ⦃@0 _ : IsTrue (x > 0)⦄ → Nat) → Nat) → Dat + NoneErasedCon : Nat → Dat +{-# COMPILE AGDA2HS Dat #-} + +-- Term variables in type parameter not supported, so not showcased here +record Rec : Set where + field + recFst : Nat + recSnd : (⦃@0 _ : IsTrue (recFst > 0)⦄ → Nat) → (⦃@0 _ : IsTrue (recFst < 5)⦄ → Nat) → Nat +open Rec public +{-# COMPILE AGDA2HS Rec #-} + +zeroLtSuc : (a : Nat) → IsTrue (0 < (a + 1)) +zeroLtSuc zero = IsTrue.itsTrue +zeroLtSuc (suc _) = IsTrue.itsTrue + +record Newt : Set where + field + theField : (f : ((x : Nat) ⦃ @0 _ : IsTrue (x > 0) ⦄ → Nat)) → (y : Nat) → ⦃ @0 _ : IsTrue (f (y + 1) ⦃ zeroLtSuc y ⦄ > 0) ⦄ → Nat +open Newt public +{-# COMPILE AGDA2HS Newt newtype #-} + +record NoneErasedNewt : Set where + field + noneErasedField : Nat +open NoneErasedNewt public +{-# COMPILE AGDA2HS NoneErasedNewt newtype #-} diff --git a/test/RuntimeCheckUseCases.agda b/test/RuntimeCheckUseCases.agda new file mode 100644 index 00000000..fb8ced35 --- /dev/null +++ b/test/RuntimeCheckUseCases.agda @@ -0,0 +1,13 @@ +module RuntimeCheckUseCases where + +open import Haskell.Prelude +open import Haskell.Extra.Dec +open import Haskell.Extra.Dec.Instances + +subtractFromGreater : (x y : Nat) ⦃@0 _ : IsFalse (x < y)⦄ → Nat +subtractFromGreater x y = x - y +{-# COMPILE AGDA2HS subtractFromGreater #-} + +headOfNonEmpty : (xs : List Nat) ⦃@0 _ : NonEmpty xs ⦄ → Nat +headOfNonEmpty (x ∷ _) = x +{-# COMPILE AGDA2HS headOfNonEmpty #-} diff --git a/test/golden/AllRuntimeCheckTests.hs b/test/golden/AllRuntimeCheckTests.hs new file mode 100644 index 00000000..7973c927 --- /dev/null +++ b/test/golden/AllRuntimeCheckTests.hs @@ -0,0 +1,4 @@ +module AllRuntimeCheckTests () where + +import AllRuntimeCheckTests.PostRtc + diff --git a/test/golden/AllRuntimeCheckTests/PostRtc.hs b/test/golden/AllRuntimeCheckTests/PostRtc.hs new file mode 100644 index 00000000..e5c33b35 --- /dev/null +++ b/test/golden/AllRuntimeCheckTests/PostRtc.hs @@ -0,0 +1,2 @@ +module AllRuntimeCheckTests.PostRtc where + diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 51ab5ba2..4909d2ee 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -78,3 +78,6 @@ import Issue264 import Issue301 import Issue305 +import RuntimeCheckCallFeatures +import RuntimeCheckUseCases + diff --git a/test/golden/PostRtc.err b/test/golden/PostRtc.err new file mode 100644 index 00000000..701f8dc3 --- /dev/null +++ b/test/golden/PostRtc.err @@ -0,0 +1 @@ +Illegal module name Fail.PostRtc, conflicts with name generated for runtime checks. diff --git a/test/golden/RuntimeCheckArg.err b/test/golden/RuntimeCheckArg.err new file mode 100644 index 00000000..9feba217 --- /dev/null +++ b/test/golden/RuntimeCheckArg.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckArg.agda:5,1-9 +Illegal name a0, conflicts with name generated for runtime checks. diff --git a/test/golden/RuntimeCheckCallFeatures.hs b/test/golden/RuntimeCheckCallFeatures.hs new file mode 100644 index 00000000..6e2cc9bb --- /dev/null +++ b/test/golden/RuntimeCheckCallFeatures.hs @@ -0,0 +1,7 @@ +module RuntimeCheckCallFeatures (externalFunCaller) where + +import Numeric.Natural (Natural) +import RuntimeCheckFeatures.PostRtc (simpleFun) + +import RuntimeCheckCallFeatures.PostRtc + diff --git a/test/golden/RuntimeCheckCallFeatures/PostRtc.hs b/test/golden/RuntimeCheckCallFeatures/PostRtc.hs new file mode 100644 index 00000000..34bb9fa2 --- /dev/null +++ b/test/golden/RuntimeCheckCallFeatures/PostRtc.hs @@ -0,0 +1,8 @@ +module RuntimeCheckCallFeatures.PostRtc where + +import Numeric.Natural (Natural) +import RuntimeCheckFeatures.PostRtc (simpleFun) + +externalFunCaller :: Natural +externalFunCaller = simpleFun 1 + diff --git a/test/golden/RuntimeCheckClass.err b/test/golden/RuntimeCheckClass.err new file mode 100644 index 00000000..176bafa3 --- /dev/null +++ b/test/golden/RuntimeCheckClass.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckClass.agda:11,8-15 +Cannot compile NoClass to class. Classes cannot have erased arguments with runtime checking. diff --git a/test/golden/RuntimeCheckFeatures.hs b/test/golden/RuntimeCheckFeatures.hs new file mode 100644 index 00000000..1c0a7500 --- /dev/null +++ b/test/golden/RuntimeCheckFeatures.hs @@ -0,0 +1,66 @@ +module RuntimeCheckFeatures (noneErasedFun, simpleFunCaller, Dat(NoneErasedCon), Rec(recFst, recSnd), Newt(theField), NoneErasedNewt(noneErasedField, NoneErasedNewt), RuntimeCheckFeatures.simpleFun, RuntimeCheckFeatures.fun, RuntimeCheckFeatures.scCon, RuntimeCheckFeatures.scRec, RuntimeCheckFeatures.scNewt) where + +import qualified Haskell.Extra.Dec.Instances (decIsTrue) +import Numeric.Natural (Natural) + +import RuntimeCheckFeatures.PostRtc + +simpleFun :: Natural -> Natural +simpleFun x + | Haskell.Extra.Dec.Instances.decIsTrue (x > 0) = + RuntimeCheckFeatures.PostRtc.simpleFun x + | not (Haskell.Extra.Dec.Instances.decIsTrue (x > 0)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (x > 0)" + +fun :: Natural -> (Natural -> Natural) -> Natural +fun x a1 = RuntimeCheckFeatures.PostRtc.fun x (go1 a1) + where + go1 up y + | Haskell.Extra.Dec.Instances.decIsTrue (y > x) && + Haskell.Extra.Dec.Instances.decIsTrue (y < 5) + = up y + | not (Haskell.Extra.Dec.Instances.decIsTrue (y > x)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (y > x)" + | not (Haskell.Extra.Dec.Instances.decIsTrue (y < 5)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (y < 5)" + +scCon :: ((Natural -> Natural) -> Natural) -> Dat +scCon a0 = Con (\ a0_0 -> a0 (go0_0 a0_0)) + where + go0_0 up x + | Haskell.Extra.Dec.Instances.decIsTrue (x > 0) = up x + | not (Haskell.Extra.Dec.Instances.decIsTrue (x > 0)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (x > 0)" + +scRec recFst recSnd + = Rec recFst (\ a1_0 a1_1 -> recSnd (go1_0 a1_0) (go1_1 a1_1)) + where + go1_0 up + | Haskell.Extra.Dec.Instances.decIsTrue (recFst > 0) = up + | not (Haskell.Extra.Dec.Instances.decIsTrue (recFst > 0)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (recFst > 0)" + go1_1 up + | Haskell.Extra.Dec.Instances.decIsTrue (recFst < 5) = up + | not (Haskell.Extra.Dec.Instances.decIsTrue (recFst < 5)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (recFst < 5)" + +scNewt theField = Newt (go0 theField) + where + go0 up f y + | Haskell.Extra.Dec.Instances.decIsTrue (f (y + 1) > 0) = + up (go0_0 f) y + | not (Haskell.Extra.Dec.Instances.decIsTrue (f (y + 1) > 0)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (f (y + 1) > 0)" + go0_0 up x + | Haskell.Extra.Dec.Instances.decIsTrue (x > 0) = up x + | not (Haskell.Extra.Dec.Instances.decIsTrue (x > 0)) = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (x > 0)" + diff --git a/test/golden/RuntimeCheckFeatures/PostRtc.hs b/test/golden/RuntimeCheckFeatures/PostRtc.hs new file mode 100644 index 00000000..7c26291c --- /dev/null +++ b/test/golden/RuntimeCheckFeatures/PostRtc.hs @@ -0,0 +1,31 @@ +module RuntimeCheckFeatures.PostRtc where + +import qualified Haskell.Extra.Dec.Instances (decIsTrue) +import Numeric.Natural (Natural) + +noneErasedFun :: Natural -> Natural +noneErasedFun _ = 1 + +noDecInstance :: Natural -> Natural +noDecInstance _ = 0 + +simpleFun :: Natural -> Natural +simpleFun _ = 0 + +simpleFunCaller :: Natural +simpleFunCaller = simpleFun 1 + +fun :: Natural -> (Natural -> Natural) -> Natural +fun _ _ = 0 + +data Dat = Con ((Natural -> Natural) -> Natural) + | NoneErasedCon Natural + +data Rec = Rec{recFst :: Natural, + recSnd :: Natural -> Natural -> Natural} + +newtype Newt = Newt{theField :: + (Natural -> Natural) -> Natural -> Natural} + +newtype NoneErasedNewt = NoneErasedNewt{noneErasedField :: Natural} + diff --git a/test/golden/RuntimeCheckGo.err b/test/golden/RuntimeCheckGo.err new file mode 100644 index 00000000..8a45cf92 --- /dev/null +++ b/test/golden/RuntimeCheckGo.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckGo.agda:5,1-9 +Illegal name go0, conflicts with name generated for runtime checks. diff --git a/test/golden/RuntimeCheckInline.err b/test/golden/RuntimeCheckInline.err new file mode 100644 index 00000000..b5c7658a --- /dev/null +++ b/test/golden/RuntimeCheckInline.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckInline.agda:9,1-13 +Cannot make function notInlinable inlinable. Inline functions cannot have erased arguments with runtime checking. diff --git a/test/golden/RuntimeCheckSc.err b/test/golden/RuntimeCheckSc.err new file mode 100644 index 00000000..db1452e0 --- /dev/null +++ b/test/golden/RuntimeCheckSc.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckSc.agda:5,6-9 +Illegal name scConflict, conflicts with name generated for runtime checks. diff --git a/test/golden/RuntimeCheckTransparent.err b/test/golden/RuntimeCheckTransparent.err new file mode 100644 index 00000000..3bd7640a --- /dev/null +++ b/test/golden/RuntimeCheckTransparent.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckTransparent.agda:9,1-14 +Cannot make function noTransparent transparent. Transparent functions cannot have erased arguments with runtime checking. diff --git a/test/golden/RuntimeCheckUnboxed.err b/test/golden/RuntimeCheckUnboxed.err new file mode 100644 index 00000000..52d438c6 --- /dev/null +++ b/test/golden/RuntimeCheckUnboxed.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckUnboxed.agda:9,8-19 +Cannot make record NoUnboxable unboxed. Unboxed records cannot have erased arguments in their fields with runtime checking. diff --git a/test/golden/RuntimeCheckUp.err b/test/golden/RuntimeCheckUp.err new file mode 100644 index 00000000..f0e25078 --- /dev/null +++ b/test/golden/RuntimeCheckUp.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckUp.agda:5,1-9 +Illegal name up, conflicts with name generated for runtime checks. diff --git a/test/golden/RuntimeCheckUseCases.hs b/test/golden/RuntimeCheckUseCases.hs new file mode 100644 index 00000000..b941554d --- /dev/null +++ b/test/golden/RuntimeCheckUseCases.hs @@ -0,0 +1,20 @@ +module RuntimeCheckUseCases (RuntimeCheckUseCases.subtractFromGreater, RuntimeCheckUseCases.headOfNonEmpty) where + +import Haskell.Extra.Dec.Instances (decIsFalse, decNonEmpty) +import Numeric.Natural (Natural) + +import RuntimeCheckUseCases.PostRtc + +subtractFromGreater :: Natural -> Natural -> Natural +subtractFromGreater x y + | decIsFalse (x < y) = + RuntimeCheckUseCases.PostRtc.subtractFromGreater x y + | not (decIsFalse (x < y)) = + error "Runtime check failed: decIsFalse (x < y)" + +headOfNonEmpty :: [Natural] -> Natural +headOfNonEmpty xs + | decNonEmpty xs = RuntimeCheckUseCases.PostRtc.headOfNonEmpty xs + | not (decNonEmpty xs) = + error "Runtime check failed: decNonEmpty xs" + diff --git a/test/golden/RuntimeCheckUseCases/PostRtc.hs b/test/golden/RuntimeCheckUseCases/PostRtc.hs new file mode 100644 index 00000000..b66e3ced --- /dev/null +++ b/test/golden/RuntimeCheckUseCases/PostRtc.hs @@ -0,0 +1,11 @@ +module RuntimeCheckUseCases.PostRtc where + +import Haskell.Extra.Dec.Instances (decIsFalse, decNonEmpty) +import Numeric.Natural (Natural) + +subtractFromGreater :: Natural -> Natural -> Natural +subtractFromGreater x y = x - y + +headOfNonEmpty :: [Natural] -> Natural +headOfNonEmpty (x : _) = x +