2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 open BCR Static; |
7 val elab_constE = ElabRel.mk_cases "<te,e_const(c),t>:ElabRel"; |
8 |
8 |
9 val elab_constE = |
9 val elab_varE = ElabRel.mk_cases "<te,e_var(x),t>:ElabRel"; |
10 ElabRel.mk_cases Exp.con_defs "<te,e_const(c),t>:ElabRel"; |
|
11 |
10 |
12 val elab_varE = |
11 val elab_fnE = ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel"; |
13 ElabRel.mk_cases Exp.con_defs "<te,e_var(x),t>:ElabRel"; |
|
14 |
12 |
15 val elab_fnE = |
13 val elab_fixE = ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel"; |
16 ElabRel.mk_cases Exp.con_defs "<te,e_fn(x,e),t>:ElabRel"; |
|
17 |
14 |
18 val elab_fixE = |
15 val elab_appE = ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel"; |
19 ElabRel.mk_cases Exp.con_defs "<te,e_fix(f,x,e),t>:ElabRel"; |
|
20 |
16 |
21 val elab_appE = |
17 AddSEs [elab_constE, elab_varE, elab_fixE]; |
22 ElabRel.mk_cases Exp.con_defs "<te,e_app(e1,e2),t>:ElabRel"; |
|
23 |
18 |
24 let open ElabRel in |
19 AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI]; |
25 claset_ref() := claset() addSIs [elab_constI,elab_varI,elab_fnI,elab_fixI] |
20 |
26 addSEs [elab_constE,elab_varE,elab_fixE] |
21 AddIs [ElabRel.appI]; |
27 addIs [elab_appI] |
22 |
28 addEs [elab_appE,elab_fnE] |
23 AddEs [elab_appE, elab_fnE]; |
29 addDs [ElabRel.dom_subset RS subsetD] |
24 |
30 end; |
25 AddDs [ElabRel.dom_subset RS subsetD]; |