diff options
Diffstat (limited to 'backends/hol4/testDivDefScript.sml')
-rw-r--r-- | backends/hol4/testDivDefScript.sml | 87 |
1 files changed, 87 insertions, 0 deletions
diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/testDivDefScript.sml new file mode 100644 index 00000000..4a87895f --- /dev/null +++ b/backends/hol4/testDivDefScript.sml @@ -0,0 +1,87 @@ +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib divDefLib + +val _ = new_theory "testDivDef" + +val def_qt = ‘ + (even (i : int) : bool result = + if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : int) : bool result = + if i = 0 then Return F else even (i - 1)) +’ + +val even_def = DefineDiv def_qt + +(* Complexifying the above definition, and overriding on purpose *) +val def_qt = ‘ + (even (i : int) : bool result = + if i = 0 then + do + b <- Return T; + Return b + od + else do + b <- odd (i - 1); + Return b + od + ) /\ + (odd (i : int) : bool result = + if i = 0 then + do + b <- Return F; + Return b + od + else do + b <- even (i - 1); + Return b + od) +’ + +val even_def = DefineDiv def_qt + +Datatype: + list_t = + ListCons 't list_t + | ListNil +End + +val def_qt = ‘ + nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + nth_mut_fwd tl i0 + od + | ListNil => + Fail Failure +’ + +val nth_mut_fwd_def = DefineDiv def_qt + +(* Complexifying the above definition, and overriding on purpose *) +val def_qt = ‘ + nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + x <- nth_mut_fwd tl i0; + Return x + od + | ListNil => + Fail Failure +’ + +val nth_mut_fwd_def = DefineDiv def_qt + +val _ = export_theory () |