src/HOLCF/cinfix.ML
changeset 13897 f62f9a75f685
parent 13896 717bd79b976f
child 13898 9410d2eb9563
--- a/src/HOLCF/cinfix.ML	Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(*  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')];
-
-  ----------------------------------------------------------------------- *) 
-
-
-
-
-
-