1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
module GF.Devel.Grammar.Grammar where
import GF.Infra.Ident
import GF.Data.Operations
import Data.Map
------------------
-- definitions --
------------------
data GF = GF {
gfabsname :: Maybe Ident ,
gfcncnames :: [Ident] ,
gflags :: Map Ident String , -- value of a global flag
gfmodules :: Map Ident Module
}
data Module = Module {
mtype :: ModuleType,
miscomplete :: Bool,
minterfaces :: [(Ident,Ident)], -- non-empty for functors
minstances :: [((Ident,MInclude),[(Ident,Ident)])], -- non-empty for inst'ions
mextends :: [(Ident,MInclude)],
mopens :: [(Ident,Ident)], -- used name, original name
mflags :: Map Ident String,
mjments :: Map Ident Judgement
}
data ModuleType =
MTAbstract
| MTConcrete Ident
| MTInterface
| MTInstance Ident
| MTGrammar
deriving Eq
data MInclude =
MIAll
| MIExcept [Ident]
| MIOnly [Ident]
type Indirection = (Ident,Bool) -- module of origin, whether canonical
data Judgement = Judgement {
jform :: JudgementForm, -- cat fun lincat lin oper param
jtype :: Type, -- context type lincat - type PType
jdef :: Term, -- lindef def lindef lin def constrs
jprintname :: Term, -- - - prname prname - -
jlink :: Ident, -- if inherited, the supermodule name, else #
jposition :: Int -- line number where def begins
}
deriving Show
data JudgementForm =
JCat
| JFun
| JLincat
| JLin
| JOper
| JParam
| JLink
deriving (Eq,Show)
type Type = Term
data Term =
Vr Ident -- ^ variable
| Con Ident -- ^ constructor
| EData -- ^ to mark in definition that a fun is a constructor
| Sort String -- ^ predefined type
| EInt Integer -- ^ integer literal
| EFloat Double -- ^ floating point literal
| K String -- ^ string literal or token: @\"foo\"@
| Empty -- ^ the empty string @[]@
| App Term Term -- ^ application: @f a@
| Abs Ident Term -- ^ abstraction: @\x -> b@
| Meta MetaSymb -- ^ metavariable: @?i@ (only parsable: ? = ?0)
| Prod Ident Term Term -- ^ function type: @(x : A) -> B@
| Eqs [Equation] -- ^ abstraction by cases: @fn {x y -> b ; z u -> c}@
-- only used in internal representation
| Typed Term Term -- ^ type-annotated term
--
-- /below this, the constructors are only for concrete syntax/
| Example Term String -- ^ example-based term: @in M.C "foo"
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
| R [Assign] -- ^ record: @{ p = a ; ...}@
| P Term Label -- ^ projection: @r.p@
| PI Term Label Int -- ^ index-annotated projection
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
| Table Term Term -- ^ table type: @P => A@
| T TInfo [Case] -- ^ table: @table {p => c ; ...}@
| V Type [Term] -- ^ course of values: @table T [c1 ; ... ; cn]@
| S Term Term -- ^ selection: @t ! p@
| Val Type Int -- ^ parameter value number: @T # i#
| Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@
| Q Ident Ident -- ^ qualified constant from a module
| QC Ident Ident -- ^ qualified constructor from a module
| C Term Term -- ^ concatenation: @s ++ t@
| Glue Term Term -- ^ agglutination: @s + t@
| EPatt Patt
| EPattType Term
| EParam Term [(Ident,Context)] -- to encode parameter constructor sets
| FV [Term] -- ^ free variation: @variants { s ; ... }@
| Alts (Term, [(Term, Term)]) -- ^ prefix-dependent: @pre {t ; s\/c ; ...}@
| Overload [(Type,Term)]
deriving (Read, Show, Eq, Ord)
data Patt =
PC Ident [Patt] -- ^ constructor pattern: @C p1 ... pn@ @C@
| PP Ident Ident [Patt] -- ^ qualified constr patt: @P.C p1 ... pn@ @P.C@
| PV Ident -- ^ variable pattern: @x@
| PW -- ^ wild card pattern: @_@
| PR [(Label,Patt)] -- ^ record pattern: @{r = p ; ...}@
| PString String -- ^ string literal pattern: @\"foo\"@
| PInt Integer -- ^ integer literal pattern: @12@
| PFloat Double -- ^ float literal pattern: @1.2@
| PT Type Patt -- ^ type-annotated pattern
| PAs Ident Patt -- ^ as-pattern: x@p
-- regular expression patterns
| PNeg Patt -- ^ negated pattern: -p
| PAlt Patt Patt -- ^ disjunctive pattern: p1 | p2
| PSeq Patt Patt -- ^ sequence of token parts: p + q
| PRep Patt -- ^ repetition of token part: p*
| PChar -- ^ string of length one: ?
| PChars String -- ^ list of characters: ["aeiou"]
| PMacro Ident -- #p
| PM Ident Ident -- #m.p
deriving (Read, Show, Eq, Ord)
-- | to guide computation and type checking of tables
data TInfo =
TRaw -- ^ received from parser; can be anything
| TTyped Type -- ^ type annotated, but can be anything
| TComp Type -- ^ expanded
| TWild Type -- ^ just one wild card pattern, no need to expand
deriving (Read, Show, Eq, Ord)
-- | record label
data Label =
LIdent String
| LVar Int
deriving (Read, Show, Eq, Ord)
type MetaSymb = Int
type Decl = (Ident,Term) -- (x:A) (_:A) A
type Context = [Decl] -- (x:A)(y:B) (x,y:A) (_,_:A)
type Substitution = [(Ident, Term)]
type Equation = ([Patt],Term)
type Labelling = (Label, Term)
type Assign = (Label, (Maybe Type, Term))
type Case = (Patt, Term)
type LocalDef = (Ident, (Maybe Type, Term))
|
