src/HOLCF/tr2.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
nipkow@243
     1
(*  Title: 	HOLCF/tr2.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Tr2 = Tr1 +
nipkow@243
    10
nipkow@243
    11
consts
nipkow@243
    12
	"@cifte"	:: "tr=>'c=>'c=>'c"
nipkow@243
    13
                             ("(3If _/ (then _/ else _) fi)" [60,60,60] 60)
nipkow@243
    14
	"Icifte"        :: "tr->'c->'c->'c"
nipkow@243
    15
nipkow@243
    16
	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [61,60] 60)
nipkow@243
    17
	"cop @andalso"	:: "tr -> tr -> tr" ("trand")
nipkow@243
    18
	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [61,60] 60)
nipkow@243
    19
	"cop @orelse"	:: "tr -> tr -> tr" ("tror")
nipkow@243
    20
nipkow@243
    21
nipkow@243
    22
rules
nipkow@243
    23
nipkow@243
    24
  ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
nipkow@243
    25
  andalso_def "trand == (LAM t1 t2.tr_when[t2][FF][t1])"
nipkow@243
    26
  orelse_def  "tror  == (LAM t1 t2.tr_when[TT][t2][t1])"
nipkow@243
    27
nipkow@243
    28
nipkow@243
    29
end
nipkow@243
    30
nipkow@243
    31
ML
nipkow@243
    32
nipkow@243
    33
(* ----------------------------------------------------------------------*)
nipkow@243
    34
(* translations for the above mixfixes                                   *)
nipkow@243
    35
(* ----------------------------------------------------------------------*)
nipkow@243
    36
nipkow@243
    37
fun ciftetr ts =
nipkow@243
    38
	let val Cfapp = Const("fapp",dummyT) in	
nipkow@243
    39
	Cfapp $ 
nipkow@243
    40
	   	(Cfapp $
nipkow@243
    41
			(Cfapp$Const("Icifte",dummyT)$(nth_elem (0,ts)))$
nipkow@243
    42
		(nth_elem (1,ts)))$
nipkow@243
    43
	(nth_elem (2,ts))
nipkow@243
    44
	end;
nipkow@243
    45
nipkow@243
    46
nipkow@243
    47
val parse_translation = [("@andalso",mk_cinfixtr "@andalso"),
nipkow@243
    48
			("@orelse",mk_cinfixtr "@orelse"),
nipkow@243
    49
			("@cifte",ciftetr)];
nipkow@243
    50
nipkow@243
    51
val print_translation = [];
nipkow@243
    52
nipkow@243
    53
nipkow@243
    54
nipkow@243
    55
nipkow@243
    56