spec/spectec/src/il/ast.ml at 864f5518deae6dbc4e36dc657b078da5e0ae1064 · WebAssembly/spec · GitHub

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
173
174
175
176
177
open Util.Source
open Xl


(* Terminals *)

type num = Num.num
type text = string
type id = string phrase
type atom = Atom.atom
type mixop = unit Mixop.mixop


(* Iteration *)

type iter =
  | Opt                          (* `?` *)
  | List                         (* `*` *)
  | List1                        (* `+` *)
  | ListN of exp * id option     (* `^` exp *)


(* Types *)

and numtyp = Num.typ
and optyp = [Bool.typ | Num.typ]

and typ = typ' phrase
and typ' =
  | VarT of id * arg list        (* typid( arg* ) *)
  | BoolT                        (* `bool` *)
  | NumT of numtyp               (* numtyp *)
  | TextT                        (* `text` *)
  | TupT of (id * typ) list      (* (id : typ, ..., id : typ) *)
  | IterT of typ * iter          (* typ iter *)

and deftyp = deftyp' phrase
and deftyp' =
  | AliasT of typ                (* type alias *)
  | StructT of typfield list     (* record type *)
  | VariantT of typcase list     (* variant type *)

and typfield = atom * (typ * quant list * prem list) * hint list  (* record field *)
and typcase = mixop * (typ * quant list * prem list) * hint list  (* variant case *)


(* Expressions *)

and unop = [Bool.unop | Num.unop]
and binop = [Bool.binop | Num.binop]
and cmpop = [Bool.cmpop | Num.cmpop]

and exp = (exp', typ) note_phrase
and exp' =
  | VarE of id                              (* varid *)
  | BoolE of bool                           (* bool *)
  | NumE of num                             (* num *)
  | TextE of text                           (* text *)
  | UnE of unop * optyp * exp               (* unop exp *)
  | BinE of binop * optyp * exp * exp       (* exp binop exp *)
  | CmpE of cmpop * optyp * exp * exp       (* exp cmpop exp *)
  | TupE of exp list                        (* ( exp* ) *)
  | ProjE of exp * int                      (* exp.i *)
  | CaseE of mixop * exp                    (* atom exp? *)
  | UncaseE of exp * mixop                  (* exp!mixop *)
  | OptE of exp option                      (* exp? *)
  | TheE of exp                             (* exp! *)
  | StrE of expfield list                   (* { expfield* } *)
  | DotE of exp * atom                      (* exp.atom *)
  | CompE of exp * exp                      (* exp @ exp *)
  | ListE of exp list                       (* [exp ... exp] *)
  | LiftE of exp                            (* exp : _? <: _* *)
  | MemE of exp * exp                       (* exp `<-` exp *)
  | LenE of exp                             (* |exp| *)
  | CatE of exp * exp                       (* exp :: exp *)
  | IdxE of exp * exp                       (* exp[exp]` *)
  | SliceE of exp * exp * exp               (* exp[exp : exp] *)
  | UpdE of exp * path * exp                (* exp[path = exp] *)
  | ExtE of exp * path * exp                (* exp[path =.. exp] *)
  | CallE of id * arg list                  (* defid( arg* ) *)
  | IterE of exp * iterexp                  (* exp iter *)
  | CvtE of exp * numtyp * numtyp           (* exp : typ1 <:> typ2 *)
  | SubE of exp * typ * typ                 (* exp : typ1 <: typ2 *)
  | AnnE of exp * typ                       (* exp : typ *)

and expfield = atom * exp                   (* atom exp *)

and path = (path', typ) note_phrase
and path' =
  | RootP                                   (*  *)
  | IdxP of path * exp                      (* path[exp] *)
  | SliceP of path * exp * exp              (* path[exp : exp] *)
  | DotP of path * atom                     (* path.atom *)

and iterexp = iter * (id * exp) list


(* Grammars *)

and sym = sym' phrase
and sym' =
  | VarG of id * arg list                   (* gramid( arg* ) *)
  | NumG of int                             (* num *)
  | TextG of string                         (* text *)
  | EpsG                                    (* epsilon *)
  | SeqG of sym list                        (* sym sym *)
  | AltG of sym list                        (* sym | sym *)
  | RangeG of sym * sym                     (* sym | ... | sym *)
  | IterG of sym * iterexp                  (* sym iter *)
  | AttrG of exp * sym                      (* exp : sym *)


(* Definitions *)

and arg = arg' phrase
and arg' =
  | ExpA of exp                             (* exp *)
  | TypA of typ                             (* `syntax` typ *)
  | DefA of id                              (* `def` defid *)
  | GramA of sym                            (* `grammar` sym *)

and param = param' phrase
and param' =
  | ExpP of id * typ                        (* varid : typ *)
  | TypP of id                              (* `syntax` varid *)
  | DefP of id * param list * typ           (* `def` defid params : typ *)
  | GramP of id * param list * typ          (* `grammar` gramid param : typ *)

and quant = param

and def = def' phrase
and def' =
  | TypD of id * param list * inst list               (* syntax type (family) *)
  | RelD of id * param list * mixop * typ * rule list (* relation *)
  | DecD of id * param list * typ * clause list       (* definition *)
  | GramD of id * param list * typ * prod list        (* grammar *)
  | RecD of def list                                  (* recursive *)
  | HintD of hintdef

and inst = inst' phrase
and inst' =
  | InstD of quant list * arg list * deftyp           (* family instance clause *)

and rule = rule' phrase
and rule' =
  | RuleD of id * quant list * mixop * exp * prem list (* relation rule *)

and clause = clause' phrase
and clause' =
  | DefD of quant list * arg list * exp * prem list   (* definition clause *)

and prod = prod' phrase
and prod' =
  | ProdD of quant list * sym * exp * prem list       (* grammar production *)

and prem = prem' phrase
and prem' =
  | RulePr of id * arg list * mixop * exp             (* premise *)
  | IfPr of exp                                       (* side condition *)
  | LetPr of exp * exp * string list                  (* binding *)
  | ElsePr                                            (* otherwise *)
  | IterPr of prem * iterexp                          (* iteration *)

and hintdef = hintdef' phrase
and hintdef' =
  | TypH of id * hint list
  | RelH of id * hint list
  | DecH of id * hint list
  | GramH of id * hint list
  | RuleH of id * id * hint list

and hint = {hintid : id; hintexp : El.Ast.exp}        (* hint *)


(* Scripts *)

type script = def list