src/HOLCF/holcf_logic.ML
author wenzelm
Thu Jul 14 19:28:25 2005 +0200 (2005-07-14)
changeset 16843 8ff9a80f3c93
parent 16364 dc9f7066d80a
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
removed mk_prodT, mk_not (cf. HOL/hologic.ML);
tuned;
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 pcpoC: class
wenzelm@4129
    14
  val pcpoS: sort
wenzelm@4129
    15
  val mk_TFree: string -> typ
wenzelm@4129
    16
  val cfun_arrow: string
wenzelm@16843
    17
  val ->> : typ * typ -> typ
wenzelm@16843
    18
  val mk_ssumT: typ * typ -> typ
wenzelm@4129
    19
  val mk_sprodT: typ * typ -> typ
wenzelm@4129
    20
  val mk_uT: typ -> typ
wenzelm@4129
    21
  val trT: typ
wenzelm@4129
    22
  val oneT: typ
wenzelm@4129
    23
end;
wenzelm@4129
    24
wenzelm@4129
    25
structure HOLCFLogic: HOLCF_LOGIC =
wenzelm@4129
    26
struct
wenzelm@4129
    27
wenzelm@16843
    28
(* sort pcpo *)
wenzelm@16843
    29
wenzelm@16843
    30
val pcpoC = Sign.intern_class (the_context ()) "pcpo";
wenzelm@16843
    31
val pcpoS = [pcpoC];
wenzelm@16843
    32
fun mk_TFree s = TFree ("'" ^ s, pcpoS);
wenzelm@16843
    33
wenzelm@16843
    34
wenzelm@16843
    35
(* basic types *)
wenzelm@4129
    36
wenzelm@4129
    37
fun mk_btyp t (S,T) = Type (t,[S,T]);
wenzelm@4129
    38
wenzelm@16843
    39
local
wenzelm@16843
    40
  val intern_type = Sign.intern_type (the_context ());
wenzelm@16843
    41
  val u = intern_type "u";
wenzelm@16843
    42
in
wenzelm@4129
    43
wenzelm@16843
    44
val cfun_arrow = intern_type "->";
wenzelm@16843
    45
val op ->> = mk_btyp cfun_arrow;
wenzelm@16843
    46
val mk_ssumT = mk_btyp (intern_type "++");
wenzelm@16843
    47
val mk_sprodT = mk_btyp (intern_type "**");
wenzelm@16843
    48
fun mk_uT T = Type (u, [T]);
wenzelm@16843
    49
val trT = Type (intern_type "tr" , []);
wenzelm@16843
    50
val oneT = Type (intern_type "one", []);
wenzelm@4129
    51
wenzelm@4129
    52
end;
wenzelm@4129
    53
wenzelm@12030
    54
end;