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