parser.mly (10241B)
1 %{ 2 open Util 3 open Node 4 module E = Error 5 module C = Concrete 6 7 (* To avoid reduce-reduce conflicts, we need to distinguish between raw 8 * expressions (which are generally of unknown syntactic category) and concrete 9 * terms/patterns/etc. In a hand-written parser, we'd have more control over 10 * when to decide the syntactic category of the top of the token stack, so 11 * we wouldn't need to make this distinction. 12 * 13 * We use (length, list) pairs in exprs, because we don't know how long the 14 * lists will be until after parsing, but we convert to arrays for efficiency 15 * and convenience in concrete syntax and onwards. *) 16 type expr = expr' node 17 and expr' = 18 | Let of int * C.definer list * expr 19 | Seq of expr * expr 20 | Match of expr * int * C.case list 21 | If of C.cond * expr * expr 22 | Iff of C.cond * expr 23 | Annot of expr * expr 24 | BinOp of expr * C.binop * expr 25 | Or of expr * expr 26 | And of expr * expr 27 | App of expr * int * expr list 28 | Fn of int * C.param list * expr 29 | FnType of int * C.domain list * expr 30 | Variant of C.tag_name * int * expr list 31 | VariantType of int * ctor list 32 | Tuple of int * expr list 33 | TupleType of int * C.domain list 34 | Unit 35 | Nat of Z.t 36 | Underscore 37 | IndexedVar of C.var_name * int 38 | Var of C.var_name 39 | Paren of expr 40 41 and ctor = ctor' node 42 and ctor' = Ctor of C.tag_name * int * C.domain list 43 44 let cons a (len, lst) = (len + 1, a :: lst) 45 46 let to_array len lst = 47 let arr = Array.make len garbage in 48 List.iteri (Array.set arr) lst; 49 arr 50 51 let rec term {loc; data = e} = loc @$ match e with 52 | Let (len, definers, body) -> C.Let (to_array len definers, term body) 53 | Seq (a, b) -> C.Seq (term a, term b) 54 | Match (scrutinee, len, cases) -> C.Match (term scrutinee, to_array len cases) 55 | If (c, t, f) -> C.If (c, term t, term f) 56 | Iff (c, t) -> C.Iff (c, term t) 57 | Annot (a, b) -> C.Annot (term a, term b) 58 | BinOp (a, o, b) -> C.BinOp (term a, o, term b) 59 | Or _ -> E.abort loc E.ParserInvalidTerm 60 | And _ -> E.abort loc E.ParserInvalidTerm 61 | App (f, len, args) -> C.App (term f, Array.map term (to_array len args)) 62 | Fn (len, params, body) -> C.Fn (to_array len params, term body) 63 | FnType (len, doms, cod) -> C.FnType (to_array len doms, term cod) 64 | Variant (tag, len, fields) -> C.Variant (tag, Array.map term (to_array len fields)) 65 | VariantType (len, ctors) -> C.VariantType (Array.map ctor (to_array len ctors)) 66 | Tuple (len, fields) -> C.Tuple (Array.map term (to_array len fields)) 67 | TupleType (len, doms) -> C.TupleType (to_array len doms) 68 | Unit -> C.Unit 69 | Nat n -> C.Nat n 70 | Underscore -> E.abort loc E.ParserInvalidTerm 71 | IndexedVar (x, i) -> C.IndexedVar (x, i) 72 | Var x -> C.Var x 73 | Paren e -> C.Paren (term e) 74 75 and ctor {loc; data = Ctor (tag, len, doms)} = 76 loc @$ C.Ctor (tag, to_array len doms) 77 78 and patt {loc; data = e} = loc @$ match e with 79 | Annot (p, t) -> C.PAnnot (patt p, term t) 80 | Or (p, q) -> C.POr (patt p, patt q) 81 | And (p, q) -> C.PAnd (patt p, patt q) 82 | Variant (tag, len, ps) -> C.PVariant (tag, Array.map patt (to_array len ps)) 83 | Tuple (len, ps) -> C.PTuple (Array.map patt (to_array len ps)) 84 | Unit -> C.PUnit 85 | Nat n -> C.PNat n 86 | Underscore -> C.PWild 87 | Var x -> C.PBind x 88 | Paren p -> C.PParen (patt p) 89 | Let _ | Seq _ | Match _ | If _ | Iff _ | BinOp _ | App _ 90 | Fn _ | FnType _ | VariantType _ | TupleType _ | IndexedVar _ -> 91 E.abort loc E.ParserInvalidPatt 92 93 let loc_of i = 94 let beg_pos = Parsing.rhs_start_pos i in 95 let end_pos = Parsing.rhs_end_pos i in 96 Loc.of_positions beg_pos end_pos 97 98 let loc () = 99 let beg_pos = Parsing.symbol_start_pos () in 100 let end_pos = Parsing.symbol_end_pos () in 101 Loc.of_positions beg_pos end_pos 102 %} 103 104 %token EOF 105 %token SEMICOLON COLON COMMA COLON_EQ QUESTION 106 %token SINGLE_ARROW DOUBLE_ARROW 107 %token HASH_LPAREN LPAREN RPAREN 108 %token LBRACK RBRACK 109 %token HASH_LBRACE LBRACE RBRACE 110 %token PIPE2 AMPERSAND2 111 %token LT LE EQ GE GT NE 112 %token PLUS MINUS ASTERISK SLASH PERCENT 113 %token PIPE AMPERSAND 114 %token REC MATCH IF THEN ELSE IFF DO FN 115 %token UNDERSCORE 116 %token <string> TAG 117 %token <string * int> INDEXED_NAME 118 %token <string> NAME 119 %token <Z.t> NAT 120 121 %start start 122 %type <Concrete.term> start 123 124 %% 125 126 (* TODO: Syntactic sugar: Allow application in patterns, with the following 127 * interpretation: 128 * p p1 ... pn := rec? b ---> p := rec? fn p1, ..., pn => b 129 * fn ..., p(p1 ... pn), ... => b ---> fn ..., p1, ..., pn, ... => b 130 * The pattern p in the second rule is restricted to being a composition of 131 * PParen and PAnnot. Note that application of the first rule may make the 132 * second rule applicable, and application of the second rule may need to be 133 * iterated until we reach a "normal form". *) 134 (* TODO: Probably we should change the match syntax when staging is added, 135 * so that we can write something like `$match x ...` instead of 136 * `$(x match ...)` for conditional compilation. *) 137 (* TODO: Chaining relations? I.e., ability to write x < y < z instead of 138 * x < y && y < z. *) 139 140 start: expr0 EOF { term $1 } 141 | error { E.abort (loc_of 1) @@ E.ParserNoRule } 142 143 expr0: (* Definitions and sequencing *) 144 | definer_list SEMICOLON expr0 { 145 let (len, lst) = $1 in 146 loc () @$ Let (len, lst, $3) 147 } 148 | expr1 SEMICOLON expr0 { loc () @$ Seq ($1, $3) } 149 | expr1 { $1 } 150 151 expr1: 152 | expr1r COLON expr1l { loc () @$ Annot ($1, $3) } 153 | expr1ll { $1 } 154 | expr1rr { $1 } 155 | expr2 { $1 } 156 157 expr1l: (* Prec 1 with a terminal to the left, OR prec >1 *) 158 | expr1ll { $1 } 159 | expr2 { $1 } 160 expr1ll: (* Prec 1 with a terminal to the left *) 161 | IF cond THEN expr1 ELSE expr1l { loc () @$ If ($2, $4, $6) } 162 | IFF cond DO expr1l { loc () @$ Iff ($2, $4) } 163 | FN param_list DOUBLE_ARROW expr1 { 164 let (len, lst) = $2 in 165 loc () @$ Fn (len, lst, $4) 166 } 167 168 expr1r: (* Prec 1 with a terminal to the right, OR prec >1 *) 169 | expr1rr { $1 } 170 | expr2 { $1 } 171 expr1rr: (* Prec 1 with a terminal to the right *) 172 | expr1r MATCH LBRACE case_list RBRACE { 173 let (len, lst) = $4 in 174 loc () @$ Match($1, len, lst) 175 } 176 177 (* TODO: Remove this and shift all precedences? Ughh. *) 178 expr2: expr3 { $1 } 179 180 expr3: (* Function arrow (right-associative) *) 181 | expr5 SINGLE_ARROW expr3 { 182 let dom = loc_of 1 @$ C.ExplicitDomain (term $1) in 183 loc () @$ FnType (1, [dom], $3) 184 } 185 | LBRACK domain_list RBRACK SINGLE_ARROW expr3 { 186 let (len, lst) = $2 in 187 if len = 0 then 188 E.abort (loc_of 2) E.ParserEmptyDomain 189 else 190 loc () @$ FnType (len, lst, $5) 191 } 192 | expr4 { $1 } 193 194 expr4: expr4a { $1 } (* Binary operators and relations *) 195 196 expr4a: (* Logical OR (left-associative) *) 197 | expr4a PIPE2 expr4b { loc () @$ BinOp ($1, C.LAnd, $3) } 198 | expr4b { $1 } 199 200 expr4b: (* Logical AND (left-associative) *) 201 | expr4b AMPERSAND2 expr4c { loc () @$ BinOp ($1, C.LOr, $3) } 202 | expr4c { $1 } 203 204 expr4c: (* Relations (non-associative) *) 205 | expr4d rel expr4d { loc () @$ BinOp ($1, $2, $3) } 206 | expr4d { $1 } 207 rel: 208 | LT { C.Lt } 209 | LE { C.Le } 210 | EQ { C.Eq } 211 | GE { C.Ge } 212 | GT { C.Gt } 213 | NE { C.Ne } 214 215 expr4d: (* Additive operators (left-associative) *) 216 | expr4d0 addop expr4e { loc () @$ BinOp ($1, $2, $3) } 217 | expr4d1 PIPE expr4e { loc () @$ Or ($1, $3) } 218 | expr4e { $1 } 219 addop: 220 | PLUS { C.Add } 221 | MINUS { C.Sub } 222 expr4d0: 223 | expr4d0 addop expr4e { loc () @$ BinOp ($1, $2, $3) } 224 | expr4e { $1 } 225 expr4d1: 226 | expr4d1 PIPE expr4e { loc () @$ Or ($1, $3) } 227 | expr4e { $1 } 228 229 expr4e: (* Multiplicative operators (left-associative) *) 230 | expr4e0 mulop expr4f { loc () @$ BinOp ($1, $2, $3) } 231 | expr4e1 AMPERSAND expr4f { loc () @$ And ($1, $3) } 232 | expr4f { $1 } 233 mulop: 234 | ASTERISK { C.Mul } 235 | SLASH { C.Div } 236 | PERCENT { C.Mod } 237 expr4e0: 238 | expr4e0 mulop expr4f { loc () @$ BinOp ($1, $2, $3) } 239 | expr4f { $1 } 240 expr4e1: 241 | expr4e1 AMPERSAND expr4f { loc () @$ And ($1, $3) } 242 | expr4f { $1 } 243 244 expr4f: expr5 { $1 } 245 246 expr5: 247 | expr6 expr6 expr6_apposition_list { 248 let (len, lst) = cons $2 $3 in 249 match $1.data with 250 | Variant (tag, 0, []) -> 251 loc () @$ Variant (tag, len, lst) 252 | _ -> 253 loc () @$ App ($1, len, lst) 254 } 255 | expr6 { $1 } 256 257 expr6: 258 | UNDERSCORE { loc () @$ Underscore } 259 | indexed_var_name { 260 let (x, i) = $1 in 261 loc () @$ IndexedVar (x, i) 262 } 263 | var_name { loc () @$ Var $1 } 264 | NAT { loc () @$ Nat $1 } 265 | tag_name { loc () @$ Variant ($1, 0, []) } 266 | HASH_LBRACE ctor_list RBRACE { 267 let (len, lst) = $2 in 268 loc () @$ VariantType (len, lst) 269 } 270 | LPAREN expr1 COMMA expr1_comma_list RPAREN { 271 let (len, lst) = $4 in 272 loc () @$ Tuple (len + 1, $2 :: lst) 273 } 274 | HASH_LPAREN domain_list RPAREN { 275 let (len, lst) = $2 in 276 loc () @$ TupleType (len, lst) 277 } 278 | LPAREN RPAREN { loc () @$ Unit } 279 | LPAREN expr0 RPAREN { loc () @$ Paren $2 } 280 281 expr1_comma_list: 282 | expr1 COMMA expr1_comma_list { cons $1 $3 } 283 | expr1 { (1, [$1]) } 284 | { (0, []) } 285 286 expr6_apposition_list: 287 | expr6 expr6_apposition_list { cons $1 $2 } 288 | { (0, []) } 289 290 definer: 291 | expr1 COLON_EQ expr1 { loc () @$ C.Definer (patt $1, term $3) } 292 | expr1 COLON_EQ REC expr1 { loc () @$ C.RecDefiner (patt $1, term $4) } 293 definer_list: 294 | definer COMMA definer_list { cons $1 $3 } 295 | definer { (1, [$1]) } 296 297 case: 298 | expr1 DOUBLE_ARROW expr1 { loc () @$ C.Case (patt $1, term $3) } 299 case_list: 300 | case COMMA case_list { cons $1 $3 } 301 | case { (1, [$1]) } 302 | { (0, []) } 303 304 cond: 305 | expr1 { loc () @$ C.TrueCond (term $1) } 306 | expr1 COLON_EQ expr1 { loc () @$ C.PattCond (patt $1, term $3) } 307 308 param: 309 | expr1 { loc () @$ C.Param (Plicity.Ex, patt $1) } 310 | QUESTION expr1 { loc () @$ C.Param (Plicity.Im, patt $2) } 311 param_list: 312 | param COMMA param_list { cons $1 $3 } 313 | param { (1, [$1]) } 314 | { (0, []) } 315 316 domain: 317 | expr1 { 318 match $1.data with 319 | Annot (p, t) -> loc () @$ C.AnnotDomain (Plicity.Ex, patt p, term t) 320 | _ -> loc () @$ C.ExplicitDomain (term $1) 321 } 322 | QUESTION expr1 { 323 match $2.data with 324 | Annot (p, t) -> loc () @$ C.AnnotDomain (Plicity.Im, patt p, term t) 325 | _ -> loc () @$ C.ImplicitTypeDomain (patt $2) 326 } 327 domain_list: 328 | domain COMMA domain_list { cons $1 $3 } 329 | domain { (1, [$1]) } 330 | { (0, []) } 331 332 tag_name: 333 | TAG { loc () @$ Name.Tag.Of $1 } 334 335 indexed_var_name: 336 | INDEXED_NAME { 337 let (x, i) = $1 in 338 (loc () @$ Name.Var.Of x, i) 339 } 340 341 var_name: 342 | NAME { loc () @$ Name.Var.Of $1 } 343 344 ctor: 345 | tag_name domain_list { 346 let (len, lst) = $2 in 347 loc () @$ Ctor ($1, len, lst) 348 } 349 ctor_list: 350 | ctor SEMICOLON ctor_list { cons $1 $3 } 351 | ctor { (1, [$1]) } 352 | { (0, []) } 353 354 %%