Initial strict runtime check

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,

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 #-}

src/Agda2Hs/Compile.hs

@@ -24,28 +24,30 @@ 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
   , 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
@@ -61,20 +63,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
@@ -86,39 +90,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

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 no erased, provide signature for smart constructor if it exists
+    checkRtc tel smartQName (hsVar conString) >>= \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 []