equal
deleted
inserted
replaced
|
1 (* Title: ZF/Coind/Static.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 open BCR Static; |
|
8 |
|
9 val elab_constE = |
|
10 ElabRel.mk_cases Exp.con_defs "<te,e_const(c),t>:ElabRel"; |
|
11 |
|
12 val elab_varE = |
|
13 ElabRel.mk_cases Exp.con_defs "<te,e_var(x),t>:ElabRel"; |
|
14 |
|
15 val elab_fnE = |
|
16 ElabRel.mk_cases Exp.con_defs "<te,e_fn(x,e),t>:ElabRel"; |
|
17 |
|
18 val elab_fixE = |
|
19 ElabRel.mk_cases Exp.con_defs "<te,e_fix(f,x,e),t>:ElabRel"; |
|
20 |
|
21 val elab_appE = |
|
22 ElabRel.mk_cases Exp.con_defs "<te,e_app(e1,e2),t>:ElabRel"; |
|
23 |
|
24 fun mk_static_cs cs= |
|
25 let open ElabRel in |
|
26 ( cs |
|
27 addSIs [elab_constI,elab_varI,elab_fnI,elab_fixI] |
|
28 addSEs [elab_constE,elab_varE,elab_fixE] |
|
29 addIs [elab_appI] |
|
30 addEs [elab_appE,elab_fnE] |
|
31 addDs [ElabRel.dom_subset RS subsetD] |
|
32 ) end ; |
|
33 |
|
34 val static_cs = mk_static_cs ZF_cs; |
|
35 |
|
36 |
|
37 |
|
38 |
|
39 |
|
40 |