# HG changeset patch
# User huffman
# Date 1268522305 28800
# Node ID 218e9766a848b497c40c7dab5049504b9d03c0af
# Parent  cae4f840d15d5b3d1a7cc91d44f59f0c942d49f9
replace some string arguments with bindings

diff -r cae4f840d15d -r 218e9766a848 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Sat Mar 13 14:30:38 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Sat Mar 13 15:18:25 2010 -0800
@@ -7,25 +7,25 @@
 signature DOMAIN_EXTENDER =
 sig
   val add_domain_cmd:
-      string ->
+      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * string) list * mixfix) list) list
       -> theory -> theory
 
   val add_domain:
-      string ->
+      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
 
   val add_new_domain_cmd:
-      string ->
+      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * string) list * mixfix) list) list
       -> theory -> theory
 
   val add_new_domain:
-      string ->
+      binding ->
       ((string * string option) list * binding * mixfix *
        (binding * (bool * binding option * typ) list * mixfix) list) list
       -> theory -> theory
@@ -126,7 +126,7 @@
 
 fun gen_add_domain
     (prep_typ : theory -> 'a -> typ)
-    (comp_dnam : string)
+    (comp_dbind : binding)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
     (thy : theory) =
@@ -192,19 +192,18 @@
           |> fold_map (fn ((eq, (x,cs)), info) =>
                 Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
              (eqs ~~ eqs' ~~ iso_infos)
-          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
+          ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
   in
     theorems_thy
-      |> Sign.add_path (Long_Name.base_name comp_dnam)
       |> PureThy.add_thmss
-           [((Binding.name "rews", flat rewss @ take_rews), [])]
+           [((Binding.qualified true "rews" comp_dbind,
+              flat rewss @ take_rews), [])]
       |> snd
-      |> Sign.parent_path
   end;
 
 fun gen_add_new_domain
     (prep_typ : theory -> 'a -> typ)
-    (comp_dnam : string)
+    (comp_dbind : binding)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
     (thy : theory) =
@@ -268,14 +267,13 @@
           |> fold_map (fn ((eq, (x,cs)), info) =>
                Domain_Theorems.theorems (eq, eqs) (Type x, cs) info)
              (eqs ~~ eqs' ~~ iso_infos)
-          ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs) take_info;
+          ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
   in
     theorems_thy
-      |> Sign.add_path (Long_Name.base_name comp_dnam)
       |> PureThy.add_thmss
-           [((Binding.name "rews", flat rewss @ take_rews), [])]
+           [((Binding.qualified true "rews" comp_dbind,
+              flat rewss @ take_rews), [])]
       |> snd
-      |> Sign.parent_path
   end;
 
 val add_domain = gen_add_domain Sign.certify_typ;
@@ -314,12 +312,12 @@
     (P.$$$ "=" |-- P.enum1 "|" cons_decl);
 
 val domains_decl =
-  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+  Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
     P.and_list1 domain_decl;
 
 fun mk_domain
     (definitional : bool)
-    (opt_name : string option,
+    (opt_name : binding option,
      doms : ((((string * string option) list * binding) * mixfix) *
              ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
   let
@@ -328,12 +326,13 @@
                  (binding * (bool * binding option * string) list * mixfix) list) list =
         map (fn (((vs, t), mx), cons) =>
                 (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
-    val comp_dnam =
-        case opt_name of NONE => space_implode "_" names | SOME s => s;
+    val comp_dbind =
+        case opt_name of NONE => Binding.name (space_implode "_" names)
+                       | SOME s => s;
   in
     if definitional 
-    then add_new_domain_cmd comp_dnam specs
-    else add_domain_cmd comp_dnam specs
+    then add_new_domain_cmd comp_dbind specs
+    else add_domain_cmd comp_dbind specs
   end;
 
 val _ =
diff -r cae4f840d15d -r 218e9766a848 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 14:30:38 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 13 15:18:25 2010 -0800
@@ -16,7 +16,7 @@
     -> theory -> thm list * theory;
 
   val comp_theorems :
-      bstring * Domain_Library.eq list ->
+      binding * Domain_Library.eq list ->
       Domain_Take_Proofs.take_induct_info ->
       theory -> thm list * theory
 
@@ -207,11 +207,12 @@
 (******************************************************************************)
 
 fun prove_induction
-    (comp_dnam, eqs : eq list)
+    (comp_dbind : binding, eqs : eq list)
     (take_rews : thm list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (thy : theory) =
 let
+  val comp_dname = Sign.full_name thy comp_dbind;
   val dnames = map (fst o fst) eqs;
   val conss  = map  snd        eqs;
   fun dc_take dn = %%:(dn^"_take");
@@ -286,7 +287,7 @@
     val is_emptys = map warn n__eqs;
     val is_finite = #is_finite take_info;
     val _ = if is_finite
-            then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
+            then message ("Proving finiteness rule for domain "^comp_dname^" ...")
             else ();
   end;
   val _ = trace " Proving finite_ind...";
@@ -400,12 +401,12 @@
     ((Binding.empty, [rule]),
      [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
 
-in thy |> Sign.add_path comp_dnam
-       |> snd o PureThy.add_thmss [
-           ((Binding.name "finite_ind" , [finite_ind]), []),
-           ((Binding.name "ind"        , [ind]       ), [])]
-       |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
-       |> Sign.parent_path
+in
+  thy
+  |> snd o PureThy.add_thmss [
+     ((Binding.qualified true "finite_ind" comp_dbind, [finite_ind]), []),
+     ((Binding.qualified true "ind"        comp_dbind, [ind]       ), [])]
+  |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
 end; (* prove_induction *)
 
 (******************************************************************************)
@@ -413,13 +414,13 @@
 (******************************************************************************)
 
 fun prove_coinduction
-    (comp_dnam, eqs : eq list)
+    (comp_dbind : binding, eqs : eq list)
     (take_lemmas : thm list)
     (thy : theory) : theory =
 let
 
 val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
+val comp_dname = Sign.full_name thy comp_dbind;
 fun dc_take dn = %%:(dn^"_take");
 val x_name = idx_name dnames "x"; 
 val n_eqs = length eqs;
@@ -433,7 +434,7 @@
   open HOLCF_Library
   val dtypes  = map (Type o fst) eqs;
   val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes);
-  val bisim_bind = Binding.name (comp_dnam ^ "_bisim");
+  val bisim_bind = Binding.suffix_name "_bisim" comp_dbind;
   val bisim_type = relprod --> boolT;
 in
   val (bisim_const, thy) =
@@ -449,10 +450,6 @@
   fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
   fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
 
-  val comp_dname = Sign.full_bname thy comp_dnam;
-  val dnames = map (fst o fst) eqs;
-  val x_name = idx_name dnames "x"; 
-
   fun one_con (con, args) =
     let
       val nonrec_args = filter_out is_rec args;
@@ -494,11 +491,9 @@
          mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs));
 
 in
-  val ([ax_bisim_def], thy) =
-      thy
-        |> Sign.add_path comp_dnam
-        |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)]
-        ||> Sign.parent_path;
+  val (ax_bisim_def, thy) =
+      yield_singleton add_defs_infer
+        (Binding.qualified true "bisim_def" comp_dbind, bisim_eqn) thy;
 end; (* local *)
 
 (* ----- theorem concerning coinduction ------------------------------------- *)
@@ -555,20 +550,19 @@
     in pg [] goal (K tacs) end;
 end; (* local *)
 
-in thy |> Sign.add_path comp_dnam
-       |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
-       |> Sign.parent_path
+in thy |> snd o PureThy.add_thmss
+                  [((Binding.qualified true "coind" comp_dbind, [coind]), [])]
 end; (* let *)
 
 fun comp_theorems
-    (comp_dnam : string, eqs : eq list)
+    (comp_dbind : binding, eqs : eq list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (thy : theory) =
 let
 val map_tab = Domain_Take_Proofs.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
-val comp_dname = Sign.full_bname thy comp_dnam;
+val comp_dname = Sign.full_name thy comp_dbind;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
 
@@ -596,11 +590,11 @@
 (* prove induction rules, unless definition is indirect recursive *)
 val thy =
     if is_indirect then thy else
-    prove_induction (comp_dnam, eqs) take_rews take_info thy;
+    prove_induction (comp_dbind, eqs) take_rews take_info thy;
 
 val thy =
     if is_indirect then thy else
-    prove_coinduction (comp_dnam, eqs) take_lemmas thy;
+    prove_coinduction (comp_dbind, eqs) take_lemmas thy;
 
 in
   (take_rews, thy)