1
2module Agda.Auto.Syntax where
3
4import Data.IORef
5import qualified Data.Set as Set
6
7import Agda.Syntax.Common (Hiding)
8import Agda.Auto.NarrowingSearch
9
10import Agda.Utils.Impossible
11
12-- | Unique identifiers for variable occurrences in unification.
13type UId o = Metavar (Exp o) (RefInfo o)
14
15data HintMode = HMNormal
16              | HMRecCall
17
18data EqReasoningConsts o = EqReasoningConsts
19  { eqrcId    -- "_≡_"
20  , eqrcBegin -- "begin_"
21  , eqrcStep  -- "_≡⟨_⟩_"
22  , eqrcEnd   -- "_∎"
23  , eqrcSym   -- "sym"
24  , eqrcCong  -- "cong"
25  :: ConstRef o
26  }
27
28data EqReasoningState = EqRSNone | EqRSChain | EqRSPrf1 | EqRSPrf2 | EqRSPrf3
29 deriving (Eq, Show)
30
31-- | The concrete instance of the 'blk' parameter in 'Metavar'.
32--   I.e., the information passed to the search control.
33
34data RefInfo o
35  = RIEnv
36    { rieHints :: [(ConstRef o, HintMode)]
37    , rieDefFreeVars :: Nat
38      -- ^ Nat - deffreevars
39      --   (to make cost of using module parameters correspond to that of hints).
40    , rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
41    }
42  | RIMainInfo
43    { riMainCxtLength :: Nat
44      -- ^ Size of typing context in which meta was created.
45    , riMainType      :: HNExp o
46      -- ^ Head normal form of type of meta.
47    , riMainIota      :: Bool
48       -- ^ True if iota steps performed when normalising target type
49       --   (used to put cost when traversing a definition
50       --    by construction instantiation).
51    }
52  | RIUnifInfo [CAction o] (HNExp o)
53    -- meta environment, opp hne
54  | RICopyInfo (ICExp o)
55  | RIIotaStep Bool -- True - semiflex
56  | RIInferredTypeUnknown
57  | RINotConstructor
58  | RIUsedVars [UId o] [Elr o]
59  | RIPickSubsvar
60
61  | RIEqRState EqReasoningState
62
63
64  | RICheckElim Bool -- isdep
65  | RICheckProjIndex [ConstRef o] -- noof proj functions
66
67
68type MyPB o = PB (RefInfo o)
69type MyMB a o = MB a (RefInfo o)
70
71type Nat = Int
72
73data MId = Id String
74         | NoId
75
76-- | Abstraction with maybe a name.
77--
78--   Different from Agda, where there is also info
79--   whether function is constant.
80data Abs a = Abs MId a
81
82-- | Constant signatures.
83
84data ConstDef o = ConstDef
85  { cdname        :: String
86    -- ^ For debug printing.
87  , cdorigin      :: o
88    -- ^ Reference to the Agda constant.
89  , cdtype        :: MExp o
90    -- ^ Type of constant.
91  , cdcont        :: DeclCont o
92    -- ^ Constant definition.
93  , cddeffreevars :: Nat
94    -- ^ Free vars of the module where the constant is defined..
95  } -- contains no metas
96
97-- | Constant definitions.
98
99data DeclCont o
100  = Def Nat [Clause o] (Maybe Nat) -- maybe an index to elimand argument
101                       (Maybe Nat) -- maybe index to elim arg if semiflex
102  | Datatype [ConstRef o] -- constructors
103             [ConstRef o] -- projection functions (in case it is a record)
104
105  | Constructor Nat -- number of omitted args
106  | Postulate
107
108type Clause o = ([Pat o], MExp o)
109
110data Pat o
111  = PatConApp (ConstRef o) [Pat o]
112  | PatVar String
113  | PatExp
114    -- ^ Dot pattern.
115{- TODO: projection patterns.
116  | PatProj (ConstRef o)
117    -- ^ Projection pattern.
118-}
119
120type ConstRef o = IORef (ConstDef o)
121
122-- | Head of application (elimination).
123data Elr o
124  = Var Nat
125  | Const (ConstRef o)
126  deriving (Eq)
127
128getVar :: Elr o -> Maybe Nat
129getVar (Var n) = Just n
130getVar Const{} = Nothing
131
132getConst :: Elr o -> Maybe (ConstRef o)
133getConst (Const c) = Just c
134getConst Var{}     = Nothing
135
136data Sort
137  = Set Nat
138  | UnknownSort
139  | Type
140
141-- | Agsy's internal syntax.
142data Exp o
143  = App
144    { appUId   :: Maybe (UId o)
145      -- ^ Unique identifier of the head.
146    , appOK    :: OKHandle (RefInfo o)
147      -- ^ This application has been type-checked.
148    , appHead  :: Elr o
149      -- ^ Head.
150    , appElims :: MArgList o
151      -- ^ Arguments.
152    }
153  | Lam Hiding (Abs (MExp o))
154    -- ^ Lambda with hiding information.
155  | Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))
156    -- ^ @True@ if possibly dependent (var not known to not occur).
157    --   @False@ if non-dependent.
158  | Sort Sort
159  | AbsurdLambda Hiding
160    -- ^ Absurd lambda with hiding information.
161
162dontCare :: Exp o
163dontCare = Sort UnknownSort
164
165-- | "Maybe expression":  Expression or reference to meta variable.
166type MExp o = MM (Exp o) (RefInfo o)
167
168data ArgList o
169  = ALNil
170    -- ^ No more eliminations.
171  | ALCons Hiding (MExp o) (MArgList o)
172    -- ^ Application and tail.
173
174  | ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)
175    -- ^ proj pre args, projfcn idx, tail
176
177  | ALConPar (MArgList o)
178    -- ^ Constructor parameter (missing in Agda).
179    --   Agsy has monomorphic constructors.
180    --   Inserted to cover glitch of polymorphic constructor
181    --   applications coming from Agda
182
183type MArgList o = MM (ArgList o) (RefInfo o)
184
185data WithSeenUIds a o = WithSeenUIds
186  { seenUIds :: [Maybe (UId o)]
187  , rawValue :: a
188  }
189
190type HNExp o = WithSeenUIds (HNExp' o) o
191
192data HNExp' o =
193    HNApp  (Elr o) (ICArgList o)
194  | HNLam  Hiding (Abs (ICExp o))
195  | HNPi   Hiding Bool (ICExp o) (Abs (ICExp o))
196  | HNSort Sort
197
198-- | Head-normal form of 'ICArgList'.  First entry is exposed.
199--
200--   Q: Why are there no projection eliminations?
201data HNArgList o = HNALNil
202                 | HNALCons Hiding (ICExp o) (ICArgList o)
203                 | HNALConPar (ICArgList o)
204
205-- | Lazy concatenation of argument lists under explicit substitutions.
206data ICArgList o = CALNil
207                 | CALConcat (Clos (MArgList o) o) (ICArgList o)
208
209-- | An expression @a@ in an explicit substitution @[CAction a]@.
210type ICExp o  = Clos (MExp o) o
211data Clos a o = Clos [CAction o] a
212
213type CExp o   = TrBr (ICExp o) o
214data TrBr a o = TrBr [MExp o] a
215
216-- | Entry of an explicit substitution.
217--
218--   An explicit substitution is a list of @CAction@s.
219--   This is isomorphic to the usual presentation where
220--   @Skip@ and @Weak@ would be constructors of exp. substs.
221
222data CAction o
223  = Sub (ICExp o)
224    -- ^ Instantation of variable.
225  | Skip
226    -- ^ For going under a binder, often called "Lift".
227  | Weak Nat
228    -- ^ Shifting substitution (going to a larger context).
229
230type Ctx o = [(MId, CExp o)]
231
232type EE = IO
233
234-- -------------------------------------------
235
236detecteliminand :: [Clause o] -> Maybe Nat
237detecteliminand cls =
238 case map cleli cls of
239  [] -> Nothing
240  (i:is) -> if all (i ==) is then i else Nothing
241 where
242  cleli (pats, _) = pateli 0 pats
243  pateli i (PatConApp _ args : pats) = if all notcon (args ++ pats) then Just i else Nothing
244  pateli i (_ : pats) = pateli (i + 1) pats
245  pateli i [] = Nothing
246  notcon PatConApp{} = False
247  notcon _ = True
248
249detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
250detectsemiflex _ _ = return False -- disabled
251
252categorizedecl :: ConstRef o -> IO ()
253categorizedecl c = do
254 cd <- readIORef c
255 case cdcont cd of
256  Def narg cls _ _ -> do
257   semif <- detectsemiflex c cls
258   let elim = detecteliminand cls
259       semifb = case (semif, elim) of
260                 (True, Just i) -> Just i -- just copying val of elim arg. this should be changed
261                 (_, _) -> Nothing
262   writeIORef c (cd {cdcont = Def narg cls elim semifb})
263  _ -> return ()
264
265-- -------------------------------------------
266
267class MetaliseOKH t where
268  metaliseOKH :: t -> IO t
269
270instance MetaliseOKH t => MetaliseOKH (MM t a) where
271  metaliseOKH = \case
272    Meta m -> return $ Meta m
273    NotM e -> NotM <$> metaliseOKH e
274
275instance MetaliseOKH t => MetaliseOKH (Abs t) where
276  metaliseOKH (Abs id b) = Abs id <$> metaliseOKH b
277
278instance MetaliseOKH (Exp o) where
279  metaliseOKH = \case
280    App uid okh elr args ->
281      (\ m -> App uid m elr) <$> (Meta <$> initMeta) <*> metaliseOKH args
282    Lam hid b -> Lam hid <$> metaliseOKH b
283    Pi uid hid dep it ot ->
284      Pi uid hid dep <$> metaliseOKH it <*> metaliseOKH ot
285    e@Sort{} -> return e
286    e@AbsurdLambda{} -> return e
287
288instance MetaliseOKH (ArgList o) where
289  metaliseOKH = \case
290    ALNil -> return ALNil
291    ALCons hid a as -> ALCons hid <$> metaliseOKH a <*> metaliseOKH as
292    ALProj eas idx hid as ->
293      (\ eas -> ALProj eas idx hid) <$> metaliseOKH eas <*> metaliseOKH as
294    ALConPar as -> ALConPar <$> metaliseOKH as
295
296metaliseokh :: MExp o -> IO (MExp o)
297metaliseokh = metaliseOKH
298
299-- -------------------------------------------
300
301class ExpandMetas t where
302  expandMetas :: t -> IO t
303
304instance ExpandMetas t => ExpandMetas (MM t a) where
305  expandMetas = \case
306    NotM e -> NotM <$> expandMetas e
307    Meta m -> do
308      mb <- readIORef (mbind m)
309      case mb of
310        Nothing -> return $ Meta m
311        Just e  -> NotM <$> expandMetas e
312
313instance ExpandMetas t => ExpandMetas (Abs t) where
314  expandMetas (Abs id b) = Abs id <$> expandMetas b
315
316instance ExpandMetas (Exp o) where
317  expandMetas = \case
318    App uid okh elr args -> App uid okh elr <$> expandMetas args
319    Lam hid b -> Lam hid <$> expandMetas b
320    Pi uid hid dep it ot ->
321      Pi uid hid dep <$> expandMetas it <*> expandMetas ot
322    t@Sort{} -> return t
323    t@AbsurdLambda{} -> return t
324
325instance ExpandMetas (ArgList o) where
326  expandMetas = \case
327    ALNil -> return ALNil
328    ALCons hid a as -> ALCons hid <$> expandMetas a <*> expandMetas as
329    ALProj eas idx hid as ->
330      (\ a b -> ALProj a b hid) <$> expandMetas eas
331      <*> expandbind idx <*> expandMetas as
332    ALConPar as -> ALConPar <$> expandMetas as
333
334-- ---------------------------------
335
336addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
337addtrailingargs newargs CALNil = CALConcat newargs CALNil
338addtrailingargs newargs (CALConcat x xs) = CALConcat x (addtrailingargs newargs xs)
339
340-- ---------------------------------
341
342closify :: MExp o -> CExp o
343closify e = TrBr [e] (Clos [] e)
344
345sub :: MExp o -> CExp o -> CExp o
346-- sub e (Clos [] x) = Clos [Sub e] x
347sub e (TrBr trs (Clos (Skip : as) x)) = TrBr (e : trs) (Clos (Sub (Clos [] e) : as) x)
348{-sub e (Clos (Weak n : as) x) = if n == 1 then
349                                Clos as x
350                               else
351                                Clos (Weak (n - 1) : as) x-}
352sub _ _ = __IMPOSSIBLE__
353
354subi :: MExp o -> ICExp o -> ICExp o
355subi e (Clos (Skip : as) x) = Clos (Sub (Clos [] e) : as) x
356subi _ _ = __IMPOSSIBLE__
357
358weak :: Weakening t => Nat -> t -> t
359weak 0 = id
360weak n = weak' n
361
362class Weakening t where
363  weak' :: Nat -> t -> t
364
365instance Weakening a => Weakening (TrBr a o) where
366  weak' n (TrBr trs e) = TrBr trs (weak' n e)
367
368instance Weakening (Clos a o) where
369  weak' n (Clos as x) = Clos (Weak n : as) x
370
371instance Weakening (ICArgList o) where
372  weak' n = \case
373    CALNil         -> CALNil
374    CALConcat a as -> CALConcat (weak' n a) (weak' n as)
375
376instance Weakening (Elr o) where
377  weak' n = rename (n+)
378
379-- | Substituting for a variable.
380doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)
381doclos = f 0
382 where
383  -- ns is the number of weakenings
384  f ns []            i = Left (ns + i)
385  f ns (Weak n : xs) i = f (ns + n) xs i
386  f ns (Sub s  : _ ) 0 = Right (weak ns s)
387  f ns (Skip   : _ ) 0 = Left ns
388  f ns (Skip   : xs) i = f (ns + 1) xs (i - 1)
389  f ns (Sub _  : xs) i = f ns xs (i - 1)
390
391
392-- | FreeVars class and instances
393
394freeVars :: FreeVars t => t -> Set.Set Nat
395freeVars = freeVarsOffset 0
396
397class FreeVars t where
398  freeVarsOffset :: Nat -> t -> Set.Set Nat
399
400instance (FreeVars a, FreeVars b) => FreeVars (a, b) where
401  freeVarsOffset n (a, b) = Set.union (freeVarsOffset n a) (freeVarsOffset n b)
402
403instance FreeVars t => FreeVars (MM t a) where
404  freeVarsOffset n e = freeVarsOffset n (rm __IMPOSSIBLE__ e)
405
406instance FreeVars t => FreeVars (Abs t) where
407  freeVarsOffset n (Abs id e) = freeVarsOffset (n + 1) e
408
409instance FreeVars (Elr o) where
410  freeVarsOffset n = \case
411    Var v   -> Set.singleton (v - n)
412    Const{} -> Set.empty
413
414instance FreeVars (Exp o) where
415  freeVarsOffset n = \case
416   App _ _ elr args -> freeVarsOffset n (elr, args)
417   Lam _ b          -> freeVarsOffset n b
418   Pi _ _ _ it ot   -> freeVarsOffset n (it, ot)
419   Sort{}           -> Set.empty
420   AbsurdLambda{}   -> Set.empty
421
422instance FreeVars (ArgList o) where
423  freeVarsOffset n es = case es of
424    ALNil         -> Set.empty
425    ALCons _ e es -> freeVarsOffset n (e, es)
426    ALConPar es   -> freeVarsOffset n es
427    ALProj{}      -> __IMPOSSIBLE__
428
429
430-- | Renaming Typeclass and instances
431rename :: Renaming t => (Nat -> Nat) -> t -> t
432rename = renameOffset 0
433
434class Renaming t where
435  renameOffset :: Nat -> (Nat -> Nat) -> t -> t
436
437instance (Renaming a, Renaming b) => Renaming (a, b) where
438  renameOffset j ren (a, b) = (renameOffset j ren a, renameOffset j ren b)
439
440instance Renaming t => Renaming (MM t a) where
441  renameOffset j ren e = NotM $ renameOffset j ren (rm __IMPOSSIBLE__ e)
442
443instance Renaming t => Renaming (Abs t) where
444  renameOffset j ren (Abs id e) = Abs id $ renameOffset (j + 1) ren e
445
446instance Renaming (Elr o) where
447  renameOffset j ren = \case
448    Var v | v >= j -> Var (ren (v - j) + j)
449    e              -> e
450
451instance Renaming (Exp o) where
452  renameOffset j ren = \case
453    App uid ok elr args -> uncurry (App uid ok) $ renameOffset j ren (elr, args)
454    Lam hid e -> Lam hid (renameOffset j ren e)
455    Pi a b c it ot -> uncurry (Pi a b c) $ renameOffset j ren (it, ot)
456    e@Sort{}         -> e
457    e@AbsurdLambda{} -> e
458
459instance Renaming (ArgList o) where
460  renameOffset j ren = \case
461    ALNil           -> ALNil
462    ALCons hid a as -> uncurry (ALCons hid) $ renameOffset j ren (a, as)
463    ALConPar as     -> ALConPar (renameOffset j ren as)
464    ALProj{}        -> __IMPOSSIBLE__
465