src/HOLCF/holcf_logic.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 4129 2fd816aa6206
child 12030 46d57d0290a2
permissions -rw-r--r--
tidying
wenzelm@4129
     1
(*  Title:      HOLCF/holcf_logic.ML
wenzelm@4129
     2
    ID:         $Id$
wenzelm@4129
     3
    Author:     David von Oheimb
wenzelm@4129
     4
wenzelm@4129
     5
Abstract syntax operations for HOLCF.
wenzelm@4129
     6
*)
wenzelm@4129
     7
wenzelm@4129
     8
infixr 6 ->>;
wenzelm@4129
     9
wenzelm@4129
    10
signature HOLCF_LOGIC =
wenzelm@4129
    11
sig
wenzelm@4129
    12
  val mk_btyp: string -> typ * typ -> typ
wenzelm@4129
    13
  val mk_prodT:          typ * typ -> typ
wenzelm@4129
    14
  val mk_not:  term -> term
wenzelm@4129
    15
wenzelm@4129
    16
  val HOLCF_sg: Sign.sg
wenzelm@4129
    17
  val pcpoC: class
wenzelm@4129
    18
  val pcpoS: sort
wenzelm@4129
    19
  val mk_TFree: string -> typ
wenzelm@4129
    20
  val cfun_arrow: string
wenzelm@4129
    21
  val ->>      : typ * typ -> typ
wenzelm@4129
    22
  val mk_ssumT : typ * typ -> typ
wenzelm@4129
    23
  val mk_sprodT: typ * typ -> typ
wenzelm@4129
    24
  val mk_uT: typ -> typ
wenzelm@4129
    25
  val trT: typ
wenzelm@4129
    26
  val oneT: typ
wenzelm@4129
    27
wenzelm@4129
    28
end;
wenzelm@4129
    29
wenzelm@4129
    30
wenzelm@4129
    31
structure HOLCFLogic: HOLCF_LOGIC =
wenzelm@4129
    32
struct
wenzelm@4129
    33
wenzelm@4129
    34
local
wenzelm@4129
    35
wenzelm@4129
    36
  open HOLogic;
wenzelm@4129
    37
wenzelm@4129
    38
in
wenzelm@4129
    39
wenzelm@4129
    40
fun mk_btyp t (S,T) = Type (t,[S,T]);
wenzelm@4129
    41
val mk_prodT = mk_btyp "*";
wenzelm@4129
    42
wenzelm@4129
    43
fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
wenzelm@4129
    44
wenzelm@4129
    45
(* basics *)
wenzelm@4129
    46
wenzelm@4129
    47
val HOLCF_sg    = sign_of HOLCF.thy;
wenzelm@4129
    48
val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
wenzelm@4129
    49
val pcpoS       = [pcpoC];
wenzelm@4129
    50
fun mk_TFree s  = TFree ("'"^s, pcpoS);
wenzelm@4129
    51
wenzelm@4129
    52
(*cfun, ssum, sprod, u, tr, one *)
wenzelm@4129
    53
wenzelm@4129
    54
local val intern = Sign.intern_tycon HOLCF_sg;
wenzelm@4129
    55
in
wenzelm@4129
    56
val cfun_arrow = intern "->";
wenzelm@4129
    57
val op   ->>  = mk_btyp cfun_arrow;
wenzelm@4129
    58
val mk_ssumT  = mk_btyp (intern "++");
wenzelm@4129
    59
val mk_sprodT = mk_btyp (intern "**");
wenzelm@4129
    60
fun mk_uT T   = Type (intern "u"  ,[T]);
wenzelm@4129
    61
val trT       = Type (intern "tr" ,[ ]);
wenzelm@4129
    62
val oneT      = Type (intern "one",[ ]);
wenzelm@4129
    63
end;
wenzelm@4129
    64
wenzelm@4129
    65
end; (* local *)
wenzelm@4129
    66
end; (* struct *)