1{-# OPTIONS_GHC -fwarn-missing-signatures #-} 2 3module Agda.Syntax.Translation.ReflectedToAbstract where 4 5import Control.Arrow ( (***) ) 6import Control.Monad.Except 7import Control.Monad.Reader 8 9import Data.Maybe 10import Data.Set (Set) 11import qualified Data.Set as Set 12import Data.Text (Text) 13import qualified Data.Text as Text 14 15import Agda.Syntax.Literal 16import Agda.Syntax.Position 17import Agda.Syntax.Info 18import Agda.Syntax.Common 19import Agda.Syntax.Abstract as A hiding (Apply) 20import Agda.Syntax.Abstract.Pattern 21import Agda.Syntax.Reflected as R 22import Agda.Syntax.Internal (Dom,Dom'(..)) 23 24import Agda.Interaction.Options (optUseUnicode, UnicodeOrAscii(..)) 25import Agda.TypeChecking.Monad as M hiding (MetaInfo) 26import Agda.Syntax.Scope.Monad (getCurrentModule) 27 28import Agda.Utils.Impossible 29import Agda.Utils.Maybe 30import Agda.Utils.Monad 31import Agda.Utils.List 32import Agda.Utils.List1 (List1, pattern (:|)) 33import qualified Agda.Utils.List1 as List1 34import Agda.Utils.Null 35import Agda.Utils.Pretty 36import Agda.Utils.Functor 37import Agda.Utils.Singleton 38import Agda.Utils.Size 39 40type Vars = [(Name,R.Type)] 41 42type MonadReflectedToAbstract m = 43 ( MonadReader Vars m 44 , MonadFresh NameId m 45 , MonadError TCErr m 46 , MonadTCEnv m 47 , ReadTCState m 48 , HasOptions m 49 , HasBuiltins m 50 , HasConstInfo m 51 ) 52 53-- | Adds a new unique name to the current context. 54-- NOTE: See @chooseName@ in @Agda.Syntax.Translation.AbstractToConcrete@ for similar logic. 55-- NOTE: See @freshConcreteName@ in @Agda.Syntax.Scope.Monad@ also for similar logic. 56withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a 57withName s = withVar s R.Unknown 58 59withVar :: MonadReflectedToAbstract m => String -> R.Type -> (Name -> m a) -> m a 60withVar s t f = do 61 name <- freshName_ s 62 ctx <- asks $ map $ nameConcrete . fst 63 glyphMode <- optUseUnicode <$> M.pragmaOptions 64 let freshNameMode = case glyphMode of 65 UnicodeOk -> A.UnicodeSubscript 66 AsciiOnly -> A.AsciiCounter 67 let name' = head $ filter (notTaken ctx) $ iterate (nextName freshNameMode) name 68 local ((name,t):) $ f name' 69 where 70 notTaken xs x = isNoName x || nameConcrete x `notElem` xs 71 72withNames :: MonadReflectedToAbstract m => [String] -> ([Name] -> m a) -> m a 73withNames ss = withVars $ zip ss $ repeat R.Unknown 74 75withVars :: MonadReflectedToAbstract m => [(String, R.Type)] -> ([Name] -> m a) -> m a 76withVars ss f = case ss of 77 [] -> f [] 78 ((s,t):ss) -> withVar s t $ \n -> withVars ss $ \ns -> f (n:ns) 79 80-- | Returns the name and type of the variable with the given de Bruijn index. 81askVar :: MonadReflectedToAbstract m => Int -> m (Maybe (Name,R.Type)) 82askVar i = reader (!!! i) 83 84askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name) 85askName i = fmap fst <$> askVar i 86 87class ToAbstract r where 88 type AbsOfRef r 89 toAbstract :: MonadReflectedToAbstract m => r -> m (AbsOfRef r) 90 91 default toAbstract 92 :: (Traversable t, ToAbstract s, t s ~ r, t (AbsOfRef s) ~ (AbsOfRef r)) 93 => MonadReflectedToAbstract m => r -> m (AbsOfRef r) 94 toAbstract = traverse toAbstract 95 96-- | Translate reflected syntax to abstract, using the names from the current typechecking context. 97toAbstract_ :: 98 (ToAbstract r 99 , MonadFresh NameId m 100 , MonadError TCErr m 101 , MonadTCEnv m 102 , ReadTCState m 103 , HasOptions m 104 , HasBuiltins m 105 , HasConstInfo m 106 ) => r -> m (AbsOfRef r) 107toAbstract_ = withShowAllArguments . toAbstractWithoutImplicit 108 109-- | Drop implicit arguments unless --show-implicit is on. 110toAbstractWithoutImplicit :: 111 (ToAbstract r 112 , MonadFresh NameId m 113 , MonadError TCErr m 114 , MonadTCEnv m 115 , ReadTCState m 116 , HasOptions m 117 , HasBuiltins m 118 , HasConstInfo m 119 ) => r -> m (AbsOfRef r) 120toAbstractWithoutImplicit x = do 121 xs <- getContextNames 122 let ctx = zip xs $ repeat R.Unknown 123 runReaderT (toAbstract x) ctx 124 125instance ToAbstract r => ToAbstract (Named name r) where 126 type AbsOfRef (Named name r) = Named name (AbsOfRef r) 127 128instance ToAbstract r => ToAbstract (Arg r) where 129 type AbsOfRef (Arg r) = NamedArg (AbsOfRef r) 130 toAbstract (Arg i x) = Arg i <$> toAbstract (unnamed x) 131 132instance ToAbstract r => ToAbstract [Arg r] where 133 type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)] 134 135-- instance ToAbstract r Expr => ToAbstract (Dom r, Name) (A.TypedBinding) where 136instance (ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) where 137 type AbsOfRef (Dom r, Name) = A.TypedBinding 138 toAbstract (Dom{domInfo = i,unDom = x, domTactic = tac}, name) = do 139 dom <- toAbstract x 140 return $ mkTBind noRange (singleton $ unnamedArg i $ mkBinder_ name) dom 141 142instance ToAbstract (Expr, Elim) where 143 type AbsOfRef (Expr, Elim) = Expr 144 toAbstract (f, Apply arg) = do 145 arg <- toAbstract arg 146 showImp <- showImplicitArguments 147 return $ if showImp || visible arg 148 then App (setOrigin Reflected defaultAppInfo_) f arg 149 else f 150 151instance ToAbstract (Expr, Elims) where 152 type AbsOfRef (Expr, Elims) = Expr 153 toAbstract (f, elims) = foldM (curry toAbstract) f elims 154 155instance ToAbstract r => ToAbstract (R.Abs r) where 156 type AbsOfRef (R.Abs r) = (AbsOfRef r, Name) 157 toAbstract (Abs s x) = withName s' $ \name -> (,) <$> toAbstract x <*> return name 158 where s' = if (isNoName s) then "z" else s -- TODO: only do this when var is free 159 160instance ToAbstract Literal where 161 type AbsOfRef Literal = Expr 162 toAbstract l = return $ A.Lit empty l 163 164instance ToAbstract Term where 165 type AbsOfRef Term = Expr 166 toAbstract = \case 167 R.Var i es -> do 168 name <- mkVarName i 169 toAbstract (A.Var name, es) 170 R.Con c es -> toAbstract (A.Con (unambiguous $ killRange c), es) 171 R.Def f es -> do 172 af <- mkDef (killRange f) 173 toAbstract (af, es) 174 R.Lam h t -> do 175 (e, name) <- toAbstract t 176 let info = setHiding h $ setOrigin Reflected defaultArgInfo 177 return $ A.Lam exprNoRange (mkDomainFree $ unnamedArg info $ mkBinder_ name) e 178 R.ExtLam cs es -> do 179 name <- freshName_ extendedLambdaName 180 m <- getCurrentModule 181 let qname = qualify m name 182 cname = nameConcrete name 183 defInfo = mkDefInfo cname noFixity' PublicAccess ConcreteDef noRange 184 cs <- toAbstract $ fmap (QNamed qname) cs 185 toAbstract 186 (A.ExtendedLam exprNoRange defInfo defaultErased qname cs, es) 187 R.Pi a b -> do 188 (b, name) <- toAbstract b 189 a <- toAbstract (a, name) 190 return $ A.Pi exprNoRange (singleton a) b 191 R.Sort s -> toAbstract s 192 R.Lit l -> toAbstract l 193 R.Meta x es -> toAbstract (A.Underscore info, es) 194 where info = emptyMetaInfo{ metaNumber = Just x } 195 R.Unknown -> return $ Underscore emptyMetaInfo 196 197mkDef :: HasConstInfo m => QName -> m A.Expr 198mkDef f = 199 ifM (isMacro . theDef <$> getConstInfo f) 200 (return $ A.Macro f) 201 (return $ A.Def f) 202 203mkApp :: Expr -> Expr -> Expr 204mkApp e1 e2 = App (setOrigin Reflected defaultAppInfo_) e1 $ defaultNamedArg e2 205 206 207mkVar :: MonadReflectedToAbstract m => Int -> m (Name, R.Type) 208mkVar i = ifJustM (askVar i) return $ do 209 cxt <- getContextTelescope 210 names <- asks $ drop (size cxt) . reverse . map fst 211 withShowAllArguments' False $ typeError $ DeBruijnIndexOutOfScope i cxt names 212 213mkVarName :: MonadReflectedToAbstract m => Int -> m Name 214mkVarName i = fst <$> mkVar i 215 216annotatePattern :: MonadReflectedToAbstract m => Int -> R.Type -> A.Pattern -> m A.Pattern 217annotatePattern _ R.Unknown p = return p 218annotatePattern i t p = local (drop $ i + 1) $ do 219 t <- toAbstract t -- go into the right context for translating the type 220 return $ A.AnnP patNoRange t p 221 222instance ToAbstract Sort where 223 type AbsOfRef Sort = Expr 224 toAbstract s = do 225 setName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSet 226 propName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinProp 227 infName <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSetOmega 228 case s of 229 SetS x -> mkApp (A.Def setName) <$> toAbstract x 230 LitS x -> return $ A.Def' setName $ A.Suffix x 231 PropS x -> mkApp (A.Def propName) <$> toAbstract x 232 PropLitS x -> return $ A.Def' propName $ A.Suffix x 233 InfS x -> return $ A.Def' infName $ A.Suffix x 234 UnknownS -> return $ mkApp (A.Def setName) $ Underscore emptyMetaInfo 235 236instance ToAbstract R.Pattern where 237 type AbsOfRef R.Pattern = A.Pattern 238 toAbstract pat = case pat of 239 R.ConP c args -> do 240 args <- toAbstract args 241 return $ A.ConP (ConPatInfo ConOCon patNoRange ConPatEager) (unambiguous $ killRange c) args 242 R.DotP t -> A.DotP patNoRange <$> toAbstract t 243 R.VarP i -> do 244 (x, t) <- mkVar i 245 annotatePattern i t $ A.VarP $ mkBindName x 246 R.LitP l -> return $ A.LitP patNoRange l 247 R.AbsurdP i -> do 248 (_, t) <- mkVar i 249 annotatePattern i t $ A.AbsurdP patNoRange 250 R.ProjP d -> return $ A.ProjP patNoRange ProjSystem $ unambiguous $ killRange d 251 252instance ToAbstract (QNamed R.Clause) where 253 type AbsOfRef (QNamed R.Clause) = A.Clause 254 255 toAbstract (QNamed name (R.Clause tel pats rhs)) = withVars (map (Text.unpack *** unArg) tel) $ \_ -> do 256 checkClauseTelescopeBindings tel pats 257 pats <- toAbstract pats 258 rhs <- toAbstract rhs 259 let lhs = spineToLhs $ SpineLHS empty name pats 260 return $ A.Clause lhs [] (RHS rhs Nothing) noWhereDecls False 261 toAbstract (QNamed name (R.AbsurdClause tel pats)) = withVars (map (Text.unpack *** unArg) tel) $ \_ -> do 262 checkClauseTelescopeBindings tel pats 263 pats <- toAbstract pats 264 let lhs = spineToLhs $ SpineLHS empty name pats 265 return $ A.Clause lhs [] AbsurdRHS noWhereDecls False 266 267instance ToAbstract [QNamed R.Clause] where 268 type AbsOfRef [QNamed R.Clause] = [A.Clause] 269 toAbstract = traverse toAbstract 270 271instance ToAbstract (List1 (QNamed R.Clause)) where 272 type AbsOfRef (List1 (QNamed R.Clause)) = List1 A.Clause 273 toAbstract = traverse toAbstract 274 275-- | Check that all variables in the telescope are bound in the left-hand side. Since we check the 276-- telescope by attaching type annotations to the pattern variables there needs to be somewhere to 277-- put the annotation. Also, since the lhs is where the variables are actually bound, missing a 278-- binding for a variable that's used later in the telescope causes unbound variable panic 279-- (see #5044). 280checkClauseTelescopeBindings :: MonadReflectedToAbstract m => [(Text, Arg R.Type)] -> [Arg R.Pattern] -> m () 281checkClauseTelescopeBindings tel pats = 282 case reverse [ x | ((x, _), i) <- zip (reverse tel) [0..], not $ Set.member i bs ] of 283 [] -> return () 284 xs -> genericDocError $ ("Missing bindings for telescope variable" <> s) <?> 285 (fsep (punctuate ", " $ map (text . Text.unpack) xs) <> ".") $$ 286 "All variables in the clause telescope must be bound in the left-hand side." 287 where s | length xs == 1 = empty 288 | otherwise = "s" 289 where 290 bs = boundVars pats 291 292 boundVars = Set.unions . map (bound . unArg) 293 bound (R.VarP i) = Set.singleton i 294 bound (R.ConP _ ps) = boundVars ps 295 bound R.DotP{} = Set.empty 296 bound R.LitP{} = Set.empty 297 bound (R.AbsurdP i) = Set.singleton i 298 bound R.ProjP{} = Set.empty 299