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