equal
deleted
inserted
replaced
21 datatype <= "univ(Ty Un ExVar)" |
21 datatype <= "univ(Ty Un ExVar)" |
22 "TyEnv" = te_emp |
22 "TyEnv" = te_emp |
23 | te_owr("te:TyEnv","x:ExVar","t:Ty") |
23 | te_owr("te:TyEnv","x:ExVar","t:Ty") |
24 |
24 |
25 consts |
25 consts |
26 te_rec :: [i,i,[i,i,i,i]=>i] => i |
|
27 defs |
|
28 te_rec_def |
|
29 "te_rec(te,c,h) == |
|
30 Vrec(te,%te g. TyEnv_case(c,%tem x t. h(tem,x,t,g`tem),te))" |
|
31 |
|
32 consts |
|
33 te_dom :: i => i |
26 te_dom :: i => i |
34 te_app :: [i,i] => i |
27 te_app :: [i,i] => i |
35 defs |
28 |
36 te_dom_def "te_dom(te) == te_rec(te,0,% te x t r. r Un {x})" |
29 |
37 te_app_def "te_app(te,x) == te_rec(te,0, % te y t r. if(x=y,t,r))" |
30 primrec (*domain of the type environment*) |
38 |
31 "te_dom (te_emp) = 0" |
|
32 "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}" |
|
33 |
|
34 primrec (*lookup up identifiers in the type environment*) |
|
35 "te_app (te_emp,x) = 0" |
|
36 "te_app (te_owr(te,y,t),x) = if(x=y, t, te_app(te,x))" |
39 |
37 |
40 end |
38 end |
41 |
39 |
42 |
40 |
43 |
41 |