--- a/doc-src/Codegen/Thy/examples/Codegen.hs Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-module Codegen where {
-
-import qualified Nat;
-
-class Null a where {
- nulla :: a;
-};
-
-heada :: forall a. (Codegen.Null a) => [a] -> a;
-heada (x : xs) = x;
-heada [] = Codegen.nulla;
-
-null_option :: forall a. Maybe a;
-null_option = Nothing;
-
-instance Codegen.Null (Maybe a) where {
- nulla = Codegen.null_option;
-};
-
-dummy :: Maybe Nat.Nat;
-dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
-
-}
--- a/doc-src/Codegen/Thy/examples/arbitrary.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-structure Codegen =
-struct
-
-val arbitrary_option : 'a option = NONE;
-
-fun dummy_option [] = arbitrary_option
- | dummy_option (x :: xs) = SOME x;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/bool_infix.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun less_nat m (Suc n) = less_eq_nat m n
- | less_nat n Zero_nat = false
-and less_eq_nat (Suc m) n = less_nat m n
- | less_eq_nat Zero_nat n = true;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-fun in_interval (k, l) n =
- Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/bool_literal.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-structure HOL =
-struct
-
-datatype boola = False | True;
-
-fun anda x True = x
- | anda x False = False
- | anda True x = x
- | anda False x = False;
-
-end; (*struct HOL*)
-
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun less_nat m (Suc n) = less_eq_nat m n
- | less_nat n Zero_nat = HOL.False
-and less_eq_nat (Suc m) n = less_nat m n
- | less_eq_nat Zero_nat n = HOL.True;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-fun in_interval (k, l) n =
- HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/bool_mlbool.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun less_nat m (Suc n) = less_eq_nat m n
- | less_nat n Zero_nat = false
-and less_eq_nat (Suc m) n = less_nat m n
- | less_eq_nat Zero_nat n = true;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-fun in_interval (k, l) n =
- (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/class.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-type 'a null = {null : 'a};
-fun null (A_:'a null) = #null A_;
-
-fun head A_ (x :: xs) = x
- | head A_ [] = null A_;
-
-val null_option : 'a option = NONE;
-
-fun null_optiona () = {null = null_option} : ('a option) null;
-
-val dummy : Nat.nat option =
- head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/class.ocaml Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-module Nat =
-struct
-
-type nat = Suc of nat | Zero_nat;;
-
-end;; (*struct Nat*)
-
-module Codegen =
-struct
-
-type 'a null = {null : 'a};;
-let null _A = _A.null;;
-
-let rec head _A = function x :: xs -> x
- | [] -> null _A;;
-
-let rec null_option = None;;
-
-let null_optiona () = ({null = null_option} : ('a option) null);;
-
-let rec dummy
- = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
-
-end;; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/collect_duplicates.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-structure HOL =
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-fun eqop A_ a = eq A_ a;
-
-end; (*struct HOL*)
-
-structure List =
-struct
-
-fun member A_ x (y :: ys) =
- (if HOL.eqop A_ y x then true else member A_ x ys)
- | member A_ x [] = false;
-
-end; (*struct List*)
-
-structure Codegen =
-struct
-
-fun collect_duplicates A_ xs ys (z :: zs) =
- (if List.member A_ z xs
- then (if List.member A_ z ys then collect_duplicates A_ xs ys zs
- else collect_duplicates A_ xs (z :: ys) zs)
- else collect_duplicates A_ (z :: xs) (z :: ys) zs)
- | collect_duplicates A_ xs ys [] = xs;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/dirty_set.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-structure ROOT =
-struct
-
-structure Nat =
-struct
-
-datatype nat = Zero_nat | Suc of nat;
-
-end; (*struct Nat*)
-
-structure Integer =
-struct
-
-datatype bit = B0 | B1;
-
-datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
-
-fun pred (Bit (k, B0)) = Bit (pred k, B1)
- | pred (Bit (k, B1)) = Bit (k, B0)
- | pred Min = Bit (Min, B0)
- | pred Pls = Min;
-
-fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
- | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
- | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
- | uminus_int Min = Bit (Pls, B1)
- | uminus_int Pls = Pls;
-
-fun succ (Bit (k, B0)) = Bit (k, B1)
- | succ (Bit (k, B1)) = Bit (succ k, B0)
- | succ Min = Pls
- | succ Pls = Bit (Pls, B1);
-
-fun plus_int (Number_of_int v) (Number_of_int w) =
- Number_of_int (plus_int v w)
- | plus_int k Min = pred k
- | plus_int k Pls = k
- | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
- | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
- | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
- | plus_int Min k = pred k
- | plus_int Pls k = k;
-
-fun minus_int (Number_of_int v) (Number_of_int w) =
- Number_of_int (plus_int v (uminus_int w))
- | minus_int z w = plus_int z (uminus_int w);
-
-fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l
- | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2
- | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2
- | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2
- | less_eq_int (Bit (k, v)) Min = less_eq_int k Min
- | less_eq_int (Bit (k, B1)) Pls = less_int k Pls
- | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls
- | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k
- | less_eq_int Min (Bit (k, B0)) = less_int Min k
- | less_eq_int Min Min = true
- | less_eq_int Min Pls = true
- | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k
- | less_eq_int Pls Min = false
- | less_eq_int Pls Pls = true
-and less_int (Number_of_int k) (Number_of_int l) = less_int k l
- | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2
- | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2
- | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2
- | less_int (Bit (k, B1)) Min = less_int k Min
- | less_int (Bit (k, B0)) Min = less_eq_int k Min
- | less_int (Bit (k, v)) Pls = less_int k Pls
- | less_int Min (Bit (k, v)) = less_int Min k
- | less_int Min Min = false
- | less_int Min Pls = true
- | less_int Pls (Bit (k, B1)) = less_eq_int Pls k
- | less_int Pls (Bit (k, B0)) = less_int Pls k
- | less_int Pls Min = false
- | less_int Pls Pls = false;
-
-fun nat_aux n i =
- (if less_eq_int i (Number_of_int Pls) then n
- else nat_aux (Nat.Suc n)
- (minus_int i (Number_of_int (Bit (Pls, B1)))));
-
-fun nat i = nat_aux Nat.Zero_nat i;
-
-end; (*struct Integer*)
-
-structure Codegen =
-struct
-
-val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
-
-val foobar_set : Nat.nat list =
- Nat.Zero_nat ::
- (Nat.Suc Nat.Zero_nat ::
- (Integer.nat
- (Integer.Number_of_int
- (Integer.Bit
- (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
- :: []));
-
-end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/Codegen/Thy/examples/fac.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-val one_nat : nat = Suc Zero_nat;
-
-fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat Zero_nat n = n;
-
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
- | times_nat Zero_nat n = Zero_nat;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
- | fac Nat.Zero_nat = Nat.one_nat;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/integers.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-structure ROOT =
-struct
-
-structure Integer =
-struct
-
-datatype bit = B0 | B1;
-
-datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
-
-fun pred (Bit (k, B0)) = Bit (pred k, B1)
- | pred (Bit (k, B1)) = Bit (k, B0)
- | pred Min = Bit (Min, B0)
- | pred Pls = Min;
-
-fun succ (Bit (k, B0)) = Bit (k, B1)
- | succ (Bit (k, B1)) = Bit (succ k, B0)
- | succ Min = Pls
- | succ Pls = Bit (Pls, B1);
-
-fun plus_int (Number_of_int v) (Number_of_int w) =
- Number_of_int (plus_int v w)
- | plus_int k Min = pred k
- | plus_int k Pls = k
- | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
- | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
- | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
- | plus_int Min k = pred k
- | plus_int Pls k = k;
-
-fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
- | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
- | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
- | uminus_int Min = Bit (Pls, B1)
- | uminus_int Pls = Pls;
-
-fun times_int (Number_of_int v) (Number_of_int w) =
- Number_of_int (times_int v w)
- | times_int (Bit (k, B0)) l = Bit (times_int k l, B0)
- | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l
- | times_int Min k = uminus_int k
- | times_int Pls w = Pls;
-
-end; (*struct Integer*)
-
-structure Codegen =
-struct
-
-fun double_inc k =
- Integer.plus_int
- (Integer.times_int
- (Integer.Number_of_int
- (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
- k)
- (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1)));
-
-end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/Codegen/Thy/examples/lexicographic.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-structure HOL =
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
-fun less_eq (A_:'a ord) = #less_eq A_;
-fun less (A_:'a ord) = #less A_;
-
-end; (*struct HOL*)
-
-structure Codegen =
-struct
-
-fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) =
- HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/lookup.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-structure ROOT =
-struct
-
-structure Codegen =
-struct
-
-fun lookup ((k, v) :: xs) l =
- (if ((k : string) = l) then SOME v else lookup xs l)
- | lookup [] l = NONE;
-
-end; (*struct Codegen*)
-
-end; (*struct ROOT*)
--- a/doc-src/Codegen/Thy/examples/monotype.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun eq_nat (Suc a) Zero_nat = false
- | eq_nat Zero_nat (Suc a) = false
- | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
- | eq_nat Zero_nat Zero_nat = true;
-
-end; (*struct Nat*)
-
-structure List =
-struct
-
-fun null (x :: xs) = false
- | null [] = true;
-
-fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
- | list_all2 p xs [] = null xs
- | list_all2 p [] ys = null ys;
-
-end; (*struct List*)
-
-structure Codegen =
-struct
-
-datatype monotype = Mono of Nat.nat * monotype list;
-
-fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
- Nat.eq_nat tyco1 tyco2 andalso
- List.list_all2 eq_monotype typargs1 typargs2;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/nat_binary.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-structure Nat =
-struct
-
-datatype nat = Dig1 of nat | Dig0 of nat | One_nat | Zero_nat;
-
-fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)
- | plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)
- | plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)
- | plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)
- | plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)
- | plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)
- | plus_nat (Dig0 m) One_nat = Dig1 m
- | plus_nat One_nat (Dig0 n) = Dig1 n
- | plus_nat m Zero_nat = m
- | plus_nat Zero_nat n = n;
-
-end; (*struct Nat*)
--- a/doc-src/Codegen/Thy/examples/pick1.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-structure HOL =
-struct
-
-fun leta s f = f s;
-
-end; (*struct HOL*)
-
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun less_nat m (Suc n) = less_eq_nat m n
- | less_nat n Zero_nat = false
-and less_eq_nat (Suc m) n = less_nat m n
- | less_eq_nat Zero_nat n = true;
-
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
- | minus_nat Zero_nat n = Zero_nat
- | minus_nat m Zero_nat = m;
-
-end; (*struct Nat*)
-
-structure Product_Type =
-struct
-
-fun split f (a, b) = f a b;
-
-end; (*struct Product_Type*)
-
-structure Codegen =
-struct
-
-fun pick ((k, v) :: xs) n =
- (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
- | pick (x :: xs) n =
- let
- val a = x;
- val (k, v) = a;
- in
- (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
- end;
-
-end; (*struct Codegen*)
--- a/doc-src/Codegen/Thy/examples/tree.ML Tue Jul 17 22:34:29 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-structure HOL =
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
-fun less_eq (A_:'a ord) = #less_eq A_;
-fun less (A_:'a ord) = #less A_;
-
-fun eqop A_ a = eq A_ a;
-
-end; (*struct HOL*)
-
-structure Orderings =
-struct
-
-type 'a preorder = {Orderings__ord_preorder : 'a HOL.ord};
-fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;
-
-type 'a order = {Orderings__preorder_order : 'a preorder};
-fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;
-
-type 'a linorder = {Orderings__order_linorder : 'a order};
-fun order_linorder (A_:'a linorder) = #Orderings__order_linorder A_;
-
-end; (*struct Orderings*)
-
-structure Nat =
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun eq_nat (Suc a) Zero_nat = false
- | eq_nat Zero_nat (Suc a) = false
- | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
- | eq_nat Zero_nat Zero_nat = true;
-
-val eq_nata = {eq = eq_nat} : nat HOL.eq;
-
-fun less_nat m (Suc n) = less_eq_nat m n
- | less_nat n Zero_nat = false
-and less_eq_nat (Suc m) n = less_nat m n
- | less_eq_nat Zero_nat n = true;
-
-val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat HOL.ord;
-
-val preorder_nat = {Orderings__ord_preorder = ord_nat} :
- nat Orderings.preorder;
-
-val order_nat = {Orderings__preorder_order = preorder_nat} :
- nat Orderings.order;
-
-val linorder_nat = {Orderings__order_linorder = order_nat} :
- nat Orderings.linorder;
-
-end; (*struct Nat*)
-
-structure Codegen =
-struct
-
-datatype ('a, 'b) searchtree =
- Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree |
- Leaf of 'a * 'b;
-
-fun update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
- (if HOL.eqop A1_ it key then Leaf (key, entry)
- else (if HOL.less_eq
- ((Orderings.ord_preorder o Orderings.preorder_order o
- Orderings.order_linorder)
- A2_)
- it key
- then Branch (Leaf (it, entry), it, Leaf (key, vala))
- else Branch (Leaf (key, vala), it, Leaf (it, entry))))
- | update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
- (if HOL.less_eq
- ((Orderings.ord_preorder o Orderings.preorder_order o
- Orderings.order_linorder)
- A2_)
- it key
- then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
- else Branch (t1, key, update (A1_, A2_) (it, entry) t2));
-
-val example : (Nat.nat, (Nat.nat list)) searchtree =
- update (Nat.eq_nata, Nat.linorder_nat)
- (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
- [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
- (update (Nat.eq_nata, Nat.linorder_nat)
- (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
- [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
- (update (Nat.eq_nata, Nat.linorder_nat)
- (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
- (Leaf (Nat.Suc Nat.Zero_nat, []))));
-
-end; (*struct Codegen*)