adaptions
authorhaftmann
Fri Jan 05 14:31:44 2007 +0100 (2007-01-05)
changeset 2201512b94d7f7e1f
parent 22014 4b70cbd96007
child 22016 e086b4e846b8
adaptions
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Jan 05 14:30:08 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Jan 05 14:31:44 2007 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  begin
     1.5  
     1.6  ML {*
     1.7 -CodegenSerializer.sml_code_width := 74;
     1.8 +CodegenSerializer.code_width := 74;
     1.9  *}
    1.10  
    1.11  (*>*)
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Jan 05 14:30:08 2007 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Jan 05 14:31:44 2007 +0100
     2.3 @@ -1,18 +1,23 @@
     2.4 -module Codegen where
     2.5 -import qualified Nat
     2.6 +module Codegen where {
     2.7 +
     2.8 +import qualified Nat;
     2.9  
    2.10 -class Null a where
    2.11 -  nulla :: a
    2.12 +class Null a where {
    2.13 +  nulla :: a;
    2.14 +};
    2.15 +
    2.16 +heada :: (Codegen.Null a) => [a] -> a;
    2.17 +heada (y : xs) = y;
    2.18 +heada [] = Codegen.nulla;
    2.19  
    2.20 -heada :: (Codegen.Null a) => ([a] -> a)
    2.21 -heada (y : xs) = y
    2.22 -heada [] = Codegen.nulla
    2.23 +null_option :: Maybe b;
    2.24 +null_option = Nothing;
    2.25  
    2.26 -null_option :: Maybe b
    2.27 -null_option = Nothing
    2.28 +instance Codegen.Null (Maybe b) where {
    2.29 +  nulla = Codegen.null_option;
    2.30 +};
    2.31  
    2.32 -instance Codegen.Null (Maybe b) where
    2.33 -  null = Codegen.null_option
    2.34 +dummy :: Maybe Nat.Nat;
    2.35 +dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
    2.36  
    2.37 -dummy :: Maybe Nat.Nat
    2.38 -dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]
    2.39 +}
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Jan 05 14:30:08 2007 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Jan 05 14:31:44 2007 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4  struct
     3.5  
     3.6  fun in_interval (k, l) n =
     3.7 -  (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
     3.8 +  Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
     3.9  
    3.10  end; (*struct Codegen*)
    3.11  
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Jan 05 14:30:08 2007 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Jan 05 14:31:44 2007 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4  struct
     4.5  
     4.6  fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
     4.7 -  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
     4.8 +  Code_Generator.op_eq A_ x y orelse memberl A_ x ys
     4.9    | memberl (A_:'a Code_Generator.eq) x [] = false;
    4.10  
    4.11  end; (*struct List*)
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Jan 05 14:30:08 2007 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Jan 05 14:31:44 2007 +0100
     5.3 @@ -11,11 +11,11 @@
     5.4  structure Codegen = 
     5.5  struct
     5.6  
     5.7 -val dummy_set : (Nat.nat -> Nat.nat) list = (Nat.Suc :: []);
     5.8 +val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
     5.9  
    5.10  val foobar_set : Nat.nat list =
    5.11 -  (Nat.Zero_nat ::
    5.12 -    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: [])));
    5.13 +  Nat.Zero_nat ::
    5.14 +    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
    5.15  
    5.16  end; (*struct Codegen*)
    5.17  
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Fri Jan 05 14:30:08 2007 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Fri Jan 05 14:31:44 2007 +0100
     6.3 @@ -4,8 +4,8 @@
     6.4  structure Codegen = 
     6.5  struct
     6.6  
     6.7 -val double_inc : IntInf.int -> IntInf.int =
     6.8 -  (fn k => IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int)));
     6.9 +fun double_inc k =
    6.10 +  IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int));
    6.11  
    6.12  end; (*struct Codegen*)
    6.13  
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Jan 05 14:30:08 2007 +0100
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Jan 05 14:31:44 2007 +0100
     7.3 @@ -12,9 +12,9 @@
     7.4  structure Product_Type = 
     7.5  struct
     7.6  
     7.7 -fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
     7.8 -  (x2, y2) =
     7.9 -  (Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2);
    7.10 +fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq)
    7.11 +  (x1, y1) (x2, y2) =
    7.12 +  Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
    7.13  
    7.14  end; (*struct Product_Type*)
    7.15  
    7.16 @@ -36,15 +36,15 @@
    7.17      val (x1, y1) = p1;
    7.18      val (x2, y2) = p2;
    7.19    in
    7.20 -    (Orderings.less (#2 B_) x1 x2 orelse
    7.21 +    Orderings.less (#2 B_) x1 x2 orelse
    7.22        Code_Generator.op_eq (#1 B_) x1 x2 andalso
    7.23 -        Orderings.less (#2 C_) y1 y2)
    7.24 +        Orderings.less (#2 C_) y1 y2
    7.25    end;
    7.26  
    7.27  fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
    7.28    (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
    7.29 -  (less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
    7.30 -    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2);
    7.31 +  less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
    7.32 +    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
    7.33  
    7.34  end; (*struct Codegen*)
    7.35