--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/cinfix.ML Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,73 @@
+(* Title: HOLCF/cinfix.ML
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+
+Some functions for the print and parse translation of continuous functions
+
+Suppose the user introduces the following notation for the continuous
+infixl . and the cont. infixr # with binding power 100
+
+consts
+ "." :: "'a => 'b => ('a**'b)" ("_._" [100,101] 100)
+ "cop ." :: "'a -> 'b -> ('a**'b)" ("spair")
+
+ "#" :: "'a => 'b => ('a**'b)" ("_#_" [101,100] 100)
+ "cop #" :: "'a -> 'b -> ('a**'b)" ("spair2")
+
+the following functions are needed to set up proper translations
+*)
+
+(* -----------------------------------------------------------------------
+ a general purpose parse translation for continuous infix operators
+ this functions must be used for every cont. infix
+ ----------------------------------------------------------------------- *)
+
+fun mk_cinfixtr id =
+ (fn ts =>
+ let val Cfapp = Const("fapp",dummyT) in
+ Cfapp $ (Cfapp$Const("cop "^id,dummyT)$(nth_elem (0,ts)))$
+ (nth_elem (1,ts))
+ end);
+
+
+
+(* -----------------------------------------------------------------------
+ make a print translation for a cont. infix operator "cop ???"
+ this is a print translation for fapp and is installed only once
+ special translations for other mixfixes (e.g. If_then_else_fi) are also
+ defined.
+ ----------------------------------------------------------------------- *)
+
+fun fapptr' ts =
+ case ts of
+ [Const("fapp",T1)$Const(s,T2)$t1,t2] =>
+ if ["c","o","p"," "] = take(4, explode s)
+ then Const(implode(drop(4, explode s)),dummyT)$t1$t2
+ else raise Match
+ | [Const("fapp",dummyT)$
+ (Const("fapp",T1)$Const("Icifte",T2)$t)$e1,e2]
+ => Const("@cifte",dummyT)$t$e1$e2
+ | _ => raise Match;
+
+
+(* -----------------------------------------------------------------------
+
+for the example above, the following must be setup in the ML section
+
+val parse_translation = [(".",mk_cinfixtr "."),
+ ("#",mk_cinfixtr "#")];
+
+
+the print translation for fapp is setup only once in the system
+
+val print_translation = [("fapp",fapptr')];
+
+ ----------------------------------------------------------------------- *)
+
+
+
+
+
+