change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
--- 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" *}
--- 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"
--- 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
--- 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;
--- 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
--- 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
--- 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"