change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
authorhuffman
Sat Oct 30 15:13:11 2010 -0700 (2010-10-30)
changeset 4032973f2b99b549d
parent 40328 ae8d187600e7
child 40330 3b7f570723f9
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
src/HOLCF/HOLCF.thy
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/Library/Stream.thy
src/HOLCF/Tools/Domain/domain.ML
src/HOLCF/Tutorial/Domain_ex.thy
src/HOLCF/Tutorial/New_Domain.thy
src/HOLCF/ex/Pattern_Match.thy
     1.1 --- a/src/HOLCF/HOLCF.thy	Sat Oct 30 12:25:18 2010 -0700
     1.2 +++ b/src/HOLCF/HOLCF.thy	Sat Oct 30 15:13:11 2010 -0700
     1.3 @@ -11,7 +11,7 @@
     1.4    Powerdomains
     1.5  begin
     1.6  
     1.7 -default_sort pcpo
     1.8 +default_sort bifinite
     1.9  
    1.10  ML {* path_add "~~/src/HOLCF/Library" *}
    1.11  
     2.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Sat Oct 30 12:25:18 2010 -0700
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Sat Oct 30 15:13:11 2010 -0700
     2.3 @@ -8,7 +8,9 @@
     2.4  imports HOLCF
     2.5  begin
     2.6  
     2.7 -domain 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
     2.8 +default_sort pcpo
     2.9 +
    2.10 +domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
    2.11  
    2.12  (*
    2.13     sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
     3.1 --- a/src/HOLCF/Library/Stream.thy	Sat Oct 30 12:25:18 2010 -0700
     3.2 +++ b/src/HOLCF/Library/Stream.thy	Sat Oct 30 15:13:11 2010 -0700
     3.3 @@ -8,7 +8,9 @@
     3.4  imports HOLCF Nat_Infinity
     3.5  begin
     3.6  
     3.7 -domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
     3.8 +default_sort pcpo
     3.9 +
    3.10 +domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
    3.11  
    3.12  definition
    3.13    smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
     4.1 --- a/src/HOLCF/Tools/Domain/domain.ML	Sat Oct 30 12:25:18 2010 -0700
     4.2 +++ b/src/HOLCF/Tools/Domain/domain.ML	Sat Oct 30 15:13:11 2010 -0700
     4.3 @@ -221,6 +221,7 @@
     4.4  (** outer syntax **)
     4.5  
     4.6  val _ = Keyword.keyword "lazy";
     4.7 +val _ = Keyword.keyword "unsafe";
     4.8  
     4.9  val dest_decl : (bool * binding option * string) parser =
    4.10    Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
    4.11 @@ -237,11 +238,12 @@
    4.12      (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
    4.13  
    4.14  val domains_decl =
    4.15 -  Parse.and_list1 domain_decl;
    4.16 +  Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
    4.17 +    Parse.and_list1 domain_decl;
    4.18  
    4.19  fun mk_domain
    4.20 -    (definitional : bool)
    4.21 -    (doms : ((((string * string option) list * binding) * mixfix) *
    4.22 +    (unsafe : bool,
    4.23 +     doms : ((((string * string option) list * binding) * mixfix) *
    4.24               ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
    4.25    let
    4.26      val specs : ((string * string option) list * binding * mixfix *
    4.27 @@ -249,17 +251,13 @@
    4.28          map (fn (((vs, t), mx), cons) =>
    4.29                  (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
    4.30    in
    4.31 -    if definitional
    4.32 -    then add_new_domain_cmd specs
    4.33 -    else add_domain_cmd specs
    4.34 +    if unsafe
    4.35 +    then add_domain_cmd specs
    4.36 +    else add_new_domain_cmd specs
    4.37    end;
    4.38  
    4.39  val _ =
    4.40    Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
    4.41 -    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
    4.42 -
    4.43 -val _ =
    4.44 -  Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
    4.45 -    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
    4.46 +    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain));
    4.47  
    4.48  end;
     5.1 --- a/src/HOLCF/Tutorial/Domain_ex.thy	Sat Oct 30 12:25:18 2010 -0700
     5.2 +++ b/src/HOLCF/Tutorial/Domain_ex.thy	Sat Oct 30 15:13:11 2010 -0700
     5.3 @@ -105,11 +105,13 @@
     5.4  
     5.5  text {* Lazy constructor arguments may have unpointed types. *}
     5.6  
     5.7 -domain natlist = nnil | ncons (lazy "nat discr") natlist
     5.8 +domain (unsafe) natlist = nnil | ncons (lazy "nat discr") natlist
     5.9  
    5.10  text {* Class constraints may be given for type parameters on the LHS. *}
    5.11  
    5.12 -domain ('a::cpo) box = Box (lazy 'a)
    5.13 +domain (unsafe) ('a::cpo) box = Box (lazy 'a)
    5.14 +
    5.15 +domain (unsafe) ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
    5.16  
    5.17  
    5.18  subsection {* Generated constants and theorems *}
    5.19 @@ -196,11 +198,4 @@
    5.20    -- "Inner syntax error: unexpected end of input"
    5.21  *)
    5.22  
    5.23 -text {*
    5.24 -  Non-cpo type parameters currently do not work.
    5.25 -*}
    5.26 -(*
    5.27 -domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
    5.28 -*)
    5.29 -
    5.30  end
     6.1 --- a/src/HOLCF/Tutorial/New_Domain.thy	Sat Oct 30 12:25:18 2010 -0700
     6.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Sat Oct 30 15:13:11 2010 -0700
     6.3 @@ -9,8 +9,8 @@
     6.4  begin
     6.5  
     6.6  text {*
     6.7 -  The definitional domain package only works with bifinite domains,
     6.8 -  i.e. types in class @{text bifinite}.
     6.9 +  UPDATE: The definitional back-end is now the default mode of the domain
    6.10 +  package. This file should be merged with @{text Domain_ex.thy}.
    6.11  *}
    6.12  
    6.13  default_sort bifinite
    6.14 @@ -21,7 +21,7 @@
    6.15    domain package.
    6.16  *}
    6.17  
    6.18 -new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    6.19 +domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    6.20  
    6.21  text {*
    6.22    The difference is that the new domain package is completely
    6.23 @@ -38,7 +38,7 @@
    6.24    indirect recursion through the lazy list type constructor.
    6.25  *}
    6.26  
    6.27 -new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    6.28 +domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    6.29  
    6.30  text {*
    6.31    For indirect-recursive definitions, the domain package is not able to
     7.1 --- a/src/HOLCF/ex/Pattern_Match.thy	Sat Oct 30 12:25:18 2010 -0700
     7.2 +++ b/src/HOLCF/ex/Pattern_Match.thy	Sat Oct 30 15:13:11 2010 -0700
     7.3 @@ -8,6 +8,8 @@
     7.4  imports HOLCF
     7.5  begin
     7.6  
     7.7 +default_sort pcpo
     7.8 +
     7.9  text {* FIXME: Find a proper way to un-hide constants. *}
    7.10  
    7.11  abbreviation fail :: "'a match"