diff options
author | Son Ho | 2023-02-01 00:40:13 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | a8cf54cd23b8bd8c4cb5690ebee48a4086c4ca8d (patch) | |
tree | 04a3de511a760beab50aca80538c469414464e37 /backends/hol4/divDefLib.sml | |
parent | 26309503ab0d7710f03333d7762e484be94767e0 (diff) |
Cleanup a bit and reorganize
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefLib.sml | 98 |
1 files changed, 8 insertions, 90 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml index 3ecb32df..59c1edaf 100644 --- a/backends/hol4/divDefLib.sml +++ b/backends/hol4/divDefLib.sml @@ -1,21 +1,21 @@ (* This file implements utilities to define potentially diverging functions *) +structure divDefLib :> divDefLib = +struct + open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory open primitivesLib -(* TODO: move *) -Theorem case_result_same_eq: - !(r : 'a result). +val case_result_same_eq = prove ( + “!(r : 'a result). (case r of Return x => Return x | Fail e => Fail e - | Diverge => Diverge) = r -Proof - rw [] >> CASE_TAC -QED + | Diverge => Diverge) = r”, + rw [] >> CASE_TAC) (* val ty = id_ty @@ -90,8 +90,6 @@ val bool_ty = “:bool” val alpha_tyvar : hol_type = “:'a” val beta_tyvar : hol_type = “:'b” -val is_diverge_def = Define ‘ - is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’ val is_diverge_tm = “is_diverge: 'a result -> bool” val diverge_tm = “Diverge : 'a result” @@ -1202,84 +1200,4 @@ fun DefineDiv (def_qt : term quotation) = final_eqs end -(* - -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 - -(* Complexigying the above definition *) -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 - -(* Checking what happens with non terminal calls *) -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 - -*) +end |