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