module Agda.Auto.Syntax where
import Agda.Utils.Impossible
#include "../undefined.h"
import Data.IORef
import Agda.Auto.NarrowingSearch
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 Nat (HNExp o) Bool
| forall a . 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 FMode = Hidden
| Instance
| NotHidden
deriving Eq
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)
data Sort = Set Nat
| UnknownSort
| Type
data Exp o = App (Maybe (UId o)) (OKHandle (RefInfo o)) (Elr o) (MArgList o)
| Lam FMode (Abs (MExp o))
| Pi (Maybe (UId o)) FMode Bool (MExp o) (Abs (MExp o))
| Sort Sort
| AbsurdLambda FMode
dontCare = Sort UnknownSort
type MExp o = MM (Exp o) (RefInfo o)
data ArgList o = ALNil
| ALCons FMode (MExp o) (MArgList o)
| ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) FMode (MArgList o)
| ALConPar (MArgList o)
type MArgList o = MM (ArgList o) (RefInfo o)
data HNExp o = HNApp [Maybe (UId o)] (Elr o) (ICArgList o)
| HNLam [Maybe (UId o)] FMode (Abs (ICExp o))
| HNPi [Maybe (UId o)] FMode Bool (ICExp o) (Abs (ICExp o))
| HNSort Sort
data HNArgList o = HNALNil
| HNALCons FMode (ICExp o) (ICArgList o)
| HNALConPar (ICArgList o)
type ICExp o = Clos (MExp o) o
type CExp o = TrBr (ICExp o) o
data ICArgList o = CALNil
| CALConcat (Clos (MArgList o) o) (ICArgList o)
data Clos a o = Clos [CAction o] a
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 ()
metaliseokh :: MExp o -> IO (MExp o)
metaliseokh = fm
where
fm (Meta m) = return $ Meta m
fm (NotM e) = do
e <- f e
return $ NotM e
f (App uid _ elr args) = do
m <- initMeta
args <- fms args
return $ App uid (Meta m) elr args
f (Lam hid (Abs id b)) = do
b <- fm b
return $ Lam hid (Abs id b)
f (Pi uid hid posdep it (Abs id ot)) = do
it <- fm it
ot <- fm ot
return $ Pi uid hid posdep it (Abs id ot)
f e@(Sort{}) = return e
f e@(AbsurdLambda{}) = return e
fms (Meta m) = return $ Meta m
fms (NotM es) = do
es <- fs es
return $ NotM es
fs ALNil = return ALNil
fs (ALCons hid a as) = do
a <- fm a
as <- fms as
return $ ALCons hid a as
fs (ALProj eas idx hid as) = do
eas <- fms eas
as <- fms as
return $ ALProj eas idx hid as
fs (ALConPar as) = do
as <- fms as
return $ ALConPar as
expandExp :: MExp o -> IO (MExp o)
expandExp = fm
where
fm (Meta m) = do
mb <- readIORef $ mbind m
case mb of
Nothing -> return $ Meta m
Just e -> fm (NotM e)
fm (NotM e) = do
e <- f e
return $ NotM e
f (App uid okh elr args) = do
args <- fms args
return $ App uid okh elr args
f (Lam hid (Abs id b)) = do
b <- fm b
return $ Lam hid (Abs id b)
f (Pi uid hid posdep it (Abs id ot)) = do
it <- fm it
ot <- fm ot
return $ Pi uid hid posdep it (Abs id ot)
f e@(Sort{}) = return e
f e@(AbsurdLambda{}) = return e
fms (Meta m) = do
mb <- readIORef $ mbind m
case mb of
Nothing -> return $ Meta m
Just es -> fms (NotM es)
fms (NotM es) = do
es <- fs es
return $ NotM es
fs ALNil = return ALNil
fs (ALCons hid a as) = do
a <- fm a
as <- fms as
return $ ALCons hid a as
fs (ALProj eas idx hid as) = do
idx <- expandbind idx
eas <- fms eas
as <- fms as
return $ ALProj eas idx hid as
fs (ALConPar as) = do
as <- fms as
return $ ALConPar 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 :: Nat -> CExp o -> CExp o
weak n (TrBr trs e) = TrBr trs (weaki n e)
weaki :: Nat -> Clos a o -> Clos a o
weaki 0 x = x
weaki n (Clos as x) = Clos (Weak n : as) x
weakarglist :: Nat -> ICArgList o -> ICArgList o
weakarglist 0 = id
weakarglist n = f
where f CALNil = CALNil
f (CALConcat (Clos cl as) as2) = CALConcat (Clos (Weak n : cl) as) (f as2)
weakelr :: Nat -> Elr o -> Elr o
weakelr 0 elr = elr
weakelr n (Var v) = Var (v + n)
weakelr _ elr@(Const _) = elr
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 (weaki 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)