src/HOLCF/Tools/domain/domain_syntax.ML

     Author:     David von Oheimb
 
 Syntax generator for domain command.
 *)
 
-structure Domain_Syntax = struct 
+signature DOMAIN_SYNTAX =
+sig
+  val add_syntax: string -> ((string * typ list) *
+	(binding * (bool * binding option * typ) list * mixfix) list) list
+    -> theory -> theory
+end;
+
+
+structure Domain_Syntax : DOMAIN_SYNTAX =
+struct 
 
 local 
 
 open Domain_Library;
 infixr 5 -->; infixr 6 ->>;
 fun calc_syntax dtypeprod ((dname, typevars), 
-	(cons': (string * mixfix * (bool * string option * typ) list) list)) =
+	(cons': (binding * (bool * binding option * typ) list * mixfix) list)) : ((binding * typ * mixfix) list * ast Syntax.trrule list) =
 let
 (* ----- constants concerning the isomorphism ------------------------------- *)
 
 local
   fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
-  fun prod     (_,_,args) = if args = [] then oneT
-			    else foldr1 mk_sprodT (map opt_lazy args);
+  fun prod     (_,args,_) = case args of [] => oneT
+                            | _ => foldr1 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) = List.foldr (op ->>) (freetvar "t") (map third args);
+  fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
 in
   val dtype  = Type(dname,typevars);
   val dtype2 = foldr1 mk_ssumT (map prod cons');
   val dnam = Long_Name.base_name dname;
-  val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
-  val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
-  val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
-  val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
+  fun dbind s = Binding.name (dnam ^ s);
+  val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
+  val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
+  val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+  val const_copy = (dbind "_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
 end;
 
 (* ----- 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 []      = []
 	in implode o esc o Symbol.explode end;
-  fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
-  fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
-			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
+  fun dis_name_ con     = Binding.name ("is_" ^ strip_esc (Binding.name_of con));
+  fun mat_name_ con     = Binding.name ("match_" ^ strip_esc (Binding.name_of con));
+  fun pat_name_ con     = Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
+  fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx);
+  fun dis (con,args,mx) = (dis_name_ con, dtype->>trT,
+			   Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri));
 			(* strictly speaking, these constants have one argument,
 			   but the mixfix (without arguments) is introduced only
 			   to generate parse rules for non-alphanumeric names*)
   fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
 			  if tvar mem typevars then freetvar ("t"^s) n else tvar end;
   fun mk_matT (a,bs,c)  = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
-  fun mat (con,s,args)  = (mat_name_ con,
+  fun mat (con,args,mx) = (mat_name_ con,
                            mk_matT(dtype, map third args, freetvar "t" 1),
-			   Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
+			   Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
   fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
-  fun sel (_   ,_,args) = List.mapPartial sel1 args;
+  fun sel (con,args,mx) = List.mapPartial sel1 args;
   fun mk_patT (a,b)     = a ->> mk_maybeT b;
   fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
-  fun pat (con ,s,args) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
+  fun pat (con,args,mx) = (pat_name_ con, (mapn pat_arg_typ 1 args) --->
 			   mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
-			   Mixfix(escape (con ^ "_pat"), [], Syntax.max_pri));
+			   Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
 
 in
   val consts_con = map con cons';
   val consts_dis = map dis cons';
   val consts_mat = map mat cons';

   val consts_sel = List.concat(map sel cons');
 end;
 
 (* ----- constants concerning induction ------------------------------------- *)
 
-  val const_take   = (dnam^"_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
-  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT       , NoSyn);
+  val const_take   = (dbind "_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
+  val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
 
 (* ----- case translation --------------------------------------------------- *)
 
 local open Syntax in
   local
-    fun c_ast con mx = Constant (Syntax.const_name mx con);
+    fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con));
     fun expvar n     = Variable ("e"^(string_of_int n));
     fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
 				     (string_of_int m));
     fun argvars n args = mapn (argvar n) 1 args;
     fun app s (l,r)  = mk_appl (Constant s) [l,r];
     val cabs = app "_cabs";
     val capp = app "Rep_CFun";
-    fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
-    fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
-    fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
+    fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args);
+    fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n);
+    fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
     fun when1 n m = if n = m then arg1 n else K (Constant "UU");
 
     fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
     fun app_pat x = mk_appl (Constant "_pat") [x];
     fun args_list [] = Constant "_noargs"

     
     val abscon_trans = mapn (fn n => fn (con,mx,args) => ParsePrintRule
         (cabs (con1 n (con,mx,args), expvar n),
          Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons'))) 1 cons';
     
-    val Case_trans = List.concat (map (fn (con,mx,args) =>
+    val Case_trans = List.concat (map (fn (con,args,mx) =>
       let
         val cname = c_ast con mx;
-        val pname = Constant (pat_name_ con);
+        val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat");
         val ns = 1 upto length args;
         val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
         val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
         val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
       in

 
 (* ----- putting all the syntax stuff together ------------------------------ *)
 
 in (* local *)
 
-fun add_syntax (comp_dnam,eqs': ((string * typ list) *
-	(string * mixfix * (bool * string option * typ) list) list) list) thy'' =
+fun add_syntax
+  (comp_dnam : string)
+  (eqs' : ((string * typ list) *
+	(binding * (bool * binding option * typ) list * mixfix) list) list)
+  (thy'' : theory) =
 let
   val dtypes  = map (Type o fst) eqs';
   val boolT   = HOLogic.boolT;
   val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
   val relprod = foldr1 HOLogic.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 const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
+  val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
+  val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
 in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ 
 				    (if length eqs'>1 then [const_copy] else[])@
 				    [const_bisim])
 	 |> Sign.add_trrules_i (List.concat(map snd ctt))
 end; (* let *)