{-# LANGUAGE CPP #-}
module Agda.Auto.Syntax where
import Data.IORef
import qualified Data.Set as Set
import Agda.Syntax.Common (Hiding)
import Agda.Auto.NarrowingSearch
#include "undefined.h"
import Agda.Utils.Impossible
type UId o = Metavar (Exp o) (RefInfo o)
data HintMode = HMNormal
| HMRecCall
data EqReasoningConsts o = EqReasoningConsts
{ eqrcId
, eqrcBegin
, eqrcStep
, eqrcEnd
, eqrcSym
, eqrcCong
:: ConstRef o
}
data EqReasoningState = EqRSNone | EqRSChain | EqRSPrf1 | EqRSPrf2 | EqRSPrf3
deriving (Eq, Show)
data RefInfo o
= RIEnv
{ rieHints :: [(ConstRef o, HintMode)]
, rieDefFreeVars :: Nat
, rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
}
| RIMainInfo
{ riMainCxtLength :: Nat
, riMainType :: HNExp o
, riMainIota :: Bool
}
| RIUnifInfo [CAction o] (HNExp o)
| RICopyInfo (ICExp o)
| RIIotaStep Bool
| RIInferredTypeUnknown
| RINotConstructor
| RIUsedVars [UId o] [Elr o]
| RIPickSubsvar
| RIEqRState EqReasoningState
| RICheckElim Bool
| RICheckProjIndex [ConstRef o]
type MyPB o = PB (RefInfo o)
type MyMB a o = MB a (RefInfo o)
type Nat = Int
data MId = Id String
| NoId
data Abs a = Abs MId a
data ConstDef o = ConstDef
{ cdname :: String
, cdorigin :: o
, cdtype :: MExp o
, cdcont :: DeclCont o
, cddeffreevars :: Nat
}
data DeclCont o
= Def Nat [Clause o] (Maybe Nat)
(Maybe Nat)
| Datatype [ConstRef o]
[ConstRef o]
| Constructor Nat
| Postulate
type Clause o = ([Pat o], MExp o)
data Pat o
= PatConApp (ConstRef o) [Pat o]
| PatVar String
| PatExp
type ConstRef o = IORef (ConstDef o)
data Elr o
= Var Nat
| Const (ConstRef o)
deriving (Eq)
getVar :: Elr o -> Maybe Nat
getVar (Var n) = Just n
getVar Const{} = Nothing
getConst :: Elr o -> Maybe (ConstRef o)
getConst (Const c) = Just c
getConst Var{} = Nothing
data Sort
= Set Nat
| UnknownSort
| Type
data Exp o
= App
{ appUId :: Maybe (UId o)
, appOK :: OKHandle (RefInfo o)
, appHead :: Elr o
, appElims :: MArgList o
}
| Lam Hiding (Abs (MExp o))
| Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))
| Sort Sort
| AbsurdLambda Hiding
dontCare :: Exp o
dontCare = Sort UnknownSort
type MExp o = MM (Exp o) (RefInfo o)
data ArgList o
= ALNil
| ALCons Hiding (MExp o) (MArgList o)
| ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)
| ALConPar (MArgList o)
type MArgList o = MM (ArgList o) (RefInfo o)
data WithSeenUIds a o = WithSeenUIds
{ seenUIds :: [Maybe (UId o)]
, rawValue :: a
}
type HNExp o = WithSeenUIds (HNExp' o) o
data HNExp' o =
HNApp (Elr o) (ICArgList o)
| HNLam Hiding (Abs (ICExp o))
| HNPi Hiding Bool (ICExp o) (Abs (ICExp o))
| HNSort Sort
data HNArgList o = HNALNil
| HNALCons Hiding (ICExp o) (ICArgList o)
| HNALConPar (ICArgList o)
data ICArgList o = CALNil
| CALConcat (Clos (MArgList o) o) (ICArgList o)
type ICExp o = Clos (MExp o) o
data Clos a o = Clos [CAction o] a
type CExp o = TrBr (ICExp o) o
data TrBr a o = TrBr [MExp o] a
data CAction o
= Sub (ICExp o)
| Skip
| Weak Nat
type Ctx o = [(MId, CExp o)]
type EE = IO
detecteliminand :: [Clause o] -> Maybe Nat
detecteliminand cls =
case map cleli cls of
[] -> Nothing
(i:is) -> if all (i ==) is then i else Nothing
where
cleli (pats, _) = pateli 0 pats
pateli i (PatConApp _ args : pats) = if all notcon (args ++ pats) then Just i else Nothing
pateli i (_ : pats) = pateli (i + 1) pats
pateli i [] = Nothing
notcon PatConApp{} = False
notcon _ = True
detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
detectsemiflex _ _ = return False
categorizedecl :: ConstRef o -> IO ()
categorizedecl c = do
cd <- readIORef c
case cdcont cd of
Def narg cls _ _ -> do
semif <- detectsemiflex c cls
let elim = detecteliminand cls
semifb = case (semif, elim) of
(True, Just i) -> Just i
(_, _) -> Nothing
writeIORef c (cd {cdcont = Def narg cls elim semifb})
_ -> return ()
class MetaliseOKH t where
metaliseOKH :: t -> IO t
instance MetaliseOKH t => MetaliseOKH (MM t a) where
metaliseOKH e = case e of
Meta m -> return $ Meta m
NotM e -> NotM <$> metaliseOKH e
instance MetaliseOKH t => MetaliseOKH (Abs t) where
metaliseOKH (Abs id b) = Abs id <$> metaliseOKH b
instance MetaliseOKH (Exp o) where
metaliseOKH e = case e of
App uid okh elr args ->
(\ m -> App uid m elr) <$> (Meta <$> initMeta) <*> metaliseOKH args
Lam hid b -> Lam hid <$> metaliseOKH b
Pi uid hid dep it ot ->
Pi uid hid dep <$> metaliseOKH it <*> metaliseOKH ot
Sort{} -> return e
AbsurdLambda{} -> return e
instance MetaliseOKH (ArgList o) where
metaliseOKH e = case e of
ALNil -> return ALNil
ALCons hid a as -> ALCons hid <$> metaliseOKH a <*> metaliseOKH as
ALProj eas idx hid as ->
(\ eas -> ALProj eas idx hid) <$> metaliseOKH eas <*> metaliseOKH as
ALConPar as -> ALConPar <$> metaliseOKH as
metaliseokh :: MExp o -> IO (MExp o)
metaliseokh = metaliseOKH
class ExpandMetas t where
expandMetas :: t -> IO t
instance ExpandMetas t => ExpandMetas (MM t a) where
expandMetas t = case t of
NotM e -> NotM <$> expandMetas e
Meta m -> do
mb <- readIORef (mbind m)
case mb of
Nothing -> return $ Meta m
Just e -> NotM <$> expandMetas e
instance ExpandMetas t => ExpandMetas (Abs t) where
expandMetas (Abs id b) = Abs id <$> expandMetas b
instance ExpandMetas (Exp o) where
expandMetas t = case t of
App uid okh elr args -> App uid okh elr <$> expandMetas args
Lam hid b -> Lam hid <$> expandMetas b
Pi uid hid dep it ot ->
Pi uid hid dep <$> expandMetas it <*> expandMetas ot
Sort{} -> return t
AbsurdLambda{} -> return t
instance ExpandMetas (ArgList o) where
expandMetas e = case e of
ALNil -> return ALNil
ALCons hid a as -> ALCons hid <$> expandMetas a <*> expandMetas as
ALProj eas idx hid as ->
(\ a b -> ALProj a b hid) <$> expandMetas eas
<*> expandbind idx <*> expandMetas as
ALConPar as -> ALConPar <$> expandMetas as
addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs newargs CALNil = CALConcat newargs CALNil
addtrailingargs newargs (CALConcat x xs) = CALConcat x (addtrailingargs newargs xs)
closify :: MExp o -> CExp o
closify e = TrBr [e] (Clos [] e)
sub :: MExp o -> CExp o -> CExp o
sub e (TrBr trs (Clos (Skip : as) x)) = TrBr (e : trs) (Clos (Sub (Clos [] e) : as) x)
sub _ _ = __IMPOSSIBLE__
subi :: MExp o -> ICExp o -> ICExp o
subi e (Clos (Skip : as) x) = Clos (Sub (Clos [] e) : as) x
subi _ _ = __IMPOSSIBLE__
weak :: Weakening t => Nat -> t -> t
weak 0 = id
weak n = weak' n
class Weakening t where
weak' :: Nat -> t -> t
instance Weakening a => Weakening (TrBr a o) where
weak' n (TrBr trs e) = TrBr trs (weak' n e)
instance Weakening (Clos a o) where
weak' n (Clos as x) = Clos (Weak n : as) x
instance Weakening (ICArgList o) where
weak' n e = case e of
CALNil -> CALNil
CALConcat a as -> CALConcat (weak' n a) (weak' n as)
instance Weakening (Elr o) where
weak' n = rename (n+)
doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)
doclos = f 0
where
f ns [] i = Left (ns + i)
f ns (Weak n : xs) i = f (ns + n) xs i
f ns (Sub s : _ ) 0 = Right (weak ns s)
f ns (Skip : _ ) 0 = Left ns
f ns (Skip : xs) i = f (ns + 1) xs (i - 1)
f ns (Sub _ : xs) i = f ns xs (i - 1)
freeVars :: FreeVars t => t -> Set.Set Nat
freeVars = freeVarsOffset 0
class FreeVars t where
freeVarsOffset :: Nat -> t -> Set.Set Nat
instance (FreeVars a, FreeVars b) => FreeVars (a, b) where
freeVarsOffset n (a, b) = Set.union (freeVarsOffset n a) (freeVarsOffset n b)
instance FreeVars t => FreeVars (MM t a) where
freeVarsOffset n e = freeVarsOffset n (rm __IMPOSSIBLE__ e)
instance FreeVars t => FreeVars (Abs t) where
freeVarsOffset n (Abs id e) = freeVarsOffset (n + 1) e
instance FreeVars (Elr o) where
freeVarsOffset n e = case e of
Var v -> Set.singleton (v - n)
Const{} -> Set.empty
instance FreeVars (Exp o) where
freeVarsOffset n e = case e of
App _ _ elr args -> freeVarsOffset n (elr, args)
Lam _ b -> freeVarsOffset n b
Pi _ _ _ it ot -> freeVarsOffset n (it, ot)
Sort{} -> Set.empty
AbsurdLambda{} -> Set.empty
instance FreeVars (ArgList o) where
freeVarsOffset n es = case es of
ALNil -> Set.empty
ALCons _ e es -> freeVarsOffset n (e, es)
ALConPar es -> freeVarsOffset n es
ALProj{} -> __IMPOSSIBLE__
rename :: Renaming t => (Nat -> Nat) -> t -> t
rename = renameOffset 0
class Renaming t where
renameOffset :: Nat -> (Nat -> Nat) -> t -> t
instance (Renaming a, Renaming b) => Renaming (a, b) where
renameOffset j ren (a, b) = (renameOffset j ren a, renameOffset j ren b)
instance Renaming t => Renaming (MM t a) where
renameOffset j ren e = NotM $ renameOffset j ren (rm __IMPOSSIBLE__ e)
instance Renaming t => Renaming (Abs t) where
renameOffset j ren (Abs id e) = Abs id $ renameOffset (j + 1) ren e
instance Renaming (Elr o) where
renameOffset j ren e = case e of
Var v | v >= j -> Var (ren (v - j) + j)
_ -> e
instance Renaming (Exp o) where
renameOffset j ren e = case e of
App uid ok elr args -> uncurry (App uid ok) $ renameOffset j ren (elr, args)
Lam hid e -> Lam hid (renameOffset j ren e)
Pi a b c it ot -> uncurry (Pi a b c) $ renameOffset j ren (it, ot)
Sort{} -> e
AbsurdLambda{} -> e
instance Renaming (ArgList o) where
renameOffset j ren e = case e of
ALNil -> ALNil
ALCons hid a as -> uncurry (ALCons hid) $ renameOffset j ren (a, as)
ALConPar as -> ALConPar (renameOffset j ren as)
ALProj{} -> __IMPOSSIBLE__