src/ZF/Coind/Static.ML
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
expanded tabs
clasohm@1461
     1
(*  Title:      ZF/Coind/Static.ML
lcp@916
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
lcp@916
     4
    Copyright   1995  University of Cambridge
lcp@916
     5
*)
lcp@916
     6
lcp@916
     7
open BCR Static;
lcp@916
     8
lcp@916
     9
val elab_constE = 
lcp@916
    10
  ElabRel.mk_cases Exp.con_defs "<te,e_const(c),t>:ElabRel";
lcp@916
    11
lcp@916
    12
val elab_varE =
lcp@916
    13
  ElabRel.mk_cases Exp.con_defs "<te,e_var(x),t>:ElabRel";
lcp@916
    14
lcp@916
    15
val elab_fnE =
lcp@916
    16
  ElabRel.mk_cases Exp.con_defs "<te,e_fn(x,e),t>:ElabRel";
lcp@916
    17
lcp@916
    18
val elab_fixE =
lcp@916
    19
  ElabRel.mk_cases Exp.con_defs "<te,e_fix(f,x,e),t>:ElabRel";
lcp@916
    20
lcp@916
    21
val elab_appE = 
lcp@916
    22
  ElabRel.mk_cases Exp.con_defs "<te,e_app(e1,e2),t>:ElabRel";
lcp@916
    23
lcp@916
    24
fun mk_static_cs cs=
lcp@916
    25
  let open ElabRel in 
lcp@916
    26
  ( cs 
lcp@916
    27
    addSIs [elab_constI,elab_varI,elab_fnI,elab_fixI]
lcp@916
    28
    addSEs [elab_constE,elab_varE,elab_fixE]
lcp@916
    29
    addIs [elab_appI]
lcp@916
    30
    addEs [elab_appE,elab_fnE]
lcp@916
    31
    addDs [ElabRel.dom_subset RS subsetD]
lcp@916
    32
  ) end ;
lcp@916
    33
lcp@916
    34
val static_cs = mk_static_cs ZF_cs;
lcp@916
    35
lcp@916
    36
lcp@916
    37
lcp@916
    38
lcp@916
    39
lcp@916
    40