# HG changeset patch
# User huffman
# Date 1288476791 25200
# Node ID 73f2b99b549d6e59da4b0a8f0f4720fa0f5ac48c
# Parent  ae8d187600e76630d8381c1ec841ecca8c107faf
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'

diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/HOLCF.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -11,7 +11,7 @@
   Powerdomains
 begin
 
-default_sort pcpo
+default_sort bifinite
 
 ML {* path_add "~~/src/HOLCF/Library" *}
 
diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -8,7 +8,9 @@
 imports HOLCF
 begin
 
-domain 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
+default_sort pcpo
+
+domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
 
 (*
    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/Library/Stream.thy
--- a/src/HOLCF/Library/Stream.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/Library/Stream.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -8,7 +8,9 @@
 imports HOLCF Nat_Infinity
 begin
 
-domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
+default_sort pcpo
+
+domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
 
 definition
   smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/Tools/Domain/domain.ML
--- a/src/HOLCF/Tools/Domain/domain.ML	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain.ML	Sat Oct 30 15:13:11 2010 -0700
@@ -221,6 +221,7 @@
 (** outer syntax **)
 
 val _ = Keyword.keyword "lazy";
+val _ = Keyword.keyword "unsafe";
 
 val dest_decl : (bool * binding option * string) parser =
   Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
@@ -237,11 +238,12 @@
     (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
 
 val domains_decl =
-  Parse.and_list1 domain_decl;
+  Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
+    Parse.and_list1 domain_decl;
 
 fun mk_domain
-    (definitional : bool)
-    (doms : ((((string * string option) list * binding) * mixfix) *
+    (unsafe : bool,
+     doms : ((((string * string option) list * binding) * mixfix) *
              ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
   let
     val specs : ((string * string option) list * binding * mixfix *
@@ -249,17 +251,13 @@
         map (fn (((vs, t), mx), cons) =>
                 (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
   in
-    if definitional
-    then add_new_domain_cmd specs
-    else add_domain_cmd specs
+    if unsafe
+    then add_domain_cmd specs
+    else add_new_domain_cmd specs
   end;
 
 val _ =
   Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
-    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
-
-val _ =
-  Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
-    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
+    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain));
 
 end;
diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/Tutorial/Domain_ex.thy
--- a/src/HOLCF/Tutorial/Domain_ex.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/Tutorial/Domain_ex.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -105,11 +105,13 @@
 
 text {* Lazy constructor arguments may have unpointed types. *}
 
-domain natlist = nnil | ncons (lazy "nat discr") natlist
+domain (unsafe) natlist = nnil | ncons (lazy "nat discr") natlist
 
 text {* Class constraints may be given for type parameters on the LHS. *}
 
-domain ('a::cpo) box = Box (lazy 'a)
+domain (unsafe) ('a::cpo) box = Box (lazy 'a)
+
+domain (unsafe) ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
 
 
 subsection {* Generated constants and theorems *}
@@ -196,11 +198,4 @@
   -- "Inner syntax error: unexpected end of input"
 *)
 
-text {*
-  Non-cpo type parameters currently do not work.
-*}
-(*
-domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
-*)
-
 end
diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/Tutorial/New_Domain.thy
--- a/src/HOLCF/Tutorial/New_Domain.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/Tutorial/New_Domain.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -9,8 +9,8 @@
 begin
 
 text {*
-  The definitional domain package only works with bifinite domains,
-  i.e. types in class @{text bifinite}.
+  UPDATE: The definitional back-end is now the default mode of the domain
+  package. This file should be merged with @{text Domain_ex.thy}.
 *}
 
 default_sort bifinite
@@ -21,7 +21,7 @@
   domain package.
 *}
 
-new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
 
 text {*
   The difference is that the new domain package is completely
@@ -38,7 +38,7 @@
   indirect recursion through the lazy list type constructor.
 *}
 
-new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
 
 text {*
   For indirect-recursive definitions, the domain package is not able to
diff -r ae8d187600e7 -r 73f2b99b549d src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -8,6 +8,8 @@
 imports HOLCF
 begin
 
+default_sort pcpo
+
 text {* FIXME: Find a proper way to un-hide constants. *}
 
 abbreviation fail :: "'a match"