summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-paper
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/misc-paper')
-rw-r--r--tests/hol4/misc-paper/Holmakefile5
-rw-r--r--tests/hol4/misc-paper/paperScript.sml136
-rw-r--r--tests/hol4/misc-paper/paperTheory.sig210
3 files changed, 0 insertions, 351 deletions
diff --git a/tests/hol4/misc-paper/Holmakefile b/tests/hol4/misc-paper/Holmakefile
deleted file mode 100644
index 3c4b8973..00000000
--- a/tests/hol4/misc-paper/Holmakefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# This file was automatically generated - modify ../Holmakefile.template instead
-INCLUDES = ../../../backends/hol4
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all
diff --git a/tests/hol4/misc-paper/paperScript.sml b/tests/hol4/misc-paper/paperScript.sml
deleted file mode 100644
index 3ac5b6ca..00000000
--- a/tests/hol4/misc-paper/paperScript.sml
+++ /dev/null
@@ -1,136 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [paper] *)
-open primitivesLib divDefLib
-
-val _ = new_theory "paper"
-
-
-val ref_incr_fwd_back_def = Define ‘
- (** [paper::ref_incr]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) *)
- ref_incr_fwd_back (x : i32) : i32 result =
- i32_add x (int_to_i32 1)
-’
-
-val test_incr_fwd_def = Define ‘
- (** [paper::test_incr]: forward function *)
- test_incr_fwd : unit result =
- do
- x <- ref_incr_fwd_back (int_to_i32 0);
- if ~ (x = int_to_i32 1) then Fail Failure else Return ()
- od
-’
-
-(** Unit test for [paper::test_incr] *)
-val _ = assert_return (“test_incr_fwd”)
-
-val choose_fwd_def = Define ‘
- (** [paper::choose]: forward function *)
- choose_fwd (b : bool) (x : 't) (y : 't) : 't result =
- if b then Return x else Return y
-’
-
-val choose_back_def = Define ‘
- (** [paper::choose]: backward function 0 *)
- choose_back (b : bool) (x : 't) (y : 't) (ret : 't) : ('t # 't) result =
- if b then Return (ret, y) else Return (x, ret)
-’
-
-val test_choose_fwd_def = Define ‘
- (** [paper::test_choose]: forward function *)
- test_choose_fwd : unit result =
- do
- z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
- z0 <- i32_add z (int_to_i32 1);
- if ~ (z0 = int_to_i32 1)
- then Fail Failure
- else (
- do
- (x, y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
- if ~ (x = int_to_i32 1)
- then Fail Failure
- else if ~ (y = int_to_i32 0) then Fail Failure else Return ()
- od)
- od
-’
-
-(** Unit test for [paper::test_choose] *)
-val _ = assert_return (“test_choose_fwd”)
-
-Datatype:
- (** [paper::List] *)
- list_t = | ListCons 't list_t | ListNil
-End
-
-val [list_nth_mut_fwd_def] = DefineDiv ‘
- (** [paper::list_nth_mut]: forward function *)
- list_nth_mut_fwd (l : 't list_t) (i : u32) : 't result =
- (case l of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return x
- else (do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_fwd tl i0
- od)
- | ListNil => Fail Failure)
-’
-
-val [list_nth_mut_back_def] = DefineDiv ‘
- (** [paper::list_nth_mut]: backward function 0 *)
- list_nth_mut_back (l : 't list_t) (i : u32) (ret : 't) : 't list_t result =
- (case l of
- | ListCons x tl =>
- if i = int_to_u32 0
- then Return (ListCons ret tl)
- else (
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl0 <- list_nth_mut_back tl i0 ret;
- Return (ListCons x tl0)
- od)
- | ListNil => Fail Failure)
-’
-
-val [sum_fwd_def] = DefineDiv ‘
- (** [paper::sum]: forward function *)
- sum_fwd (l : i32 list_t) : i32 result =
- (case l of
- | ListCons x tl => do
- i <- sum_fwd tl;
- i32_add x i
- od
- | ListNil => Return (int_to_i32 0))
-’
-
-val test_nth_fwd_def = Define ‘
- (** [paper::test_nth]: forward function *)
- test_nth_fwd : unit result =
- let l = ListNil in
- let l0 = ListCons (int_to_i32 3) l in
- let l1 = ListCons (int_to_i32 2) l0 in
- do
- x <- list_nth_mut_fwd (ListCons (int_to_i32 1) l1) (int_to_u32 2);
- x0 <- i32_add x (int_to_i32 1);
- l2 <- list_nth_mut_back (ListCons (int_to_i32 1) l1) (int_to_u32 2) x0;
- i <- sum_fwd l2;
- if ~ (i = int_to_i32 7) then Fail Failure else Return ()
- od
-’
-
-(** Unit test for [paper::test_nth] *)
-val _ = assert_return (“test_nth_fwd”)
-
-val call_choose_fwd_def = Define ‘
- (** [paper::call_choose]: forward function *)
- call_choose_fwd (p : (u32 # u32)) : u32 result =
- let (px, py) = p in
- do
- pz <- choose_fwd T px py;
- pz0 <- u32_add pz (int_to_u32 1);
- (px0, _) <- choose_back T px py pz0;
- Return px0
- od
-’
-
-val _ = export_theory ()
diff --git a/tests/hol4/misc-paper/paperTheory.sig b/tests/hol4/misc-paper/paperTheory.sig
deleted file mode 100644
index 2da80da1..00000000
--- a/tests/hol4/misc-paper/paperTheory.sig
+++ /dev/null
@@ -1,210 +0,0 @@
-signature paperTheory =
-sig
- type thm = Thm.thm
-
- (* Definitions *)
- val call_choose_fwd_def : thm
- val choose_back_def : thm
- val choose_fwd_def : thm
- val list_nth_mut_back_def : thm
- val list_nth_mut_fwd_def : thm
- val list_t_TY_DEF : thm
- val list_t_case_def : thm
- val list_t_size_def : thm
- val ref_incr_fwd_back_def : thm
- val sum_fwd_def : thm
- val test_choose_fwd_def : thm
- val test_incr_fwd_def : thm
- val test_nth_fwd_def : thm
-
- (* Theorems *)
- val datatype_list_t : thm
- val list_t_11 : thm
- val list_t_Axiom : thm
- val list_t_case_cong : thm
- val list_t_case_eq : thm
- val list_t_distinct : thm
- val list_t_induction : thm
- val list_t_nchotomy : thm
-
- val paper_grammars : type_grammar.grammar * term_grammar.grammar
-(*
- [divDef] Parent theory of "paper"
-
- [call_choose_fwd_def] Definition
-
- ⊢ ∀p. call_choose_fwd p =
- (let
- (px,py) = p
- in
- do
- pz <- choose_fwd T px py;
- pz0 <- u32_add pz (int_to_u32 1);
- (px0,_) <- choose_back T px py pz0;
- Return px0
- od)
-
- [choose_back_def] Definition
-
- ⊢ ∀b x y ret.
- choose_back b x y ret =
- if b then Return (ret,y) else Return (x,ret)
-
- [choose_fwd_def] Definition
-
- ⊢ ∀b x y. choose_fwd b x y = if b then Return x else Return y
-
- [list_nth_mut_back_def] Definition
-
- ⊢ ∀l i ret.
- list_nth_mut_back l i ret =
- case l of
- ListCons x tl =>
- if i = int_to_u32 0 then Return (ListCons ret tl)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- tl0 <- list_nth_mut_back tl i0 ret;
- Return (ListCons x tl0)
- od
- | ListNil => Fail Failure
-
- [list_nth_mut_fwd_def] Definition
-
- ⊢ ∀l i.
- list_nth_mut_fwd l i =
- case l of
- ListCons x tl =>
- if i = int_to_u32 0 then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_fwd tl i0
- od
- | ListNil => Fail Failure
-
- [list_t_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0'.
- ∀ $var$('list_t').
- (∀a0'.
- (∃a0 a1.
- a0' =
- (λa0 a1.
- ind_type$CONSTR 0 a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
- a0 a1 ∧ $var$('list_t') a1) ∨
- a0' =
- ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
- $var$('list_t') a0') ⇒
- $var$('list_t') a0') rep
-
- [list_t_case_def] Definition
-
- ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
- ∀f v. list_t_CASE ListNil f v = v
-
- [list_t_size_def] Definition
-
- ⊢ (∀f a0 a1.
- list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
- ∀f. list_t_size f ListNil = 0
-
- [ref_incr_fwd_back_def] Definition
-
- ⊢ ∀x. ref_incr_fwd_back x = i32_add x (int_to_i32 1)
-
- [sum_fwd_def] Definition
-
- ⊢ ∀l. sum_fwd l =
- case l of
- ListCons x tl => do i <- sum_fwd tl; i32_add x i od
- | ListNil => Return (int_to_i32 0)
-
- [test_choose_fwd_def] Definition
-
- ⊢ test_choose_fwd =
- do
- z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
- z0 <- i32_add z (int_to_i32 1);
- if z0 ≠ int_to_i32 1 then Fail Failure
- else
- do
- (x,y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
- if x ≠ int_to_i32 1 then Fail Failure
- else if y ≠ int_to_i32 0 then Fail Failure
- else Return ()
- od
- od
-
- [test_incr_fwd_def] Definition
-
- ⊢ test_incr_fwd =
- do
- x <- ref_incr_fwd_back (int_to_i32 0);
- if x ≠ int_to_i32 1 then Fail Failure else Return ()
- od
-
- [test_nth_fwd_def] Definition
-
- ⊢ test_nth_fwd =
- (let
- l = ListNil;
- l0 = ListCons (int_to_i32 3) l;
- l1 = ListCons (int_to_i32 2) l0
- in
- do
- x <-
- list_nth_mut_fwd (ListCons (int_to_i32 1) l1) (int_to_u32 2);
- x0 <- i32_add x (int_to_i32 1);
- l2 <-
- list_nth_mut_back (ListCons (int_to_i32 1) l1)
- (int_to_u32 2) x0;
- i <- sum_fwd l2;
- if i ≠ int_to_i32 7 then Fail Failure else Return ()
- od)
-
- [datatype_list_t] Theorem
-
- ⊢ DATATYPE (list_t ListCons ListNil)
-
- [list_t_11] Theorem
-
- ⊢ ∀a0 a1 a0' a1'.
- ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
-
- [list_t_Axiom] Theorem
-
- ⊢ ∀f0 f1. ∃fn.
- (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
- fn ListNil = f1
-
- [list_t_case_cong] Theorem
-
- ⊢ ∀M M' f v.
- M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
- (M' = ListNil ⇒ v = v') ⇒
- list_t_CASE M f v = list_t_CASE M' f' v'
-
- [list_t_case_eq] Theorem
-
- ⊢ list_t_CASE x f v = v' ⇔
- (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
-
- [list_t_distinct] Theorem
-
- ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
-
- [list_t_induction] Theorem
-
- ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
-
- [list_t_nchotomy] Theorem
-
- ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
-
-
-*)
-end
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-25 00:22:12 +0000