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 {_} {_} {_} {_} {[]} = 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 #-}

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

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 []