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)