1
{-# OPTIONS -fglasgow-exts #-}
3
module Agda.Auto.Syntax where
7
import Agda.Auto.NarrowingSearch
10
data RefInfo o = RIEnv [ConstRef o]
11
| RIMainInfo Nat (HNExp o)
12
| forall a . RIUnifInfo (Metavar a (RefInfo o)) [CAction o] (HNExp o) -- metavar is the flexible side of the equality
14
type MyPB o = PB (RefInfo o)
15
type MyMB a o = MB a (RefInfo o)
26
data Abs a = Abs MId a
28
data ConstDef o = ConstDef {cdname :: String, cdorigin :: o, cdtype :: MExp o, cdcont :: DeclCont o} -- contains no metas
30
data DeclCont o = Def Nat [Clause o]
31
| Datatype [ConstRef o] -- constructors
35
type Clause o = ([Pat o], MExp o)
37
data Pat o = PatConApp (ConstRef o) [Pat o]
41
type ConstRef o = IORef (ConstDef o)
46
data Sort = SortLevel Nat
49
data Exp o = App (Elr o) (MArgList o)
50
| Lam FMode (Abs (MExp o))
51
| Fun FMode (MExp o) (MExp o)
52
| Pi FMode Bool (MExp o) (Abs (MExp o)) -- true if possibly dependent (var not known to not occur)
55
type MExp o = MM (Exp o) (RefInfo o)
57
data ArgList o = ALNil
58
| ALCons FMode (MExp o) (MArgList o)
59
| ALConPar (MArgList o) -- inserted to cover glitch of polymorphic constructor applications coming from Agda
61
type MArgList o = MM (ArgList o) (RefInfo o)
63
data HNExp o = HNApp (Elr o) (CArgList o)
64
| HNLam (Abs (CExp o))
65
| HNFun FMode (CExp o) (CExp o)
66
| HNPi FMode Bool (CExp o) (Abs (CExp o))
69
data HNArgList o = HNALNil
70
| HNALCons (CExp o) (CArgList o)
71
| HNALConPar (CArgList o)
73
type CExp o = Clos (MExp o) o
75
data CArgList o = CALNil
76
| CALConcat (Clos (MArgList o) o) (CArgList o)
77
-- !! (CALCons and CALConcat are used differently by eta rule in hncomp, but could replace those uses by a new CALSnoc construction)
79
data Clos a o = Clos [CAction o] a
81
data CAction o = Sub (CExp o)
85
type Ctx o = [(MId, CExp o)]
90
| ElrsCons (Elr o) (Elrs o)