src/HOLCF/holcf_logic.ML
author wenzelm
Sat Jun 11 22:15:48 2005 +0200 (2005-06-11)
changeset 16364 dc9f7066d80a
parent 14981 e73f8140af78
child 16843 8ff9a80f3c93
permissions -rw-r--r--
refer to name spaces values instead of names;
     1 (*  Title:      HOLCF/holcf_logic.ML
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 
     5 Abstract syntax operations for HOLCF.
     6 *)
     7 
     8 infixr 6 ->>;
     9 
    10 signature HOLCF_LOGIC =
    11 sig
    12   val mk_btyp: string -> typ * typ -> typ
    13   val mk_prodT:          typ * typ -> typ
    14   val mk_not:  term -> term
    15 
    16   val HOLCF_sg: Sign.sg
    17   val pcpoC: class
    18   val pcpoS: sort
    19   val mk_TFree: string -> typ
    20   val cfun_arrow: string
    21   val ->>      : typ * typ -> typ
    22   val mk_ssumT : typ * typ -> typ
    23   val mk_sprodT: typ * typ -> typ
    24   val mk_uT: typ -> typ
    25   val trT: typ
    26   val oneT: typ
    27 
    28 end;
    29 
    30 
    31 structure HOLCFLogic: HOLCF_LOGIC =
    32 struct
    33 
    34 open HOLogic;
    35 
    36 fun mk_btyp t (S,T) = Type (t,[S,T]);
    37 val mk_prodT = mk_btyp "*";
    38 
    39 fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
    40 
    41 (* basics *)
    42 
    43 val HOLCF_sg    = sign_of HOLCF.thy;
    44 val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
    45 val pcpoS       = [pcpoC];
    46 fun mk_TFree s  = TFree ("'"^s, pcpoS);
    47 
    48 (*cfun, ssum, sprod, u, tr, one *)
    49 
    50 local val intern = Sign.intern_type HOLCF_sg;
    51 in
    52 val cfun_arrow = intern "->";
    53 val op   ->>  = mk_btyp cfun_arrow;
    54 val mk_ssumT  = mk_btyp (intern "++");
    55 val mk_sprodT = mk_btyp (intern "**");
    56 fun mk_uT T   = Type (intern "u"  ,[T]);
    57 val trT       = Type (intern "tr" ,[ ]);
    58 val oneT      = Type (intern "one",[ ]);
    59 end;
    60 
    61 end;