summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Translation/InternalToAbstract.hs')
-rw-r--r--src/full/Agda/Syntax/Translation/InternalToAbstract.hs539
1 files changed, 280 insertions, 259 deletions
diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
index da47b35..1333506 100644
--- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
{-|
Translating from internal syntax to abstract syntax. Enables nice
@@ -51,6 +50,7 @@ import Agda.Syntax.Internal as I
import qualified Agda.Utils.VarSet as VSet
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
+import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses(Fail))
@@ -99,6 +99,22 @@ reifyIArg' e = flip Common.Arg (unArg e) <$> reify (argInfo e)
reifyIArgs' :: [I.Arg e] -> TCM [A.Arg e]
reifyIArgs' = mapM reifyIArg'
+-- Composition of reified eliminations ------------------------------------
+
+elims :: Expr -> [I.Elim' Expr] -> TCM Expr
+elims e [] = return e
+elims e (I.Apply arg : es) = do
+ arg <- reifyIArg' arg
+ elims (A.App exprInfo e $ fmap unnamed arg) es
+elims e (I.Proj d : es) = elims (A.App exprInfo (A.Proj d) $ defaultNamedArg e) es
+
+reifyIElim :: Reify i a => I.Elim' i -> TCM (I.Elim' a)
+reifyIElim (I.Apply i) = I.Apply <$> traverse reify i
+reifyIElim (I.Proj d) = return $ I.Proj d
+
+reifyIElims :: Reify i a => [I.Elim' i] -> TCM [I.Elim' a]
+reifyIElims = mapM reifyIElim
+
-- Omitting information ---------------------------------------------------
exprInfo :: ExprInfo
@@ -146,13 +162,18 @@ instance Reify MetaId Expr where
caseMaybeM (isInteractionMeta x) underscore $ \ ii@InteractionId{} ->
return $ A.QuestionMark (mi' {metaNumber = Just n}) ii
+-- Does not print with-applications correctly:
+-- instance Reify DisplayTerm Expr where
+-- reifyWhen = reifyWhenE
+-- reify d = reifyTerm False $ dtermToTerm d
+
instance Reify DisplayTerm Expr where
reifyWhen = reifyWhenE
reify d = case d of
DTerm v -> reifyTerm False v
DDot v -> reify v
DCon c vs -> apps (A.Con (AmbQ [conName c])) =<< reifyIArgs vs
- DDef f vs -> apps (A.Def f) =<< reifyIArgs vs
+ DDef f es -> elims (A.Def f) =<< reifyIElims es
DWithApp u us vs -> do
(e, es) <- reify (u, us)
reifyApp (if null es then e else A.WithApp exprInfo e es) vs
@@ -164,7 +185,7 @@ instance Reify DisplayTerm Expr where
reifyDisplayForm :: QName -> I.Args -> TCM A.Expr -> TCM A.Expr
reifyDisplayForm f vs fallback = do
ifNotM displayFormsEnabled fallback $ {- else -} do
- caseMaybeM (liftTCM $ displayForm f vs) fallback reify
+ caseMaybeM (liftTCM $ displayForm f vs) fallback reify
-- | @reifyDisplayFormP@ tries to recursively
-- rewrite a lhs with a display form.
@@ -197,10 +218,12 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d
_ -> return lhs
where
+ -- Andreas, 2015-05-03: Ulf, please comment on what
+ -- is the idea behind okDisplayForm.
okDisplayForm (DWithApp d ds []) =
okDisplayForm d && all okDisplayTerm ds
okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
- okDisplayForm (DDef f vs) = all okDArg vs
+ okDisplayForm (DDef f es) = all okDElim es
okDisplayForm DDot{} = False
okDisplayForm DCon{} = False
okDisplayForm DTerm{} = True -- False?
@@ -212,7 +235,8 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okDisplayTerm DDef{} = False
okDisplayTerm _ = False
- okDArg = okDisplayTerm . unArg
+ okDElim (I.Apply v) = okDisplayTerm $ unArg v
+ okDElim I.Proj{} = True -- True, man, or False? No clue what I am implementing here --Andreas, 2015-05-03
okArg = okTerm . unArg
okElim (I.Apply a) = okArg a
@@ -223,27 +247,27 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okTerm (I.Def x []) = isNoName $ qnameToConcrete x -- Handling wildcards in display forms
okTerm _ = True -- False
- -- Flatten a dt into (parentName, parentArgs, withArgs).
- flattenWith :: DisplayTerm -> (QName, [I.Arg DisplayTerm], [DisplayTerm])
+ -- Flatten a dt into (parentName, parentElims, withArgs).
+ flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [DisplayTerm])
flattenWith (DWithApp d ds1 ds2) = case flattenWith d of
- (f, vs, ds0) -> (f, vs, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
- flattenWith (DDef f vs) = (f, vs, []) -- .^ hacky, but we should only hit this when printing debug info
- flattenWith (DTerm (I.Def f es)) =
- let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
- in (f, map (fmap DTerm) vs, [])
+ (f, es, ds0) -> (f, es, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
+ flattenWith (DDef f es) = (f, es, []) -- .^ hacky, but we should only hit this when printing debug info
+ flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, [])
flattenWith _ = __IMPOSSIBLE__
displayLHS :: [A.Pattern] -> [A.Pattern] -> DisplayTerm -> TCM A.SpineLHS
displayLHS ps wps d = case flattenWith d of
(f, vs, ds) -> do
ds <- mapM termToPat ds
- vs <- mapM argToPat vs
+ vs <- mapM elimToPat vs
vs <- reifyIArgs' vs
return $ SpineLHS i f vs (ds ++ wps)
--- return $ LHS i (LHSHead f vs) (ds ++ wps)
where
ci = ConPatInfo False patNoRange
+
argToPat arg = fmap unnamed <$> traverse termToPat arg
+ elimToPat (I.Apply arg) = argToPat arg
+ elimToPat (I.Proj d) = return $ defaultNamedArg $ A.DefP patNoRange d []
termToPat :: DisplayTerm -> TCM A.Pattern
@@ -302,42 +326,41 @@ instance Reify Term Expr where
reifyTerm :: Bool -> Term -> TCM Expr
reifyTerm expandAnonDefs0 v = do
- hasDisplayForms <- displayFormsEnabled
- -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
- -- (i.e. when we don't care about nice printing)
- let expandAnonDefs = expandAnonDefs0 && hasDisplayForms
- v <- unSpine <$> instantiate v
- case v of
- _ | isHackReifyToMeta v -> return $ A.Underscore emptyMetaInfo
- I.Var n es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
- reifyApp (A.Var x) vs
- I.Def x es -> do
+ -- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
+ -- (i.e. when we don't care about nice printing)
+ expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
+ v <- unSpine <$> instantiate v
+ case v of
+ _ | isHackReifyToMeta v -> return $ A.Underscore emptyMetaInfo
+ I.Var n es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- reifyDisplayForm x vs $ reifyDef expandAnonDefs x vs
- I.Con c vs -> do
- let x = conName c
- isR <- isGeneratedRecordConstructor x
- case isR of
- True -> do
- showImp <- showImplicitArguments
- let keep (a, v) = showImp || notHidden a
- r <- getConstructorData x
- xs <- getRecordFieldNames r
- vs <- map unArg <$> reifyIArgs vs
- return $ A.Rec exprInfo $ map (unArg *** id) $ filter keep $ zip xs vs
- False -> reifyDisplayForm x vs $ do
- ci <- getConstInfo x
- let Constructor{conPars = np} = theDef ci
- -- if we are the the module that defines constructor x
- -- then we have to drop at least the n module parameters
- n <- getDefFreeVars x
- -- the number of parameters is greater (if the data decl has
- -- extra parameters) or equal (if not) to n
- when (n > np) __IMPOSSIBLE__
- let h = A.Con (AmbQ [x])
- if null vs then return h else do
+ x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
+ reifyApp (A.Var x) vs
+ I.Def x es -> do
+ let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
+ reifyDisplayForm x vs $ reifyDef expandAnonDefs x vs
+ I.Con c vs -> do
+ let x = conName c
+ isR <- isGeneratedRecordConstructor x
+ case isR of
+ True -> do
+ showImp <- showImplicitArguments
+ let keep (a, v) = showImp || notHidden a
+ r <- getConstructorData x
+ xs <- getRecordFieldNames r
+ vs <- map unArg <$> reifyIArgs vs
+ return $ A.Rec exprInfo $ map (unArg *** id) $ filter keep $ zip xs vs
+ False -> reifyDisplayForm x vs $ do
+ ci <- getConstInfo x
+ let Constructor{conPars = np} = theDef ci
+ -- if we are the the module that defines constructor x
+ -- then we have to drop at least the n module parameters
+ n <- getDefFreeVars x
+ -- the number of parameters is greater (if the data decl has
+ -- extra parameters) or equal (if not) to n
+ when (n > np) __IMPOSSIBLE__
+ let h = A.Con (AmbQ [x])
+ if null vs then return h else do
es <- reifyIArgs vs
-- Andreas, 2012-04-20: do not reify parameter arguments of constructor
-- if the first regular constructor argument is hidden
@@ -379,86 +402,86 @@ reifyTerm expandAnonDefs0 v = do
]
napps h $ genericDrop (n - np) $ nameFirstIfHidden doms es
-}
--- I.Lam info b | isAbsurdBody b -> return $ A.AbsurdLam exprInfo $ getHiding info
- I.Lam info b -> do
- (x,e) <- reify b
- info <- reify info
- return $ A.Lam exprInfo (DomainFree info x) e
- -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
- I.Lit l -> reify l
- I.Level l -> reify l
- I.Pi a b -> case b of
- NoAbs _ b'
- | notHidden a -> uncurry (A.Fun $ exprInfo) <$> reify (a, b')
- -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
- -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
- -- and (b) the name of the binder might matter.
- -- See issue 951 (a) and 952 (b).
- | otherwise -> mkPi b =<< reify a
- b -> mkPi b =<< do
- ifM (domainFree a (absBody b))
- {- then -} (Common.Arg <$> reify (domInfo a) <*> pure underscore)
- {- else -} (reify a)
- where
- mkPi b (Common.Arg info a) = do
- (x, b) <- reify b
- return $ A.Pi exprInfo [TypedBindings noRange $ Common.Arg info (TBind noRange [x] a)] b
- -- We can omit the domain type if it doesn't have any free variables
- -- and it's mentioned in the target type.
- domainFree a b = do
- df <- asks envPrintDomainFreePi
- return $ and [df, freeIn 0 b, VSet.null $ allVars $ freeVars a]
-
- I.Sort s -> reify s
- I.MetaV x es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- x' <- reify x
- apps x' =<< reifyIArgs vs
- I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
- I.Shared p -> reifyTerm expandAnonDefs $ derefPtr p
- I.ExtLam cls args -> do
- x <- freshName_ "extlam"
- reifyExtLam (qnameFromList [x]) 0 cls (map (fmap unnamed) args)
- where
- -- Andreas, 2012-10-20 expand a copy in an anonymous module
- -- to improve error messages.
- -- Don't do this if we have just expanded into a display form,
- -- otherwise we loop!
- reifyDef :: Bool -> QName -> I.Args -> TCM Expr
- reifyDef True x@(QName m name) vs | A.isAnonymousModuleName m = do
- r <- reduceDefCopy x vs
- case r of
- YesReduction _ v -> do
- reportSLn "reify.anon" 60 $ unlines
- [ "reduction on defined ident. in anonymous module"
- , "x = " ++ show x
- , "v = " ++ show v
- ]
- reify v
- NoReduction () -> do
- reportSLn "reify.anon" 60 $ unlines
- [ "no reduction on defined ident. in anonymous module"
- , "x = " ++ show x
- , "vs = " ++ show vs
- ]
- reifyDef' x vs
- reifyDef _ x vs = reifyDef' x vs
-
- reifyDef' :: QName -> I.Args -> TCM Expr
- reifyDef' x@(QName _ name) vs = do
- -- We should drop this many arguments from the local context.
- n <- getDefFreeVars x
- mdefn <- liftTCM $ (Just <$> getConstInfo x) `catchError` \_ -> return Nothing
- -- check if we have an absurd lambda
- let reifyAbsurdLambda cont =
- case theDef <$> mdefn of
- Just Function{ funCompiled = Just Fail, funClauses = [cl] }
- | isAbsurdLambdaName x -> do
- -- get hiding info from last pattern, which should be ()
- let h = getHiding $ last (clausePats cl)
- apps (A.AbsurdLam exprInfo h) =<< reifyIArgs vs
- _ -> cont
- reifyAbsurdLambda $ do
+-- I.Lam info b | isAbsurdBody b -> return $ A.AbsurdLam exprInfo $ getHiding info
+ I.Lam info b -> do
+ (x,e) <- reify b
+ info <- reify info
+ return $ A.Lam exprInfo (DomainFree info x) e
+ -- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
+ I.Lit l -> reify l
+ I.Level l -> reify l
+ I.Pi a b -> case b of
+ NoAbs _ b'
+ | notHidden a -> uncurry (A.Fun $ exprInfo) <$> reify (a, b')
+ -- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
+ -- since (a) the syntax {A} -> B or {{A}} -> B is not legal
+ -- and (b) the name of the binder might matter.
+ -- See issue 951 (a) and 952 (b).
+ | otherwise -> mkPi b =<< reify a
+ b -> mkPi b =<< do
+ ifM (domainFree a (absBody b))
+ {- then -} (Common.Arg <$> reify (domInfo a) <*> pure underscore)
+ {- else -} (reify a)
+ where
+ mkPi b (Common.Arg info a) = do
+ (x, b) <- reify b
+ return $ A.Pi exprInfo [TypedBindings noRange $ Common.Arg info (TBind noRange [pure x] a)] b
+ -- We can omit the domain type if it doesn't have any free variables
+ -- and it's mentioned in the target type.
+ domainFree a b = do
+ df <- asks envPrintDomainFreePi
+ return $ and [df, freeIn 0 b, VSet.null $ allVars $ freeVars a]
+
+ I.Sort s -> reify s
+ I.MetaV x es -> do
+ let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
+ x' <- reify x
+ apps x' =<< reifyIArgs vs
+ I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
+ I.Shared p -> reifyTerm expandAnonDefs $ derefPtr p
+ I.ExtLam cls args -> do
+ x <- freshName_ "extlam"
+ reifyExtLam (qnameFromList [x]) 0 cls (map (fmap unnamed) args)
+ where
+ -- Andreas, 2012-10-20 expand a copy in an anonymous module
+ -- to improve error messages.
+ -- Don't do this if we have just expanded into a display form,
+ -- otherwise we loop!
+ reifyDef :: Bool -> QName -> I.Args -> TCM Expr
+ reifyDef True x@(QName m name) vs | A.isAnonymousModuleName m = do
+ r <- reduceDefCopy x vs
+ case r of
+ YesReduction _ v -> do
+ reportSLn "reify.anon" 60 $ unlines
+ [ "reduction on defined ident. in anonymous module"
+ , "x = " ++ show x
+ , "v = " ++ show v
+ ]
+ reify v
+ NoReduction () -> do
+ reportSLn "reify.anon" 60 $ unlines
+ [ "no reduction on defined ident. in anonymous module"
+ , "x = " ++ show x
+ , "vs = " ++ show vs
+ ]
+ reifyDef' x vs
+ reifyDef _ x vs = reifyDef' x vs
+
+ reifyDef' :: QName -> I.Args -> TCM Expr
+ reifyDef' x@(QName _ name) vs = do
+ -- We should drop this many arguments from the local context.
+ n <- getDefFreeVars x
+ mdefn <- liftTCM $ (Just <$> getConstInfo x) `catchError` \_ -> return Nothing
+ -- check if we have an absurd lambda
+ let reifyAbsurdLambda cont =
+ case theDef <$> mdefn of
+ Just Function{ funCompiled = Just Fail, funClauses = [cl] }
+ | isAbsurdLambdaName x -> do
+ -- get hiding info from last pattern, which should be ()
+ let h = getHiding $ last (clausePats cl)
+ apps (A.AbsurdLam exprInfo h) =<< reifyIArgs vs
+ _ -> cont
+ reifyAbsurdLambda $ do
(pad, vs :: [I.NamedArg Term]) <- do
case mdefn of
Nothing -> return ([], map (fmap unnamed) $ genericDrop n vs)
@@ -475,7 +498,7 @@ reifyTerm expandAnonDefs0 v = do
-- These are the dropped projection arguments
(np, pad, dom) <-
case def of
- Function{ funProjection = Just Projection{ projIndex = np } } -> do
+ Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do
TelV tel _ <- telView (defType defn)
scope <- getScope
let (as, dom:_) = splitAt (np - 1) $ telToList tel
@@ -507,14 +530,14 @@ reifyTerm expandAnonDefs0 v = do
let apps = foldl' (\e a -> A.App exprInfo e (fmap unnamed a))
napps (A.Def x `apps` pad) =<< reifyIArgs vs
- reifyExtLam :: QName -> Int -> [I.Clause] -> [I.NamedArg Term] -> TCM Expr
- reifyExtLam x n cls vs = do
- reportSLn "reify.def" 10 $ "reifying extended lambda with definition: x = " ++ show x
- -- drop lambda lifted arguments
- cls <- mapM (reify . QNamed x . dropArgs n) $ cls
- let cx = nameConcrete $ qnameName x
- dInfo = mkDefInfo cx defaultFixity' PublicAccess ConcreteDef (getRange x)
- napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
+ reifyExtLam :: QName -> Int -> [I.Clause] -> [I.NamedArg Term] -> TCM Expr
+ reifyExtLam x n cls vs = do
+ reportSLn "reify.def" 10 $ "reifying extended lambda with definition: x = " ++ show x
+ -- drop lambda lifted arguments
+ cls <- mapM (reify . QNamed x . dropArgs n) $ cls
+ let cx = nameConcrete $ qnameName x
+ dInfo = mkDefInfo cx defaultFixity' PublicAccess ConcreteDef (getRange x)
+ napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
-- | @nameFirstIfHidden n (a1->...an->{x:a}->b) ({e} es) = {x = e} es@
nameFirstIfHidden :: [I.Dom (ArgName, t)] -> [I.Arg a] -> [I.NamedArg a]
@@ -647,95 +670,95 @@ stripImplicits :: ([A.NamedArg A.Pattern], [A.Pattern]) ->
TCM ([A.NamedArg A.Pattern], [A.Pattern])
stripImplicits (ps, wps) = do -- v if show-implicit we don't need the names
ifM showImplicitArguments (return (map (unnamed . namedThing <$>) ps, wps)) $ do
- let vars = dotVars (ps, wps)
- reportSLn "reify.implicit" 30 $ unlines
- [ "stripping implicits"
- , " ps = " ++ show ps
- , " wps = " ++ show wps
- , " vars = " ++ show vars
- ]
- let allps = ps ++ map defaultNamedArg wps
- sps = blankDots $ foldl (.) (strip Set.empty) (map rearrangeBinding $ Set.toList vars) $ allps
- (ps', wps') = splitAt (length sps - length wps) sps
- reportSLn "reify.implicit" 30 $ unlines
- [ " ps' = " ++ show ps'
- , " wps' = " ++ show (map namedArg wps')
- ]
- return (ps', map namedArg wps')
- where
- argsVars = Set.unions . map argVars
- argVars = patVars . namedArg
- patVars p = case p of
- A.VarP x -> Set.singleton x
- A.ConP _ _ ps -> argsVars ps
- A.DefP _ _ ps -> Set.empty
- A.DotP _ e -> Set.empty
- A.WildP _ -> Set.empty
- A.AbsurdP _ -> Set.empty
- A.LitP _ -> Set.empty
- A.ImplicitP _ -> Set.empty
- A.AsP _ _ p -> patVars p
- A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- Set.empty
-
- -- Replace dot variables by ._ if they use implicitly bound variables. This
- -- is slightly nicer than making the implicts explicit.
- blankDots ps = (map . fmap . fmap . fmap) blank ps
- where
- bound = argsVars ps
- blank e | Set.null (Set.difference (dotVars e) bound) = e
- | otherwise = A.Underscore emptyMetaInfo
-
- -- Pick the "best" place to bind the variable. Best in this case
- -- is the left-most explicit binding site. But, of course we can't
- -- do this since binding site might be forced by a parent clause.
- -- Why? Because the binding site we pick might not exist in the
- -- generated with function if it corresponds to a dot pattern.
- rearrangeBinding x ps = ps
-
- strip dvs ps = stripArgs True ps
- where
- stripArgs _ [] = []
- stripArgs fixedPos (a : as) =
- case getHiding a of
- Hidden | canStrip a as -> stripArgs False as
- Instance | canStrip a as -> stripArgs False as
- _ -> stripName fixedPos (stripArg a) :
- stripArgs True as
-
- stripName True = fmap (unnamed . namedThing)
- stripName False = id
-
- canStrip a as = and
- [ varOrDot p
- , noInterestingBindings p
- , all (flip canStrip []) $ takeWhile isUnnamedHidden as
- ]
- where p = namedArg a
-
- isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
-
- stripArg a = fmap (fmap stripPat) a
-
- stripPat p = case p of
- A.VarP _ -> p
- A.ConP i c ps -> A.ConP i c $ stripArgs True ps
- A.DefP _ _ _ -> p
- A.DotP _ e -> p
- A.WildP _ -> p
- A.AbsurdP _ -> p
- A.LitP _ -> p
- A.ImplicitP _ -> p
- A.AsP i x p -> A.AsP i x $ stripPat p
- A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- p
-
- noInterestingBindings p =
- Set.null $ dvs `Set.intersection` patVars p
-
- varOrDot A.VarP{} = True
- varOrDot A.WildP{} = True
- varOrDot A.DotP{} = True
- varOrDot A.ImplicitP{} = True
- varOrDot _ = False
+ let vars = dotVars (ps, wps)
+ reportSLn "reify.implicit" 30 $ unlines
+ [ "stripping implicits"
+ , " ps = " ++ show ps
+ , " wps = " ++ show wps
+ , " vars = " ++ show vars
+ ]
+ let allps = ps ++ map defaultNamedArg wps
+ sps = blankDots $ foldl (.) (strip Set.empty) (map rearrangeBinding $ Set.toList vars) $ allps
+ (ps', wps') = splitAt (length sps - length wps) sps
+ reportSLn "reify.implicit" 30 $ unlines
+ [ " ps' = " ++ show ps'
+ , " wps' = " ++ show (map namedArg wps')
+ ]
+ return (ps', map namedArg wps')
+ where
+ argsVars = Set.unions . map argVars
+ argVars = patVars . namedArg
+ patVars p = case p of
+ A.VarP x -> Set.singleton x
+ A.ConP _ _ ps -> argsVars ps
+ A.DefP _ _ ps -> Set.empty
+ A.DotP _ e -> Set.empty
+ A.WildP _ -> Set.empty
+ A.AbsurdP _ -> Set.empty
+ A.LitP _ -> Set.empty
+ A.ImplicitP _ -> Set.empty
+ A.AsP _ _ p -> patVars p
+ A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- Set.empty
+
+ -- Replace dot variables by ._ if they use implicitly bound variables. This
+ -- is slightly nicer than making the implicts explicit.
+ blankDots ps = (map . fmap . fmap . fmap) blank ps
+ where
+ bound = argsVars ps
+ blank e | Set.null (Set.difference (dotVars e) bound) = e
+ | otherwise = A.Underscore emptyMetaInfo
+
+ -- Pick the "best" place to bind the variable. Best in this case
+ -- is the left-most explicit binding site. But, of course we can't
+ -- do this since binding site might be forced by a parent clause.
+ -- Why? Because the binding site we pick might not exist in the
+ -- generated with function if it corresponds to a dot pattern.
+ rearrangeBinding x ps = ps
+
+ strip dvs ps = stripArgs True ps
+ where
+ stripArgs _ [] = []
+ stripArgs fixedPos (a : as) =
+ case getHiding a of
+ Hidden | canStrip a as -> stripArgs False as
+ Instance | canStrip a as -> stripArgs False as
+ _ -> stripName fixedPos (stripArg a) :
+ stripArgs True as
+
+ stripName True = fmap (unnamed . namedThing)
+ stripName False = id
+
+ canStrip a as = and
+ [ varOrDot p
+ , noInterestingBindings p
+ , all (flip canStrip []) $ takeWhile isUnnamedHidden as
+ ]
+ where p = namedArg a
+
+ isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
+
+ stripArg a = fmap (fmap stripPat) a
+
+ stripPat p = case p of
+ A.VarP _ -> p
+ A.ConP i c ps -> A.ConP i c $ stripArgs True ps
+ A.DefP _ _ _ -> p
+ A.DotP _ e -> p
+ A.WildP _ -> p
+ A.AbsurdP _ -> p
+ A.LitP _ -> p
+ A.ImplicitP _ -> p
+ A.AsP i x p -> A.AsP i x $ stripPat p
+ A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- p
+
+ noInterestingBindings p =
+ Set.null $ dvs `Set.intersection` patVars p
+
+ varOrDot A.VarP{} = True
+ varOrDot A.WildP{} = True
+ varOrDot A.DotP{} = True
+ varOrDot A.ImplicitP{} = True
+ varOrDot _ = False
-- | @dotVars ps@ gives all the variables inside of dot patterns of @ps@
-- It is only invoked for patternish things. (Ulf O-tone!)
@@ -820,7 +843,7 @@ instance DotVars RHS where
dotVars (RHS e) = dotVars e
dotVars AbsurdRHS = Set.empty
dotVars (WithRHS _ es clauses) = __IMPOSSIBLE__ -- NZ
- dotVars (RewriteRHS _ es rhs _) = __IMPOSSIBLE__ -- NZ
+ dotVars (RewriteRHS xes rhs _) = __IMPOSSIBLE__ -- NZ
instance DotVars TypedBindings where
dotVars (TypedBindings _ bs) = dotVars bs
@@ -858,14 +881,14 @@ reifyPatterns tel perm ps = evalStateT (reifyArgs ps) 0
lift $ A.VarP <$> nameOfBV (size tel - 1 - j)
I.DotP v -> do
t <- lift $ reify v
- tick
+ _ <- tick
let vars = Set.map show (dotVars t)
t' = if Set.member "()" vars then underscore else t
return $ A.DotP patNoRange t'
I.LitP l -> return $ A.LitP l
I.ProjP d -> return $ A.DefP patNoRange d []
- I.ConP c mt ps -> A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
- where ci = flip ConPatInfo patNoRange $ maybe False fst mt
+ I.ConP c cpi ps -> A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
+ where ci = flip ConPatInfo patNoRange $ fromMaybe False $ I.conPRecord cpi
instance Reify NamedClause A.Clause where
reify (QNamed f (I.Clause _ tel perm ps body _)) = addCtxTel tel $ do
@@ -893,21 +916,24 @@ instance Reify Type Expr where
instance Reify Sort Expr where
reifyWhen = reifyWhenE
- reify s =
- do s <- instantiateFull s
- case s of
- I.Type (I.Max []) -> return $ A.Set exprInfo 0
- I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set exprInfo n
- I.Type a -> do
- a <- reify a
- return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
- I.Prop -> return $ A.Prop exprInfo
- I.Inf -> A.Var <$> freshName_ ("Setω" :: String)
- I.DLub s1 s2 -> do
- lub <- freshName_ ("dLub" :: String) -- TODO: hack
- (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
- let app x y = A.App exprInfo x (defaultNamedArg y)
- return $ A.Var lub `app` e1 `app` e2
+ reify s = do
+ s <- instantiateFull s
+ case s of
+ I.Type (I.Max []) -> return $ A.Set exprInfo 0
+ I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set exprInfo n
+ I.Type a -> do
+ a <- reify a
+ return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
+ I.Prop -> return $ A.Prop exprInfo
+ I.Inf -> A.Var <$> freshName_ ("Setω" :: String)
+ I.SizeUniv -> do
+ I.Def sizeU [] <- primSizeUniv
+ return $ A.Def sizeU
+ I.DLub s1 s2 -> do
+ lub <- freshName_ ("dLub" :: String) -- TODO: hack
+ (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
+ let app x y = A.App exprInfo x (defaultNamedArg y)
+ return $ A.Var lub `app` e1 `app` e2
instance Reify Level Expr where
reifyWhen = reifyWhenE
@@ -932,7 +958,7 @@ instance Reify I.Telescope A.Telescope where
Common.Arg info e <- reify arg
(x,bs) <- reify tel
let r = getRange e
- return $ TypedBindings r (Common.Arg info (TBind r [x] e)) : bs
+ return $ TypedBindings r (Common.Arg info (TBind r [pure x] e)) : bs
instance Reify I.ArgInfo A.ArgInfo where
reify i = flip (mapArgInfoColors.const) i <$> reify (argInfoColors i)
@@ -951,8 +977,3 @@ instance (Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1,i2,i3) (a1,a2,a3)
instance (Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1,i2,i3,i4) (a1,a2,a3,a4) where
reify (x,y,z,w) = (,,,) <$> reify x <*> reify y <*> reify z <*> reify w
-
-instance (Reify t t', Reify a a')
- => Reify (Judgement t a) (Judgement t' a') where
- reify (HasType i t) = HasType <$> reify i <*> reify t
- reify (IsSort i t) = IsSort <$> reify i <*> reify t