src/HOLCF/domain/syntax.ML

 structure Domain_Syntax = struct 
 
 local 
 
 open Domain_Library;
-infixr 5 -->; infixr 6 ~>;
-fun calc_syntax dtypeprod ((dname, typevars), (cons':
-			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
+infixr 5 -->; infixr 6 ->>;
+fun calc_syntax dtypeprod ((dname, typevars), 
+	(cons': (string * mixfix * (bool*string*typ) list) list)) =
 let
-(* ----- constants concerning the isomorphism ------------------------------------- *)
+(* ----- constants concerning the isomorphism ------------------------------- *)
 
 local
-  fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
-  fun prod     (_,_,args) = if args = [] then Type("one",[])
-				         else foldr'(mk_typ "**") (map opt_lazy args);
-  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
-  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
+  fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
+  fun prod     (_,_,args) = if args = [] then oneT
+			    else foldr' mk_sprodT (map opt_lazy args);
+  fun freetvar s = let val tvar = mk_TFree s in
+		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
+  fun when_type (_   ,_,args) = foldr (op ->>) (map third args,freetvar "t");
 in
   val dtype  = Type(dname,typevars);
-  val dtype2 = foldr' (mk_typ "++") (map prod cons');
+  val dtype2 = foldr' mk_ssumT (map prod cons');
   val dnam = Sign.base_name dname;
-  val const_rep  = (dnam^"_rep" ,              dtype  ~> dtype2, NoSyn');
-  val const_abs  = (dnam^"_abs" ,              dtype2 ~> dtype , NoSyn');
-  val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
-					       	 dtype ~> freetvar "t"), NoSyn');
-  val const_copy = (dnam^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
+  val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
+  val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
+  val const_when = (dnam^"_when",foldr (op ->>) ((map when_type cons'),
+					        dtype ->> freetvar "t"), NoSyn);
+  val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
 end;
 
-(* ----- constants concerning the constructors, discriminators and selectors ------ *)
-
-fun is_infix (ThyOps.CInfixl       _ ) = true
-|   is_infix (ThyOps.CInfixr       _ ) = true
-|   is_infix (ThyOps.Mixfix(Infixl _)) = true
-|   is_infix (ThyOps.Mixfix(Infixr _)) = true
-|   is_infix  _                        = false;
+(* ----- constants concerning constructors, discriminators, and selectors --- *)
 
 local
   val escape = let
-	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
-							   else        c :: esc cs
-	|   esc []        = []
+	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
+							 else      c::esc cs
+	|   esc []      = []
 	in implode o esc o explode end;
-  fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
-  fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
-			 	 ThyOps.Mixfix(Mixfix("is'_"^
-				 (if is_infix s then Id else escape)con,[],max_pri)));
-  fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
+  fun con (name,s,args) = (name,foldr (op ->>) (map third args,dtype),s);
+  fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
+			   Mixfix(escape ("is_" ^ con), [], max_pri));
+			(* stricly speaking, these constants have one argument,
+			   but the mixfix (without arguments) is introduced only
+			   to generate parse rules for non-alphanumeric names*)
+  fun sel (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
 in
   val consts_con = map con cons';
   val consts_dis = map dis cons';
   val consts_sel = flat(map sel cons');
 end;
 
-(* ----- constants concerning induction ------------------------------------------- *)
+(* ----- constants concerning induction ------------------------------------- *)
 
-  val const_take   = (dnam^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
-  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
+  val const_take   = (dnam^"_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
+  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT       , NoSyn);
 
-(* ----- case translation --------------------------------------------------------- *)
+(* ----- case translation --------------------------------------------------- *)
 
 local open Syntax in
   val case_trans = let 
-	fun c_ast con syn = Constant (ThyOps.const_name con syn);
-	fun expvar n      = Variable ("e"^(string_of_int n));
-	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
+	fun c_ast con mx = Constant (const_name con mx);
+	fun expvar n     = Variable ("e"^(string_of_int n));
+	fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
+					 (string_of_int m));
 	fun app s (l,r)   = mk_appl (Constant s) [l,r];
-	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
-		 [if is_infix syn
-		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
-		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
+	fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
+		 [foldl (app "fapp") (c_ast con mx, (mapn (argvar n) 1 args)),
 		  expvar n];
 	fun arg1 n (con,_,args) = if args = [] then expvar n 
 				  else mk_appl (Constant "LAM ") 
 		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
   in
     ParsePrintRule
       (mk_appl (Constant "@case") [Variable "x", foldr'
-				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
+				(fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
 				 (mapn case1 1 cons')],
-       mk_appl (Constant "@fapp") [foldl 
-				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
+       mk_appl (Constant "fapp") [foldl 
+				(fn (w,a ) => mk_appl (Constant"fapp" ) [w,a ])
 				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
 				 Variable "x"])
   end;
 end;
 

      consts_con @ consts_dis @ consts_sel @
     [const_take, const_finite],
     [case_trans])
 end; (* let *)
 
-(* ----- putting all the syntax stuff together ------------------------------------ *)
+(* ----- putting all the syntax stuff together ------------------------------ *)
 
 in (* local *)
 
 fun add_syntax (comp_dnam,eqs': ((string * typ list) *
-		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
+	(string * mixfix * (bool*string*typ) list) list) list) thy'' =
 let
-  val dtypes  = map (Type      o fst) eqs';
-  val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
-  val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
-  val const_copy   = (comp_dnam^"_copy"  ,funprod ~> funprod       , NoSyn');
-  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
+  val dtypes  = map (Type o fst) eqs';
+  val boolT   = HOLogic.boolT;
+  val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
+  val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+  val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
+  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
   val ctt           = map (calc_syntax funprod) eqs';
-  val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
-in thy'' |> add_cur_ops_i (flat(map fst ctt))
-	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
+in thy'' |> ContConsts.add_consts_i (flat (map fst ctt) @ 
+				    (if length eqs'>1 then [const_copy] else[])@
+				    [const_bisim])
 	 |> Theory.add_trrules_i (flat(map snd ctt))
 end; (* let *)
 
 end; (* local *)
 end; (* struct *)