1{-# OPTIONS_GHC -fno-warn-orphans #-} 2 3module Agda.Auto.SearchControl where 4 5import Control.Monad 6import Data.IORef 7import Control.Monad.State 8import Data.Maybe (mapMaybe, fromMaybe) 9 10import Agda.Syntax.Common (Hiding(..)) 11import Agda.Auto.NarrowingSearch 12import Agda.Auto.Syntax 13 14import Agda.Utils.Impossible 15 16instance Refinable (ArgList o) (RefInfo o) where 17 refinements _ infos _ = return $ fmap (Move 0) $ 18 [ return ALNil, cons NotHidden, cons Hidden ] 19 ++ if getIsDep infos then [] 20 else [ proj NotHidden, proj Hidden ] 21 22 where 23 24 getIsDep :: [RefInfo o] -> Bool 25 getIsDep (x : xs) = case x of 26 RICheckElim isDep -> isDep 27 _ -> getIsDep xs 28 getIsDep _ = __IMPOSSIBLE__ 29 30 proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o) 31 proj hid = ALProj <$> newPlaceholder <*> newPlaceholder 32 <*> return hid <*> newPlaceholder 33 34 cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o) 35 cons hid = ALCons hid <$> newPlaceholder <*> newPlaceholder 36 37 38data ExpRefInfo o = ExpRefInfo 39 { eriMain :: Maybe (RefInfo o) 40 , eriUnifs :: [RefInfo o] 41 , eriInfTypeUnknown :: Bool 42 , eriIsEliminand :: Bool 43 , eriUsedVars :: Maybe ([UId o], [Elr o]) 44 , eriIotaStep :: Maybe Bool 45 , eriPickSubsVar :: Bool 46 , eriEqRState :: Maybe EqReasoningState 47 } 48 49initExpRefInfo :: ExpRefInfo o 50initExpRefInfo = ExpRefInfo 51 { eriMain = Nothing 52 , eriUnifs = [] 53 , eriInfTypeUnknown = False 54 , eriIsEliminand = False 55 , eriUsedVars = Nothing 56 , eriIotaStep = Nothing 57 , eriPickSubsVar = False 58 , eriEqRState = Nothing 59 } 60 61getinfo :: [RefInfo o] -> ExpRefInfo o 62getinfo = foldl step initExpRefInfo where 63 64 step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o 65 step eri x@RIMainInfo{} = eri { eriMain = Just x } 66 step eri x@RIUnifInfo{} = eri { eriUnifs = x : eriUnifs eri } 67 step eri RIInferredTypeUnknown = eri { eriInfTypeUnknown = True } 68 step eri RINotConstructor = eri { eriIsEliminand = True } 69 step eri (RIUsedVars nuids nused) = eri { eriUsedVars = Just (nuids, nused) } 70 step eri (RIIotaStep semif) = eri { eriIotaStep = Just iota' } where 71 iota' = semif || (Just True ==) (eriIotaStep eri) 72 step eri RIPickSubsvar = eri { eriPickSubsVar = True } 73 step eri (RIEqRState s) = eri { eriEqRState = Just s } 74 step eri _ = __IMPOSSIBLE__ 75 76 77-- | @univar sub v@ figures out what the name of @v@ "outside" of 78-- the substitution @sub@ ought to be, if anything. 79 80univar :: [CAction o] -> Nat -> Maybe Nat 81univar cl v = getOutsideName cl v 0 where 82 83 getOutsideName :: [CAction o] -> Nat -> Nat -> Maybe Nat 84 -- @v@ is offset by @v'@ binders 85 getOutsideName [] v v' = Just (v' + v) 86 -- @v@ was introduced by the weakening: disappears 87 getOutsideName (Weak n : _) v v' | v < n = Nothing 88 -- @v@ was introduced before the weakening: strengthened 89 getOutsideName (Weak n : xs) v v' = getOutsideName xs (v - n) v' 90 -- Name of @v@ before the substitution was pushed in 91 -- had to be offset by 1 92 getOutsideName (Sub _ : xs) v v' = getOutsideName xs v (v' + 1) 93 -- If this is the place where @v@ was bound, it used to 94 -- be called 0 + offset of all the vars substituted for 95 getOutsideName (Skip : _) 0 v' = Just v' 96 -- Going over a binder: de Bruijn name of @v@ decreased 97 -- but offset increased 98 getOutsideName (Skip : xs) v v' = getOutsideName xs (v - 1) (v' + 1) 99 100-- | List of the variables instantiated by the substitution 101subsvars :: [CAction o] -> [Nat] 102subsvars = f 0 where 103 104 f :: Nat -> [CAction o] -> [Nat] 105 f n [] = [] 106 f n (Weak _ : xs) = f n xs -- why? 107 f n (Sub _ : xs) = n : f (n + 1) xs 108 f n (Skip : xs) = f (n + 1) xs 109 110-- | Moves 111-- A move is composed of a @Cost@ together with an action 112-- computing the refined problem. 113 114type Move o = Move' (RefInfo o) (Exp o) 115 116-- | New constructors 117-- Taking a step towards a solution consists in picking a 118-- constructor and filling in the missing parts with 119-- placeholders to be discharged later on. 120 121newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk)) 122newAbs mid = Abs mid <$> newPlaceholder 123 124newLam :: Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o) 125newLam hid mid = Lam hid <$> newAbs mid 126 127newPi :: UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o) 128newPi uid dep hid = Pi (Just uid) hid dep <$> newPlaceholder <*> newAbs NoId 129 130foldArgs :: [(Hiding, MExp o)] -> MArgList o 131foldArgs = foldr (\ (h, a) sp -> NotM $ ALCons h a sp) (NotM ALNil) 132 133-- | New spine of arguments potentially using placeholders 134 135newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o) 136newArgs' h tms = foldArgs . zip h . (++ tms) <$> replicateM size newPlaceholder 137 where size = length h - length tms 138 139newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o) 140newArgs h = newArgs' h [] 141 142-- | New @App@lication node using a new spine of arguments 143-- respecting the @Hiding@ annotation 144 145newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] -> 146 RefCreateEnv (RefInfo o) (Exp o) 147newApp' meta cst hds tms = 148 App (Just meta) <$> newOKHandle <*> return (Const cst) <*> newArgs' hds tms 149 150newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o) 151newApp meta cst hds = newApp' meta cst hds [] 152 153-- | Equality reasoning steps 154-- The begin token is accompanied by two steps because 155-- it does not make sense to have a derivation any shorter 156-- than that. 157 158eqStep :: UId o -> EqReasoningConsts o -> Move o 159eqStep meta eqrc = Move costEqStep $ newApp meta (eqrcStep eqrc) 160 [Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden] 161 162eqEnd :: UId o -> EqReasoningConsts o -> Move o 163eqEnd meta eqrc = Move costEqEnd $ newApp meta (eqrcEnd eqrc) 164 [Hidden, Hidden, NotHidden] 165 166eqCong :: UId o -> EqReasoningConsts o -> Move o 167eqCong meta eqrc = Move costEqCong $ newApp meta (eqrcCong eqrc) 168 [Hidden, Hidden, Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden] 169 170eqSym :: UId o -> EqReasoningConsts o -> Move o 171eqSym meta eqrc = Move costEqSym $ newApp meta (eqrcSym eqrc) 172 [Hidden, Hidden, Hidden, Hidden, NotHidden] 173 174eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o 175eqBeginStep2 meta eqrc = Move costEqStep $ do 176 e1 <- newApp meta (eqrcStep eqrc) 177 [Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden] 178 e2 <- newApp' meta (eqrcStep eqrc) 179 [Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden] 180 [NotM e1] 181 newApp' meta (eqrcBegin eqrc) [Hidden, Hidden, Hidden, Hidden, NotHidden] 182 [NotM e2] 183 184 185-- | Pick the first unused UId amongst the ones you have seen (GA: ??) 186-- Defaults to the head of the seen ones. 187 188pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool) 189pickUid used seen = maybe (head seen, False) (, True) $ firstUnused seen where 190 {- ?? which uid to pick -} 191 192 firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o)) 193 firstUnused [] = Nothing 194 firstUnused (Nothing : _) = Just Nothing 195 firstUnused (mu@(Just u) : us) = 196 if u `elem` used then firstUnused us else Just mu 197 198instance Refinable (Exp o) (RefInfo o) where 199 refinements envinfo infos meta = 200 let 201 hints = rieHints envinfo 202 deffreevars = rieDefFreeVars envinfo 203 204 meqr = rieEqReasoningConsts envinfo 205 206 ExpRefInfo { eriMain = Just (RIMainInfo n tt iotastepdone) 207 , eriUnifs = unis 208 , eriInfTypeUnknown = inftypeunknown 209 , eriIsEliminand = iseliminand -- TODO:: Defined but not used 210 , eriUsedVars = Just (uids, usedvars) 211 , eriIotaStep = iotastep 212 , eriPickSubsVar = picksubsvar -- TODO:: Defined but not used 213 , eriEqRState = meqrstate 214 } = getinfo infos 215 216 eqrstate = fromMaybe EqRSNone meqrstate 217 218 set l = return $ Sort (Set l) 219 in case unis of 220 [] -> 221 let 222 223 eqr = fromMaybe __IMPOSSIBLE__ meqr 224 eq_end = eqEnd meta eqr 225 eq_step = eqStep meta eqr 226 eq_cong = eqCong meta eqr 227 eq_sym = eqSym meta eqr 228 eq_begin_step2 = eqBeginStep2 meta eqr 229 230 adjustCost i = if inftypeunknown then costInferredTypeUnkown else i 231 varcost v | v < n - deffreevars = adjustCost $ 232 if v `elem` (mapMaybe getVar usedvars) 233 then costAppVarUsed else costAppVar 234 varcost v | otherwise = adjustCost costAppHint 235 varapps = map (\ v -> Move (varcost v) $ app n meta Nothing (Var v)) [0..n - 1] 236 hintapps = map (\(c, hm) -> Move (cost c hm) (app n meta Nothing (Const c))) hints 237 where 238 cost :: ConstRef o -> HintMode -> Cost 239 cost c hm = adjustCost $ case (iotastep , hm) of 240 (Just _ , _ ) -> costIotaStep 241 (Nothing , HMNormal) -> 242 if c `elem` (mapMaybe getConst usedvars) 243 then costAppHintUsed else costAppHint 244 (Nothing , HMRecCall) -> 245 if c `elem` (mapMaybe getConst usedvars) 246 then costAppRecCallUsed else costAppRecCall 247 generics = varapps ++ hintapps 248 in case rawValue tt of 249 250 _ | eqrstate == EqRSChain -> 251 return [eq_end, eq_step] 252 253 HNPi hid _ _ (Abs id _) -> return $ 254 Move (adjustCost (if iotastepdone then costLamUnfold else costLam)) (newLam hid id) 255 : Move costAbsurdLam (return $ AbsurdLambda hid) 256 : generics 257 258 HNSort (Set l) -> return $ 259 map (Move (adjustCost costSort) . set) [0..l - 1] 260 ++ map (Move (adjustCost costPi) . newPi meta True) [NotHidden, Hidden] 261 ++ generics 262 263 264 HNApp (Const c) _ -> do 265 cd <- readIORef c 266 return $ case cdcont cd of 267 268 Datatype cons _ | eqrstate == EqRSNone -> 269 map (\c -> Move (adjustCost $ case iotastep of 270 Just True -> costUnification 271 _ -> if length cons <= 1 272 then costAppConstructorSingle 273 else costAppConstructor) 274 $ app n meta Nothing (Const c)) cons 275 ++ generics 276 ++ (guard (maybe False ((c ==) . eqrcId) meqr) 277 *> [eq_sym, eq_cong, eq_begin_step2]) 278 279 _ | eqrstate == EqRSPrf1 -> generics ++ [eq_sym, eq_cong] 280 _ | eqrstate == EqRSPrf2 -> generics ++ [eq_cong] 281 282 _ -> generics 283 _ -> return generics 284 (RIUnifInfo cl hne : _) -> 285 let 286 subsvarapps = map (Move costUnification . app n meta Nothing . Var) (subsvars cl) 287 mlam = case rawValue tt of 288 HNPi hid _ _ (Abs id _) -> [Move costUnification (newLam hid id)] 289 _ -> [] 290 generics = mlam ++ subsvarapps 291 292 in 293 return $ case rawValue hne of 294 HNApp (Var v) _ -> 295 let (uid, isunique) = pickUid uids $ seenUIds hne 296 uni = case univar cl v of 297 Just v | v < n -> [Move (costUnificationIf isunique) $ app n meta uid (Var v)] 298 _ -> [] 299 in uni ++ generics 300 HNApp (Const c) _ -> 301 let (uid, isunique) = pickUid uids $ seenUIds hne 302 in Move (costUnificationIf isunique) (app n meta uid (Const c)) : generics 303 HNLam{} -> generics 304 HNPi hid possdep _ _ -> 305 let (uid, isunique) = pickUid uids $ seenUIds hne 306 in Move (costUnificationIf isunique) (newPi (fromMaybe meta uid) possdep hid) : generics 307 HNSort (Set l) -> map (Move costUnification . set) [0..l] ++ generics 308 HNSort _ -> generics 309 _ -> __IMPOSSIBLE__ 310 311 where 312 313 app :: Nat -> UId o -> Maybe (UId o) -> Elr o -> 314 RefCreateEnv (RefInfo o) (Exp o) 315 app n meta muid elr = do 316 p <- newPlaceholder 317 p <- case elr of 318 Var{} -> return p 319 Const c -> do 320 cd <- RefCreateEnv $ lift $ readIORef c 321 let dfvapp 0 _ = p 322 dfvapp i n = NotM $ ALCons NotHidden 323 (NotM $ App Nothing (NotM $ OKVal) (Var n) (NotM ALNil)) 324 (dfvapp (i - 1) (n - 1)) 325 -- NotHidden is ok because agda reification throws these arguments 326 -- away and agsy skips typechecking them 327 return $ dfvapp (cddeffreevars cd) (n - 1) 328 okh <- newOKHandle 329 return $ App (Just $ fromMaybe meta muid) okh elr p 330 331 332extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> Move o 333extraref meta seenuids c = Move costAppExtraRef $ app (head seenuids) (Const c) 334 where 335 app muid elr = App (Just $ fromMaybe meta muid) 336 <$> newOKHandle <*> return elr <*> newPlaceholder 337 338instance Refinable (ICExp o) (RefInfo o) where 339 refinements _ infos _ = 340 let (RICopyInfo e : _) = infos 341 in return [Move 0 (return e)] 342 343 344instance Refinable (ConstRef o) (RefInfo o) where 345 refinements _ [RICheckProjIndex projs] _ = return $ map (Move 0 . return) projs 346 refinements _ _ _ = __IMPOSSIBLE__ 347 348 349-- --------------------------------- 350 351costIncrease, costUnificationOccurs, costUnification, costAppVar, 352 costAppVarUsed, costAppHint, costAppHintUsed, costAppRecCall, 353 costAppRecCallUsed, costAppConstructor, costAppConstructorSingle, 354 costAppExtraRef, costLam, costLamUnfold, costPi, costSort, costIotaStep, 355 costInferredTypeUnkown, costAbsurdLam 356 :: Cost 357 358costUnificationIf :: Bool -> Cost 359costUnificationIf b = if b then costUnification else costUnificationOccurs 360 361costIncrease = 1000 362costUnificationOccurs = 100 -- 1000001 -- 1 -- 100 363costUnification = 0000 364costAppVar = 0000 -- 0, 1 365costAppVarUsed = 1000 -- 5 366costAppHint = 3000 -- 2, 5 367costAppHintUsed = 5000 368costAppRecCall = 0 -- 1000? 369costAppRecCallUsed = 10000 -- 1000? 370costAppConstructor = 1000 371costAppConstructorSingle = 0000 372costAppExtraRef = 1000 373costLam = 0000 -- 1, 0 374costLamUnfold = 1000 -- 1, 0 375costPi = 1000003 -- 100 -- 5 376costSort = 1000004 -- 0 377costIotaStep = 3000 -- 1000005 -- 2 -- 100 378costInferredTypeUnkown = 1000006 -- 100 379costAbsurdLam = 0 380 381costEqStep, costEqEnd, costEqSym, costEqCong :: Cost 382costEqStep = 2000 383costEqEnd = 0 384costEqSym = 0 385costEqCong = 500 386 387prioNo, prioTypeUnknown, prioTypecheckArgList, prioInferredTypeUnknown, 388 prioCompBeta, prioCompBetaStructured, prioCompareArgList, prioCompIota, 389 prioCompChoice, prioCompUnif, prioCompCopy, prioNoIota, prioAbsurdLambda, 390 prioProjIndex 391 :: Prio 392prioNo = (-1) 393prioTypeUnknown = 0 394prioTypecheckArgList = 3000 395prioInferredTypeUnknown = 4000 396prioCompBeta = 4000 397prioCompBetaStructured = 4000 398prioCompIota = 4000 399prioCompChoice = 5000 -- 700 -- 5000 400prioCompUnif = 6000 -- 2 401prioCompCopy = 8000 402prioCompareArgList = 7000 -- 5 -- 2 403prioNoIota = 500 -- 500 404prioAbsurdLambda = 1000 405 406prioProjIndex = 3000 407 408prioTypecheck :: Bool -> Prio 409prioTypecheck False = 1000 410prioTypecheck True = 0 411 412-- --------------------------------- 413 414instance Trav a => Trav [a] where 415 type Block [a] = Block a 416 trav _ [] = return () 417 trav f (x:xs) = trav f x >> trav f xs 418 419instance Trav (MId, CExp o) where 420 type Block (MId, CExp o) = RefInfo o 421 trav f (_, ce) = trav f ce 422 423instance Trav (TrBr a o) where 424 type Block (TrBr a o) = RefInfo o 425 trav f (TrBr es _) = trav f es 426 427instance Trav (Exp o) where 428 type Block (Exp o) = RefInfo o 429 trav f = \case 430 App _ _ _ args -> trav f args 431 Lam _ (Abs _ b) -> trav f b 432 Pi _ _ _ it (Abs _ ot) -> trav f it >> trav f ot 433 Sort _ -> return () 434 AbsurdLambda{} -> return () 435 436instance Trav (ArgList o) where 437 type Block (ArgList o) = RefInfo o 438 trav _ ALNil = return () 439 trav f (ALCons _ arg args) = trav f arg >> trav f args 440 trav f (ALProj eas _ _ as) = trav f eas >> trav f as 441 trav f (ALConPar args) = trav f args 442 443-- --------------------------------- 444