diff options
Diffstat (limited to 'tests/hol4/misc-paper')
-rw-r--r-- | tests/hol4/misc-paper/Holmakefile | 5 | ||||
-rw-r--r-- | tests/hol4/misc-paper/paperScript.sml | 135 | ||||
-rw-r--r-- | tests/hol4/misc-paper/paperTheory.sig | 210 |
3 files changed, 350 insertions, 0 deletions
diff --git a/tests/hol4/misc-paper/Holmakefile b/tests/hol4/misc-paper/Holmakefile new file mode 100644 index 00000000..3c4b8973 --- /dev/null +++ b/tests/hol4/misc-paper/Holmakefile @@ -0,0 +1,5 @@ +# 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 new file mode 100644 index 00000000..4d6e99ba --- /dev/null +++ b/tests/hol4/misc-paper/paperScript.sml @@ -0,0 +1,135 @@ +(** 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] *) + ref_incr_fwd_back (x : i32) : i32 result = + i32_add x (int_to_i32 1) +’ + +val test_incr_fwd_def = Define ‘ + (** [paper::test_incr] *) + 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] *) + 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] *) + 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] *) + 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] *) + 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] *) + 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] *) + 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] *) + 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] *) + 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 new file mode 100644 index 00000000..2da80da1 --- /dev/null +++ b/tests/hol4/misc-paper/paperTheory.sig @@ -0,0 +1,210 @@ +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 |