Mercurial > urweb
comparison src/urweb.grm @ 705:e6706a1df013
Track uniqueness sets in table types
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 07 Apr 2009 14:11:32 -0400 |
parents | 70cbdcf5989b |
children | 1fb318c17546 |
comparison
equal
deleted
inserted
replaced
704:70cbdcf5989b | 705:e6706a1df013 |
---|---|
292 | 292 |
293 | query of exp | 293 | query of exp |
294 | query1 of exp | 294 | query1 of exp |
295 | tables of (con * exp) list | 295 | tables of (con * exp) list |
296 | tname of con | 296 | tname of con |
297 | tnameW of (con * con) | 297 | tnameW of con * con |
298 | tnames of con | 298 | tnames of (con * con) * (con * con) list |
299 | tnames' of (con * con) list | 299 | tnames' of (con * con) * (con * con) list |
300 | table of con * exp | 300 | table of con * exp |
301 | tident of con | 301 | tident of con |
302 | fident of con | 302 | fident of con |
303 | seli of select_item | 303 | seli of select_item |
304 | selis of select_item list | 304 | selis of select_item list |
491 | 491 |
492 cst : UNIQUE tnames (let | 492 cst : UNIQUE tnames (let |
493 val loc = s (UNIQUEleft, tnamesright) | 493 val loc = s (UNIQUEleft, tnamesright) |
494 | 494 |
495 val e = (EVar (["Basis"], "unique", Infer), loc) | 495 val e = (EVar (["Basis"], "unique", Infer), loc) |
496 val e = (ECApp (e, tnames), loc) | 496 val e = (ECApp (e, #1 (#1 tnames)), loc) |
497 val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc) | |
498 val e = (EDisjointApp e, loc) | |
497 in | 499 in |
498 (EDisjointApp e, loc) | 500 (EDisjointApp e, loc) |
499 end) | 501 end) |
500 | LBRACE eexp RBRACE (eexp) | 502 | LBRACE eexp RBRACE (eexp) |
501 | 503 |
503 val loc = s (tnameleft, tnameright) | 505 val loc = s (tnameleft, tnameright) |
504 in | 506 in |
505 (tname, (CWild (KType, loc), loc)) | 507 (tname, (CWild (KType, loc), loc)) |
506 end) | 508 end) |
507 | 509 |
508 tnames : tnameW (CRecord [tnameW], s (tnameWleft, tnameWright)) | 510 tnames : tnameW (tnameW, []) |
509 | LPAREN tnames' RPAREN (CRecord tnames', s (LPARENleft, RPARENright)) | 511 | LPAREN tnames' RPAREN (tnames') |
510 | LBRACE LBRACE cexp RBRACE RBRACE (cexp) | 512 |
511 | 513 tnames': tnameW (tnameW, []) |
512 tnames': tnameW ([tnameW]) | 514 | tnameW COMMA tnames' (#1 tnames', tnameW :: #2 tnames') |
513 | tnameW COMMA tnames' (tnameW :: tnames') | |
514 | 515 |
515 valis : vali ([vali]) | 516 valis : vali ([vali]) |
516 | vali AND valis (vali :: valis) | 517 | vali AND valis (vali :: valis) |
517 | 518 |
518 sgn : sgntm (sgntm) | 519 sgn : sgntm (sgntm) |