src/HOLCF/cinfix.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/cinfix.ML
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
nipkow@243
     7
Some functions for the print and parse translation of continuous functions
nipkow@243
     8
nipkow@243
     9
Suppose the user introduces the following notation for the continuous
nipkow@243
    10
infixl . and the cont. infixr # with binding power 100
nipkow@243
    11
nipkow@243
    12
consts  
nipkow@243
    13
	"."     :: "'a => 'b => ('a**'b)" ("_._" [100,101] 100)
nipkow@243
    14
	"cop ." :: "'a -> 'b -> ('a**'b)" ("spair")
nipkow@243
    15
nipkow@243
    16
	"#"     :: "'a => 'b => ('a**'b)" ("_#_" [101,100] 100)
nipkow@243
    17
	"cop #" :: "'a -> 'b -> ('a**'b)" ("spair2")
nipkow@243
    18
nipkow@243
    19
the following functions are needed to set up proper translations
nipkow@243
    20
*)
nipkow@243
    21
nipkow@243
    22
(* -----------------------------------------------------------------------  
nipkow@243
    23
   a general purpose parse translation for continuous infix operators 
nipkow@243
    24
   this functions must be used for every cont. infix         
nipkow@243
    25
   ----------------------------------------------------------------------- *) 
nipkow@243
    26
nipkow@243
    27
fun mk_cinfixtr id =
nipkow@243
    28
	(fn ts =>
nipkow@243
    29
	let val Cfapp = Const("fapp",dummyT) in	
nipkow@243
    30
	Cfapp $ (Cfapp$Const("cop "^id,dummyT)$(nth_elem (0,ts)))$
nipkow@243
    31
	(nth_elem (1,ts))
nipkow@243
    32
	end);
nipkow@243
    33
nipkow@243
    34
nipkow@243
    35
nipkow@243
    36
(* -----------------------------------------------------------------------  
nipkow@243
    37
   make a print translation for a cont. infix operator "cop ???"    
nipkow@243
    38
   this is a print translation for fapp and is installed only once  
nipkow@243
    39
   special translations for other mixfixes (e.g. If_then_else_fi) are also 
nipkow@243
    40
   defined.
nipkow@243
    41
   ----------------------------------------------------------------------- *) 
nipkow@243
    42
nipkow@243
    43
fun fapptr' ts =
nipkow@243
    44
  case ts of
nipkow@243
    45
   [Const("fapp",T1)$Const(s,T2)$t1,t2] =>
nipkow@243
    46
	if ["c","o","p"," "] = take(4, explode s)
nipkow@243
    47
	  then Const(implode(drop(4, explode s)),dummyT)$t1$t2
nipkow@243
    48
	else raise Match
nipkow@243
    49
  | [Const("fapp",dummyT)$
nipkow@243
    50
	(Const("fapp",T1)$Const("Icifte",T2)$t)$e1,e2] 
nipkow@243
    51
      => Const("@cifte",dummyT)$t$e1$e2 
nipkow@243
    52
  | _ => raise Match;
nipkow@243
    53
nipkow@243
    54
nipkow@243
    55
(* -----------------------------------------------------------------------  
nipkow@243
    56
nipkow@243
    57
for the example above, the following must be setup in the ML section 
nipkow@243
    58
nipkow@243
    59
val parse_translation = [(".",mk_cinfixtr "."),
nipkow@243
    60
			 ("#",mk_cinfixtr "#")];
nipkow@243
    61
nipkow@243
    62
nipkow@243
    63
the print translation for fapp is setup only once in the system
nipkow@243
    64
nipkow@243
    65
val print_translation = [("fapp",fapptr')];
nipkow@243
    66
nipkow@243
    67
  ----------------------------------------------------------------------- *) 
nipkow@243
    68
nipkow@243
    69
nipkow@243
    70
nipkow@243
    71
nipkow@243
    72
nipkow@243
    73