    {-# OPTIONS -fglasgow-exts #-}

    module Agda.Auto.Syntax where

    import Data.IORef

    import Agda.Auto.NarrowingSearch

    data RefInfo o = RIEnv [ConstRef o]
                   | RIMainInfo Nat (HNExp o)
                   | forall a . RIUnifInfo (Metavar a (RefInfo o)) [CAction o] (HNExp o)  -- metavar is the flexible side of the equality

    type MyPB o = PB (RefInfo o)
    type MyMB a o = MB a (RefInfo o)

    type Nat = Int

    data FMode = Hidden
               | 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}  -- contains no metas

    data DeclCont o = Def Nat [Clause o]
                    | Datatype [ConstRef o]  -- constructors
                    | Constructor
                    | Postulate

    type Clause o = ([Pat o], MExp o)

    data Pat o = PatConApp (ConstRef o) [Pat o]
               | PatVar
               | PatExp

    type ConstRef o = IORef (ConstDef o)

    data Elr o = Var Nat
               | Const (ConstRef o)

    data Sort = SortLevel Nat
              | Type

    data Exp o = App (Elr o) (MArgList o)
               | Lam FMode (Abs (MExp o))
               | Fun FMode (MExp o) (MExp o)
               | Pi FMode Bool (MExp o) (Abs (MExp o))  -- true if possibly dependent (var not known to not occur)
               | Sort Sort

    type MExp o = MM (Exp o) (RefInfo o)

    data ArgList o = ALNil
                   | ALCons FMode (MExp o) (MArgList o)
                   | ALConPar (MArgList o)  -- inserted to cover glitch of polymorphic constructor applications coming from Agda

    type MArgList o = MM (ArgList o) (RefInfo o)

    data HNExp o = HNApp (Elr o) (CArgList o)
                 | HNLam (Abs (CExp o))
                 | HNFun FMode (CExp o) (CExp o)
                 | HNPi FMode Bool (CExp o) (Abs (CExp o))
                 | HNSort Sort

    data HNArgList o = HNALNil
                     | HNALCons (CExp o) (CArgList o)
                     | HNALConPar (CArgList o)

    type CExp o = Clos (MExp o) o

    data CArgList o = CALNil
                    | CALConcat (Clos (MArgList o) o) (CArgList o)
     -- !! (CALCons and CALConcat are used differently by eta rule in hncomp, but could replace those uses by a new CALSnoc construction)

    data Clos a o = Clos [CAction o] a

    data CAction o = Sub (CExp o)
                   | Skip
                   | Weak Nat

    type Ctx o = [(MId, CExp o)]

    type EE = IO

    data Elrs o = ElrsNil
                | ElrsCons (Elr o) (Elrs o)
                | ElrsWeak (Elrs o)