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