From 2f98c9a89a9ad811f88ae4a742fc2e1a34116e8d 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 | 69 ++-- src/Agda2Hs/Compile/Data.hs | 56 ++- src/Agda2Hs/Compile/Function.hs | 34 +- src/Agda2Hs/Compile/Name.hs | 9 +- src/Agda2Hs/Compile/Record.hs | 61 +++- src/Agda2Hs/Compile/RuntimeCheckUtils.hs | 331 ++++++++++++++++++ src/Agda2Hs/Compile/Type.hs | 2 +- src/Agda2Hs/Compile/Types.hs | 25 +- src/Agda2Hs/Compile/Utils.hs | 38 +- src/Agda2Hs/HsUtils.hs | 3 + src/Agda2Hs/Render.hs | 51 ++- src/Main.hs | 8 +- test/AllFailTests.agda | 2 + test/AllRuntimeCheckFailTests.agda | 5 + test/AllRuntimeCheckTests.agda | 5 + test/AllTests.agda | 4 + 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 | 16 +- test/RuntimeCheckAutoImport.agda | 7 + test/RuntimeCheckCallFeatures.agda | 9 + test/RuntimeCheckFeatures.agda | 87 +++++ test/RuntimeCheckUseCases.agda | 12 + test/golden/AllRuntimeCheckTests.hs | 4 + test/golden/AllRuntimeCheckTests/PostRtc.hs | 2 + test/golden/AllTests.hs | 4 + test/golden/PostRtc.err | 1 + test/golden/RuntimeCheckArg.err | 2 + test/golden/RuntimeCheckAutoImport.hs | 15 + test/golden/RuntimeCheckAutoImport/PostRtc.hs | 8 + test/golden/RuntimeCheckCallFeatures.hs | 7 + .../RuntimeCheckCallFeatures/PostRtc.hs | 8 + test/golden/RuntimeCheckClass.err | 2 + test/golden/RuntimeCheckFeatures.hs | 67 ++++ test/golden/RuntimeCheckFeatures/PostRtc.hs | 52 +++ 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 | 18 + test/golden/RuntimeCheckUseCases/PostRtc.hs | 11 + 52 files changed, 1113 insertions(+), 98 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/RuntimeCheckAutoImport.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/RuntimeCheckAutoImport.hs create mode 100644 test/golden/RuntimeCheckAutoImport/PostRtc.hs 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 b85576db..2e863770 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..564bcac8 --- /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 {xs = []} = True ⟨ allNil ⟩ + decAll {xs = 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 {xs = []} = False ⟨ (λ ()) ⟩ + decAny {xs = 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 2a2941e7..54d7db35 100644 --- a/src/Agda2Hs/Compile.hs +++ b/src/Agda2Hs/Compile.hs @@ -24,15 +24,16 @@ 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 import Agda2Hs.Pragma import qualified Language.Haskell.Exts.Syntax as Hs import qualified Language.Haskell.Exts.Pretty as Hs -initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv -initCompileEnv tlm rewrites = CompileEnv +initCompileEnv :: TopLevelModuleName -> Bool -> SpecialRules -> CompileEnv +initCompileEnv tlm rtc rewrites = CompileEnv { currModule = tlm , minRecordName = Nothing , isNestedInType = False @@ -40,6 +41,7 @@ initCompileEnv tlm rewrites = CompileEnv , compilingLocal = False , whereModules = [] , copatternsEnabled = False + , rtc = rtc , rewrites = rewrites , writeImports = True } @@ -47,8 +49,8 @@ initCompileEnv tlm rewrites = CompileEnv 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 @@ -64,20 +66,22 @@ moduleSetup _ _ m _ = do compile :: Options -> ModuleEnv -> IsMain -> Definition - -> TCM (CompiledDef, CompileOutput) -compile opts tlm _ def = + -> TCM (RtcDefs, 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 RtcDefs + compileAndTag = (tag <$>) <$> do p <- processPragma qname reportSDoc "agda2hs.compile" 5 $ text "Compiling definition:" <+> prettyTCM qname @@ -89,39 +93,42 @@ 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 - (TuplePragma b , Record{} ) -> return [] - - (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 $ WithRtc [] [] + (ExistingClassPragma, _ ) -> return $ WithRtc [] [] + (TuplePragma b , Record{} ) -> return $ WithRtc [] [] + (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 {} ) | not isInstance -> compileRecord (ToRecord False ds) def + -- ^ Names that may induce runtime checks or are safe to have none + _ -> do + tellNoErased $ prettyShow $ qnameName $ defName def + (`WithRtc` []) <$> 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 verifyOutput :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName - -> [(CompiledDef, CompileOutput)] -> TCM Bool + -> [(RtcDefs, CompileOutput)] -> TCM Bool verifyOutput _ _ _ m ls = do reportSDoc "agda2hs.compile" 5 $ text "Checking generated output before rendering: " <+> prettyTCM m ensureUniqueConstructors where ensureUniqueConstructors = do let allCons = do - (r, _) <- ls + -- take from concat'd definitions and runtime checks + r <- ls >>= (\(WithRtc d r) -> d : [r]) . fst (_, a) <- r Hs.DataDecl _ _ _ _ cons _ <- a Hs.QualConDecl _ _ _ con <- cons diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs index 3a544a0a..65486a5f 100644 --- a/src/Agda2Hs/Compile/Data.hs +++ b/src/Agda2Hs/Compile/Data.hs @@ -1,8 +1,9 @@ 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.List ( intercalate, partition ) import Agda.Compiler.Backend import Agda.Syntax.Common import Agda.Syntax.Internal @@ -14,11 +15,27 @@ import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) +import Agda.Utils.Monad ( ifNotM ) -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 +data DataRtcResult + = NoRtc + | DataNoneErased String + | DataUncheckable + | DataCheckable [Hs.Decl ()] + +concatRtc :: [DataRtcResult] -> ([String], [Hs.Decl ()]) +concatRtc [] = ([], []) +concatRtc (res : ress) = case res of + DataNoneErased s -> (s : tlNoneErased, tlCheckable) + DataCheckable ds -> (tlNoneErased, ds ++ tlCheckable) + _ -> tl + where + tl@(tlNoneErased, tlCheckable) = concatRtc ress checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C () checkNewtype name cs = do @@ -27,9 +44,10 @@ checkNewtype name cs = do (Hs.QualConDecl () _ _ (Hs.ConDecl () cName types):_) -> checkNewtypeCon cName types _ -> __IMPOSSIBLE__ -compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()] +compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C RtcDecls 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) @@ -38,14 +56,21 @@ 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 <- ifNotM (emitsRtc $ defName def) (return []) $ do + let (noneErased, chks) = concatRtc $ map snd chkdCs + -- Always export data type name + tellNoErased $ prettyName ++ "(" ++ intercalate ", " noneErased ++ ")" + return chks + + 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 $ WithRtc [Hs.DataDecl () target Nothing hd cs ds] chks where allIndicesErased :: Type -> C () allIndicesErased t = reduce (unEl t) >>= \case @@ -56,17 +81,28 @@ 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 (), DataRtcResult) 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 <- ifNotM (emitsRtc c) (return NoRtc) $ do + sig <- Hs.TypeSig () [hsName $ prettyShow $ qnameName smartQName] <$> compileType (unEl ty) + -- export constructor name when none erased, provide signature for smart constructor if it exists + checkRtc tel smartQName (hsVar conString) alternatingLevels >>= \case + NoneErased -> return $ DataNoneErased conString + Uncheckable -> return DataUncheckable + Checkable ds -> return $ DataCheckable $ sig : ds + + 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 3366837c..537505f4 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 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 ) @@ -97,7 +98,7 @@ compileLitNatPat = \case compileFun, compileFun' :: Bool -- ^ Whether the type signature shuuld also be generated - -> Definition -> C [Hs.Decl ()] + -> Definition -> C RtcDecls compileFun withSig def@Defn{..} = setCurrentRangeQ defName @@ -115,7 +116,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) + ((`WithRtc` []) <$> (ensureNoLocals err >> compileTypeDef x def)) -- otherwise, we have to compile clauses. $ do tel <- lookupSection m @@ -159,7 +160,15 @@ 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 <- ifNotM (emitsRtc defName) (return []) $ do + let typeTel = theTel $ telView' defType + success = hsVar $ prettyShow m ++ ".PostRtc." ++ prettyShow n + checkRtc typeTel defName success alternatingLevels >>= \case + NoneErased -> do tellNoErased $ prettyShow n; return [] + Uncheckable -> return [] + Checkable ds -> return $ sig ++ ds + return $ WithRtc def chk where Function{..} = theDef m = qnameModule defName @@ -235,7 +244,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 defn 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 @@ -373,13 +382,20 @@ 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 (andM [emitsRtc $ defName def, not <$> checkNoneErased tele]) $ genericDocError =<< + "Cannot make function" <+> prettyTCM (defName def) <+> "transparent." <+> + "Transparent functions cannot have erased arguments with runtime checking." + compiledFun <- defn <$> compileFun False def + case compiledFun of [Hs.FunBind _ cls] -> mapM_ checkTransparentClause cls [Hs.TypeDecl _ hd b] -> checkTransparentTypeDef hd b _ -> __IMPOSSIBLE__ where + tele = theTel $ telView' $ defType def + checkTransparentClause :: Hs.Match () -> C () checkTransparentClause = \case Hs.Match _ _ [p] (Hs.UnGuardedRhs _ e) _ | patToExp p == Just e -> return () @@ -396,8 +412,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 (andM [emitsRtc $ defName def, 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 ed42dcbb..4ba958af 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -34,7 +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 ( whenM ) +import Agda.Utils.Monad ( ifNotM, whenM ) import Agda2Hs.AgdaUtils import Agda2Hs.Compile.Types @@ -106,9 +106,12 @@ compileQName f parent <- parentName f par <- traverse (compileName . qnameName) parent let mod0 = qnameModule $ fromMaybe f parent - mod <- compileModuleName mod0 + mod' <- compileModuleName mod0 + mod <- ifNotM (emitsRtc f) (return mod') $ case mod' of + Hs.ModuleName () s -> do + return $ Hs.ModuleName () $ s ++ ".PostRtc" 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..933142c7 100644 --- a/src/Agda2Hs/Compile/Record.hs +++ b/src/Agda2Hs/Compile/Record.hs @@ -4,7 +4,7 @@ module Agda2Hs.Compile.Record where import Control.Monad ( unless, when ) import Control.Monad.Reader ( MonadReader(local) ) -import Data.List ( (\\), nub ) +import Data.List ( (\\), intercalate, nub ) import Data.List.NonEmpty ( NonEmpty(..) ) import Data.Map ( Map ) import qualified Data.Map as Map @@ -23,10 +23,12 @@ import Agda.TypeChecking.Telescope import Agda.Utils.Singleton import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) +import Agda.Utils.Monad ( andM, ifNotM, 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 +52,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 + concatMap defn <$> traverse (compileFun False) defaults let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ] return (definedFields, declMap) @@ -91,7 +93,7 @@ compileMinRecords def sls = do return ([minPragma | not (null prims)] ++ Map.elems decls) -compileRecord :: RecordTarget -> Definition -> C (Hs.Decl ()) +compileRecord :: RecordTarget -> Definition -> C RtcDecls compileRecord target def = do TelV tel _ <- telViewUpTo recPars (defType def) addContext tel $ do @@ -101,24 +103,43 @@ compileRecord target def = do let fieldTel = snd $ splitTelescopeAt recPars recTel case target of ToClass ms -> do - (classConstraints, classDecls) <- compileRecFields classDecl recFields fieldTel + whenM (andM [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 $ WithRtc [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, fieldTypes) <- compileRecFields fieldDecl recFields fieldTel + + chk <- ifNotM (emitsRtc $ defName def) (return []) $ do + let scType = foldr (Hs.TyFun ()) (Hs.TyVar () $ Hs.Ident () rString) fieldTypes + sig = Hs.TypeSig () [hsName $ prettyShow $ qnameName smartQName] scType + -- Both the fields and their types should be considered to be in odd position + (noneErasedCons, chk) <- checkRtc fieldTel smartQName (hsVar conString) (Odd : alternatingLevels) >>= \case + NoneErased -> return ([conString], []) + Uncheckable -> return ([], []) + Checkable ds -> return ([], sig : ds) + -- Always export record name and field names. Export constructor when it has no erased types. + tellNoErased $ rString ++ "(" ++ intercalate ", " (fieldStrings ++ noneErasedCons) ++ ")" + return chk + when newtyp $ checkNewtypeCon cName fieldDecls let target = if newtyp then Hs.NewType () else Hs.DataType () - compileDataRecord constraints fieldDecls target hd ds - + (\c -> WithRtc [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 -- Reuse record name for constructor if no given name + 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], [Hs.Type ()]) 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, hsTypes) <- 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, hsA : hsTypes) DomConstraint hsA -> case target of - ToClass{} -> return (hsA : hsAssts , hsFields) + ToClass{} -> return (hsA : hsAssts, hsFields, fieldStrings, hsTypes) ToRecord{} -> genericError $ "Not supported: record/class with constraint fields" - DomDropped -> return (hsAssts , hsFields) + DomDropped -> return (hsAssts, hsFields, fieldStrings, hsTypes) DomForall{} -> __IMPOSSIBLE__ (_, _) -> __IMPOSSIBLE__ @@ -185,6 +207,9 @@ checkUnboxPragma def = do addContext tel $ do pars <- getContextArgs let fieldTel = recTel `apply` pars + whenM (andM [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..60353b07 --- /dev/null +++ b/src/Agda2Hs/Compile/RuntimeCheckUtils.hs @@ -0,0 +1,331 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Agda2Hs.Compile.RuntimeCheckUtils (importDec, checkNoneErased, smartConstructor, NestedLevel (Odd), alternatingLevels, 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 (NiceEnv (NiceEnv), niceDeclarations, 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 Agda.Utils.List (initLast) +import qualified Agda.Utils.List1 as List1 +import Agda.Utils.Monad (allM, partitionM, unless) +import Agda2Hs.Compile.Term (compileTerm) +import Agda2Hs.Compile.Type (DomOutput (DODropped), compileDom) +import Agda2Hs.Compile.Types (C) +import Agda2Hs.Compile.Utils +import Agda2Hs.HsUtils +import Control.Monad.Except (catchError) +import Control.Monad.State (StateT (StateT, runStateT)) +import Data.List (intersect) +import Data.Map (empty) +import Data.Maybe (catMaybes, fromJust, isJust) +import Data.Tree (flatten, unfoldTree) +import Data.Tuple (swap) +import qualified Language.Haskell.Exts as Hs + +-- Import Haskell.Extra.Dec{,.Instances} +-- based on Agda.Syntax.Translation.ConcreteToAbstract.importPrimitives +importDec :: TCM () +importDec = do + let haskellExtra = AN.Qual (AC.simpleName "Haskell") . AN.Qual (AC.simpleName "Extra") + dec = AC.simpleName "Dec" + 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 dec + run $ AN.Qual 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 + -- 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 the telescope has no erased types. +checkNoneErased :: Telescope -> C Bool +checkNoneErased tel = do + let doms = telToList tel + (erased, other) <- partitionM (checkTopOrDataErased . fst) $ zip doms $ map (domToTel . (snd <$>)) doms + (null erased &&) <$> allM other (checkNoneErased . snd) + +-- Check if a type is erased or contains an erased type within a data type or record. +-- In this case, it should be checked. +checkTopOrDataErased :: Dom (a, Type) -> C Bool +checkTopOrDataErased d = do + let domType = snd <$> d + unfold = unfoldTypes [unDom domType] + -- do not recurse into Pi at top level (that is still handled by checkRtc'), + -- but do at `Apply` levels below + tels = [domToTel t | Pi t _ <- map unArg unfold] + quantities = getQuantity d : map getQuantity unfold + domDropped <- (DODropped ==) <$> compileDom domType + (or (domDropped : [True | Quantity0 _ <- quantities]) ||) . not . and <$> mapM checkNoneErased tels + +-- Only preconditions on odd levels of nesting should incur a check +-- because only they can be violated from Haskell +-- See Findler and Felleisen, Contracts for Higher-Order Functions, ICFP 2002 +data NestedLevel = Odd | Even + +-- Expected only to be used with infinite lists. Stream would be +-- more faithful, but we use lists for dependency simplicity. +whenOdd :: [NestedLevel] -> [a] -> [a] +whenOdd (Odd : _) l = l +whenOdd (Even : _) _ = [] + +alternatingLevels :: [NestedLevel] +alternatingLevels = cycle [Odd, Even] + +-- 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 : notChks ++ [otherwiseChk] + andChks = foldr1 (\c -> Hs.InfixApp () c $ Hs.QVarOp () $ Hs.UnQual () $ Hs.Symbol () "&&") chks + chk2err chk = + let msg = "Runtime check failed: " ++ Hs.prettyPrint chk + in Hs.App () (hsVar "error") $ Hs.Lit () $ Hs.String () msg msg + errs = zip chks $ map chk2err chks + (nots, otherwise) = fromJust $ initLast errs + notChks = map (\(chk, err) -> Hs.GuardedRhs () [Hs.Qualifier () $ Hs.App () (hsVar "not") chk] err) nots + otherwiseChk = (\(_, err) -> Hs.GuardedRhs () [Hs.Qualifier () $ hsVar "otherwise"] err) otherwise + +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] + +{- Suffixes for `go` functions in the `where` declaration for nested +erased arguments and `a` arguments for unnamed arguments. +Example to show all cases: + +Turning + +tripleOdd : (((m : Nat) → @0 IsTrue (m > 0) → (((n : Nat) → @0 IsFalse (n < 1) → Nat) → Nat) → Nat) → Nat) → Nat + +into + +tripleOdd a0 = TripleOdd.PostRtc.tripleOdd (\ a1 -> a0 (go1 a1)) + where + go1 up m a2 + | decIsTrue (m > 0) = up m (\ a3 -> a2 (go0 a3)) + | otherwise = error "Runtime check failed: decIsTrue (m > 0)" + where + go0 up n + | decIsFalse (n < 1) = up n + | otherwise = error "Runtime check failed: decIsFalse (n < 1)" + +has a tree of + +(((m : Nat) → @0 … → (((n : Nat) → @0 … → Nat) → Nat) → Nat) → Nat) → Nat ~ (0, 0) +Reserve a0 for ((Nat → ((Nat → Nat) → Nat) → Nat) → Nat): + ((m : Nat) → @0 … → (((n : Nat) → @0 … → Nat) → Nat) → Nat) → Nat ~ (0, 1) +Reserve a1 for (Nat → ((Nat → Nat) → Nat) → Nat): + (m : Nat) → @0 … → (((n : Nat) → @0 … → Nat) → Nat) → Nat ~ (0, 2) +Reserve a2 for ((Nat → Nat) → Nat): + ((n : Nat) → @0 … → Nat) → Nat ~ (0, 3) +Reserve a3 for (Nat → Nat): + (n : Nat) → @0 … → Nat ~ (0, 4) + ~ (0, 4) +Reserve go0 for (((Nat → Nat) → Nat) → Nat): + ~ (1, 4) +Inline: + ~ (1, 4) +Reserve go1 for ((Nat → ((Nat → Nat) → Nat) → Nat) → Nat → ((Nat → Nat) → Nat) → Nat): + ~ (2, 4) +Inline: +~ (2, 4) +-} +type NameIndices = (Int, Int) + +-- Creates a runtime check if necessary and possible, informing C accordingly. +-- Takes telescope of type to check, name, level of nesting, and expression on success. +checkRtc :: Telescope -> QName -> Hs.Exp () -> [NestedLevel] -> C RtcResult +checkRtc tel name success lvls = do + (_, chk) <- checkRtc' (0, 0) tel lvls + case chk of + NoneErased' -> return NoneErased + Uncheckable' -> return Uncheckable + Checkable' {..} -> do + tellAllCheckable name + let rhs = eApp success theirRhs + chkName = hsName $ prettyShow $ qnameName name + chk = createRtc chkName theirLhs theirChks rhs $ binds theirDecls + return $ Checkable [chk] + +-- Recursively check for runtime checkability in nested types. +-- Accumulates on name indices for `go` function and `a` argument. +-- Takes telescope of type to check. +checkRtc' :: NameIndices -> Telescope -> [NestedLevel] -> C (NameIndices, RtcResult') +checkRtc' idcs tel lvls = do + -- Partition out arguments that are erased and at top level (those we will attempt to check) + (erased, call) <- partitionM (checkTopOrDataErased . fst) $ zip doms telsUpTo + ourChks <- uncurry createGuardExp `mapM` whenOdd lvls erased + -- Recursively accumulate checks on arguments below top level + (belowIdcs, belowChks) <- mapAccumLM checkRtc'' idcs $ map (,lvls) call + (belowIdcs,) + <$> if not $ all isJust belowChks && all isJust ourChks + then return Uncheckable' + else -- all checkable or none erased + let (theirLhs, theirRhs, decls) = unzip3 $ catMaybes belowChks + theirDecls = concat decls + -- all checks below found an instance + theirChks = catMaybes ourChks + in if null theirDecls && null erased + then return NoneErased' + else return Checkable' {..} + where + doms = telToList tel + telsUpTo = map (\i -> fst $ splitTelescopeAt i tel) [0 ..] + +-- Check a single type for runtime checkability. +-- Accumulates on name indices for `go` function and `a` argument. +-- Takes domain of type and telescope up to that point for context. +-- If checkable, returns lhs and rhs at that point plus declarations from checks below. +checkRtc'' :: + NameIndices -> + ((Dom (ArgName, Type), Telescope), [NestedLevel]) -> + C (NameIndices, Maybe (Hs.Pat (), Hs.Exp (), [Hs.Decl ()])) +checkRtc'' (goIdx, argIdx) ((d, tUpTo), _ : lvls) = + -- Mutual recursion with checkRtc' + addContext tUpTo (checkRtc' (goIdx, ourArgIdx) tAt lvls) >>= \case + (idcs, NoneErased') -> return (idcs, Just (ourLhs, argVar, [])) + (idcs, Uncheckable') -> return (idcs, Nothing) + ((theirGoIdx, theirArgIdx), Checkable' {..}) -> do + let go = "go" ++ show theirGoIdx + conflicts = tAtNames `intersect` [go, arg, up] + unless (null conflicts) $ errorNameConflict $ head conflicts + let (ourGoIdx, ourRhs, ourRtc) = + if null theirChks + then -- inline if nothing to check at this level (consumes no `goIdx`) + -- e.g. `\ a1 -> a0 (go1 a1)`, continuing the example above `NameIndices` + (theirGoIdx, Hs.Lambda () theirLhs $ argVar `eApp` theirRhs, theirDecls) + else + let -- e.g. `up x a2` + lhs = hsPat up : theirLhs + -- e.g. `up x (go0 a2)` + rhs = hsVar up `eApp` theirRhs + rtc = createRtc (hsName go) lhs theirChks rhs $ binds theirDecls + in -- e.g. `go1 a1` + (succ theirGoIdx, hsVar go `eApp` [argVar], [rtc]) + return ((ourGoIdx, theirArgIdx), Just (ourLhs, ourRhs, ourRtc)) + where + tAt = domToTel $ snd <$> d + tAtNames = map (fst . unDom) $ telToList tAt + name = fst $ unDom d + -- Use arg name if available, otherwise insert one (consumes one on `argIdx`) + (arg, ourArgIdx) = if name == "_" then ("a" ++ show argIdx, succ argIdx) else (name, argIdx) + ourLhs = hsPat arg + argVar = hsVar arg + up = "up" + +---- Small convenience functions + +-- Gather telescope from domain +domToTel :: Dom Type -> Telescope +domToTel = theTel . telView' . unDom + +-- Unfold data types and records from list of types +unfoldTypes :: [Type] -> [Arg Term] +unfoldTypes tys = + concat $ + flatten $ + ( \tes -> + let argss = [[a | Apply a <- es] | Def _ es <- tes] + in (concat argss, map (map unArg) argss) + ) + `unfoldTree` map unEl tys + +-- Create binds from declarations except when empty +binds :: [Hs.Decl ()] -> Maybe (Hs.Binds ()) +binds [] = Nothing +binds decls = Just $ Hs.BDecls () decls + +-- 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 -> TCMT IO (Maybe Term) +findDecInstances t = + do + (m, v) <- newInstanceMeta "" t + findInstance m Nothing + Just <$> instantiate v + `catchError` return (return Nothing) + +-- Create expression to be put in the guard +createGuardExp :: Dom (a, Type) -> Telescope -> C (Maybe (Hs.Exp ())) +createGuardExp dom telUpTo = addContext telUpTo $ do + dec <- decify $ snd $ unDom dom + liftTCM (findDecInstances dec) >>= traverse (compileTerm dec) + +-- from GHC.Utils.Monad +mapAccumLM :: (Monad m, Traversable t) => (acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y) +mapAccumLM f s = fmap swap . flip runStateT s . traverse f' + where + f' = StateT . (fmap . fmap) swap . flip f diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs index 889c0f73..7cd5b8b6 100644 --- a/src/Agda2Hs/Compile/Type.hs +++ b/src/Agda2Hs/Compile/Type.hs @@ -223,7 +223,7 @@ compileInlineType f args = do _ -> genericDocError =<< text "Could not reduce inline type alias " <+> prettyTCM f -data DomOutput = DOInstance | DODropped | DOType | DOTerm +data DomOutput = DOInstance | DODropped | DOType | DOTerm deriving Eq compileDom :: Dom Type -> C DomOutput compileDom a = do diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 2892a8ea..6902c83a 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -34,6 +34,18 @@ type Ranged a = (Range, a) type Code = (Hs.Module Hs.SrcSpanInfo, [Hs.Comment]) +data WithRtc d = WithRtc { + defn :: d, + -- Runtime check + rtcDefn :: d +} + +instance Functor WithRtc where + fmap f (WithRtc d r) = WithRtc (f d) (f r) + +type RtcDefs = WithRtc CompiledDef +type RtcDecls = WithRtc [Hs.Decl ()] + -- | Custom substitution for a given definition. data Rewrite = Rewrite { rewFrom :: String @@ -62,6 +74,7 @@ data Options = Options , optOutDir :: Maybe FilePath , optConfigFile :: Maybe FilePath , optExtensions :: [Hs.Extension] + , optRtc :: Bool , optRewrites :: SpecialRules , optPrelude :: PreludeOptions } @@ -88,6 +101,8 @@ data CompileEnv = CompileEnv -- ^ the where-blocks currently in scope. Hack until Agda adds where-prominence , 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. , writeImports :: Bool @@ -125,14 +140,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 d5fac4b8..6da2c160 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -41,6 +41,7 @@ import Agda.Utils.Lens ( (<&>) ) import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Singleton +import Agda.Utils.Tuple ( (-*-) ) import AgdaInternals import Agda2Hs.AgdaUtils ( (~~) ) @@ -323,10 +324,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] tellUnboxedTuples :: Hs.Boxed -> C () tellUnboxedTuples Hs.Boxed = return () @@ -358,7 +365,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 RtcDecls -> C RtcDecls maybePrependFixity n f comp | f /= noFixity = do hsLvl <- checkFixityLevel n (fixityLevel f) let x = hsName $ prettyShow $ qnameName n @@ -366,7 +373,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]:) + (head <$>) <$> comp maybePrependFixity n f comp = comp @@ -390,3 +398,25 @@ checkNoAsPatterns = \case noWriteImports :: C a -> C a noWriteImports = local $ \e -> e { writeImports = False } + +testResolveStringName :: String -> C (Maybe QName) +testResolveStringName s = do + cqname <- liftTCM $ parseName noRange s + rname <- liftTCM $ resolveName cqname + case rname of + DefinedName _ aname _ -> return $ Just $ anameName aname + _ -> return Nothing + +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.hs 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 e09a5a8b..3835a6ef 100644 --- a/src/Agda2Hs/HsUtils.hs +++ b/src/Agda2Hs/HsUtils.hs @@ -78,6 +78,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..b772f4b8 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 + -> [(RtcDefs, 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 . defn . fst) outs ++ codeBlocks code + chkdefs = concatMap (defBlock . rtcDefn . 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,29 @@ 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 + + -- "pre" runtime check output (_the_ output if RTC disabled) + 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 c8642aec..da6275e6 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,10 @@ 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 (RtcDefs, CompileOutput) backend = Backend' { backendName = "agda2hs" , backendVersion = Just (showVersion version) @@ -64,6 +67,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 24deabc8..72fbbdf0 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..10ec318d --- /dev/null +++ b/test/AllRuntimeCheckTests.agda @@ -0,0 +1,5 @@ +module AllRuntimeCheckTests where + +import RuntimeCheckCallFeatures +import RuntimeCheckUseCases +import RuntimeCheckAutoImport diff --git a/test/AllTests.agda b/test/AllTests.agda index c62f9f24..27b7b84d 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -179,4 +179,8 @@ import ErasedPatternLambda import CustomTuples import ProjectionLike import FunCon + +import RuntimeCheckCallFeatures +import RuntimeCheckUseCases +import RuntimeCheckAutoImport #-} 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..f3f8c9fe --- /dev/null +++ b/test/Fail/RuntimeCheckArg.agda @@ -0,0 +1,7 @@ +module Fail.RuntimeCheckArg where + +open import Haskell.Prelude + +conflict : ((Nat → (a1 : Nat) → @0 IsTrue (a1 > 0) → Nat) → 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..25511450 --- /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) → 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..81f9e0ff --- /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 NotUnboxable : Set where + field noUnboxField : (@0 _ : IsTrue Bool.true) → Nat +{-# COMPILE AGDA2HS NotUnboxable unboxed #-} diff --git a/test/Fail/RuntimeCheckUp.agda b/test/Fail/RuntimeCheckUp.agda new file mode 100644 index 00000000..d68da756 --- /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) → Nat +conflict _ = 0 +{-# COMPILE AGDA2HS conflict #-} diff --git a/test/Makefile b/test/Makefile index ed87e47a..acfdc500 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,27 +11,32 @@ default : compare build/%.hs : %.agda *.agda Fail/*.agda Cubical/*.agda agda2hs @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 == + mkdir -p build fail : print-fail $(patsubst Fail/%.agda,build/%.err,$(wildcard Fail/*.agda)) build/%.err : Fail/%.agda agda2hs @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/RuntimeCheckAutoImport.agda b/test/RuntimeCheckAutoImport.agda new file mode 100644 index 00000000..f3084d5d --- /dev/null +++ b/test/RuntimeCheckAutoImport.agda @@ -0,0 +1,7 @@ +module RuntimeCheckAutoImport where + +open import Haskell.Prelude + +simpleFun : (x : Nat) ⦃@0 _ : IsTrue (x > 0)⦄ → Nat +simpleFun _ = 0 +{-# COMPILE AGDA2HS simpleFun #-} diff --git a/test/RuntimeCheckCallFeatures.agda b/test/RuntimeCheckCallFeatures.agda new file mode 100644 index 00000000..d6fcd80b --- /dev/null +++ b/test/RuntimeCheckCallFeatures.agda @@ -0,0 +1,9 @@ +{-# 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..ddeaa14c --- /dev/null +++ b/test/RuntimeCheckFeatures.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --sized-types #-} +module RuntimeCheckFeatures where + +open import Haskell.Prelude +open import Haskell.Extra.Delay +open import Haskell.Extra.Erase +open import Haskell.Extra.Dec.Instances + +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 #-} + +-- Even precondition +singleEven : ((x : Nat) → @0 IsTrue (x > 0) → Nat) → Nat +singleEven _ = 0 +{-# COMPILE AGDA2HS singleEven #-} + +-- Double odd precondition with backreferencing and same-level nested checks +doubleOdd : (x : Nat) → (((y : Nat) → @0 IsFalse (x < y) → Nat) → Nat) → (((y : Nat) → @0 IsFalse (x < y) → Nat) → Nat) → Nat +doubleOdd _ _ _ = 0 +{-# COMPILE AGDA2HS doubleOdd #-} + +-- Triple odd precondition with multi-level checks +tripleOdd : (((m : Nat) → @0 IsTrue (m > 0) → (((n : Nat) → @0 IsFalse (n < 1) → Nat) → Nat) → Nat) → Nat) → Nat +tripleOdd _ = 0 +{-# COMPILE AGDA2HS tripleOdd #-} + +-- 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) → 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 +open Rec public +{-# COMPILE AGDA2HS Rec #-} + +record Newt : Set where + field + theField : (x : Nat) → @0 IsTrue (x > 0) → Nat +open Newt public +{-# COMPILE AGDA2HS Newt newtype #-} + +record NoneErasedNewt : Set where + field + noneErasedField : Nat +open NoneErasedNewt public +{-# COMPILE AGDA2HS NoneErasedNewt newtype #-} + +record ErasedField : Set where + field + erasedFst : Nat + @0 erasedSnd : IsTrue (erasedFst > 0) +open ErasedField public +{-# COMPILE AGDA2HS ErasedField #-} + +-- Should not be exported due to erased within +listErased : (fs : List (((n : Nat) → @0 ⦃ IsFalse (n < 1) ⦄ → Nat) → Nat)) → Nat +listErased _ = 0 +{-# COMPILE AGDA2HS listErased #-} + +-- Should not be exported due to erased (part of TCB) +eraseTCB : (n : Nat) → @0 Erase (IsFalse (1 < n)) → Nat +eraseTCB n iErased = 0 +{-# COMPILE AGDA2HS eraseTCB #-} + +-- Should be exported despite TCB record containing an erasure because erasure is not in a critical position +fUnzip : {a b : Set} {f : Set → Set} → ⦃ Functor f ⦄ → f (a × b) → (f a × f b) +fUnzip xs = (fmap fst xs , fmap snd xs) +{-# COMPILE AGDA2HS fUnzip #-} diff --git a/test/RuntimeCheckUseCases.agda b/test/RuntimeCheckUseCases.agda new file mode 100644 index 00000000..0590787d --- /dev/null +++ b/test/RuntimeCheckUseCases.agda @@ -0,0 +1,12 @@ +module RuntimeCheckUseCases where + +open import Haskell.Prelude +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 f970e50c..83c24b76 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -87,3 +87,7 @@ import CustomTuples import ProjectionLike import FunCon +import RuntimeCheckCallFeatures +import RuntimeCheckUseCases +import RuntimeCheckAutoImport + 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..229d0abf --- /dev/null +++ b/test/golden/RuntimeCheckArg.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckArg.agda:5,1-9 +Illegal name a1, conflicts with name generated for runtime checks. diff --git a/test/golden/RuntimeCheckAutoImport.hs b/test/golden/RuntimeCheckAutoImport.hs new file mode 100644 index 00000000..c0dd7f15 --- /dev/null +++ b/test/golden/RuntimeCheckAutoImport.hs @@ -0,0 +1,15 @@ +module RuntimeCheckAutoImport (RuntimeCheckAutoImport.simpleFun) where + +import qualified Haskell.Extra.Dec.Instances (decIsTrue) +import Numeric.Natural (Natural) + +import RuntimeCheckAutoImport.PostRtc + +simpleFun :: Natural -> Natural +simpleFun x + | Haskell.Extra.Dec.Instances.decIsTrue (x > 0) = + RuntimeCheckAutoImport.PostRtc.simpleFun x + | otherwise = + error + "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (x > 0)" + diff --git a/test/golden/RuntimeCheckAutoImport/PostRtc.hs b/test/golden/RuntimeCheckAutoImport/PostRtc.hs new file mode 100644 index 00000000..8dbef56a --- /dev/null +++ b/test/golden/RuntimeCheckAutoImport/PostRtc.hs @@ -0,0 +1,8 @@ +module RuntimeCheckAutoImport.PostRtc where + +import qualified Haskell.Extra.Dec.Instances (decIsTrue) +import Numeric.Natural (Natural) + +simpleFun :: Natural -> Natural +simpleFun _ = 0 + 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..45e77a6a --- /dev/null +++ b/test/golden/RuntimeCheckFeatures.hs @@ -0,0 +1,67 @@ +module RuntimeCheckFeatures (noneErasedFun, simpleFunCaller, singleEven, Dat(NoneErasedCon), Rec(recFst, recSnd), Newt(theField), NoneErasedNewt(noneErasedField, NoneErasedNewt), ErasedField(erasedFst), fUnzip, RuntimeCheckFeatures.simpleFun, RuntimeCheckFeatures.doubleOdd, RuntimeCheckFeatures.tripleOdd, RuntimeCheckFeatures.scCon, RuntimeCheckFeatures.scRec, RuntimeCheckFeatures.scNewt, RuntimeCheckFeatures.scErasedField) where + +import Haskell.Extra.Dec.Instances (decIsFalse, decIsTrue) +import Numeric.Natural (Natural) + +import RuntimeCheckFeatures.PostRtc + +simpleFun :: Natural -> Natural +simpleFun x + | decIsTrue (x > 0) = RuntimeCheckFeatures.PostRtc.simpleFun x + | otherwise = error "Runtime check failed: decIsTrue (x > 0)" + +doubleOdd :: + Natural -> + ((Natural -> Natural) -> Natural) -> + ((Natural -> Natural) -> Natural) -> Natural +doubleOdd x a0 a2 + = RuntimeCheckFeatures.PostRtc.doubleOdd x (\ a1 -> a0 (go0 a1)) + (\ a3 -> a2 (go1 a3)) + where + go0 up y + | decIsFalse (x < y) = up y + | otherwise = error "Runtime check failed: decIsFalse (x < y)" + go1 up y + | decIsFalse (x < y) = up y + | otherwise = error "Runtime check failed: decIsFalse (x < y)" + +tripleOdd :: + ((Natural -> ((Natural -> Natural) -> Natural) -> Natural) -> + Natural) + -> Natural +tripleOdd a0 + = RuntimeCheckFeatures.PostRtc.tripleOdd (\ a1 -> a0 (go1 a1)) + where + go1 up m a2 + | decIsTrue (m > 0) = up m (\ a3 -> a2 (go0 a3)) + | otherwise = error "Runtime check failed: decIsTrue (m > 0)" + where + go0 up n + | decIsFalse (n < 1) = up n + | otherwise = error "Runtime check failed: decIsFalse (n < 1)" + +scCon :: Natural -> Dat +scCon x + | decIsTrue (x > 0) = Con x + | otherwise = error "Runtime check failed: decIsTrue (x > 0)" + +scRec :: Natural -> Natural -> Rec +scRec recFst recSnd = Rec recFst (go0 recSnd) + where + go0 up + | decIsTrue (recFst > 0) = up + | otherwise = error "Runtime check failed: decIsTrue (recFst > 0)" + +scNewt :: (Natural -> Natural) -> Newt +scNewt theField = Newt (go0 theField) + where + go0 up x + | decIsTrue (x > 0) = up x + | otherwise = error "Runtime check failed: decIsTrue (x > 0)" + +scErasedField :: Natural -> ErasedField +scErasedField erasedFst + | decIsTrue (erasedFst > 0) = ErasedField erasedFst + | otherwise = + error "Runtime check failed: decIsTrue (erasedFst > 0)" + diff --git a/test/golden/RuntimeCheckFeatures/PostRtc.hs b/test/golden/RuntimeCheckFeatures/PostRtc.hs new file mode 100644 index 00000000..05d1d619 --- /dev/null +++ b/test/golden/RuntimeCheckFeatures/PostRtc.hs @@ -0,0 +1,52 @@ +module RuntimeCheckFeatures.PostRtc where + +import Haskell.Extra.Dec.Instances (decIsFalse, decIsTrue) +import Numeric.Natural (Natural) + +noneErasedFun :: Natural -> Natural +noneErasedFun _ = 1 + +noDecInstance :: Natural -> Natural +noDecInstance x = 0 + +simpleFun :: Natural -> Natural +simpleFun _ = 0 + +simpleFunCaller :: Natural +simpleFunCaller = simpleFun 1 + +singleEven :: (Natural -> Natural) -> Natural +singleEven _ = 0 + +doubleOdd :: + Natural -> + ((Natural -> Natural) -> Natural) -> + ((Natural -> Natural) -> Natural) -> Natural +doubleOdd _ _ _ = 0 + +tripleOdd :: + ((Natural -> ((Natural -> Natural) -> Natural) -> Natural) -> + Natural) + -> Natural +tripleOdd _ = 0 + +data Dat = Con Natural + | NoneErasedCon Natural + +data Rec = Rec{recFst :: Natural, recSnd :: Natural} + +newtype Newt = Newt{theField :: Natural -> Natural} + +newtype NoneErasedNewt = NoneErasedNewt{noneErasedField :: Natural} + +data ErasedField = ErasedField{erasedFst :: Natural} + +listErased :: [(Natural -> Natural) -> Natural] -> Natural +listErased _ = 0 + +eraseTCB :: Natural -> Natural +eraseTCB n = 0 + +fUnzip :: Functor f => f (a, b) -> (f a, f b) +fUnzip xs = (fmap (\ r -> fst r) xs, fmap (\ r -> snd r) xs) + 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..dacf50c2 --- /dev/null +++ b/test/golden/RuntimeCheckUnboxed.err @@ -0,0 +1,2 @@ +test/Fail/RuntimeCheckUnboxed.agda:9,8-20 +Cannot make record NotUnboxable 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..1e4df68d --- /dev/null +++ b/test/golden/RuntimeCheckUseCases.hs @@ -0,0 +1,18 @@ +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 + | otherwise = error "Runtime check failed: decIsFalse (x < y)" + +headOfNonEmpty :: [Natural] -> Natural +headOfNonEmpty xs + | decNonEmpty xs = RuntimeCheckUseCases.PostRtc.headOfNonEmpty xs + | otherwise = 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 +