src/HOLCF/cinfix.ML

New comments on how to deal with unproved termination conditions

(*  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')];

  ----------------------------------------------------------------------- *)