diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/divDefLib.sml | 11 | ||||
| -rw-r--r-- | backends/hol4/divDefLibTestScript.sml | 12 |
2 files changed, 17 insertions, 6 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml index 3e2d7c04..347e2d8e 100644 --- a/backends/hol4/divDefLib.sml +++ b/backends/hol4/divDefLib.sml @@ -445,8 +445,14 @@ fun mk_body (fnames : string list) (in_out_tys : (hol_type * hol_type) list) | CONST _ => tm | LAMB (x, tm) => let - (* The variable might shadow one of the functions *) - val fnames_set = Redblackset.delete (fnames_set, (fst o dest_var) x) + (* The variable might shadow one of the functions: remove it from + the set of function names - remark: Redblackset.delete raises + [NotFound] if the value is not present in the set *) + val varname = (fst o dest_var) x + val fnames_set = + if Redblackset.member (fnames_set, varname) + then Redblackset.delete (fnames_set, varname) + else fnames_set (* Update the term in the lambda *) val tm = replace_rec_calls fnames_set tm in @@ -468,6 +474,7 @@ fun mk_body (fnames : string list) (in_out_tys : (hol_type * hol_type) list) else (* Rec call: replace *) let + val _ = print_dbg ("replace_rec_calls: rec call\n\n") val _ = replace_rec_calls_rec_call_tm := tm (* First, find the index of the function *) val fname = (fst o dest_var) app diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml index c4a57783..b1243065 100644 --- a/backends/hol4/divDefLibTestScript.sml +++ b/backends/hol4/divDefLibTestScript.sml @@ -8,12 +8,16 @@ open primitivesLib open divDefTheory divDefLib val [even_def, odd_def] = DefineDiv ‘ - (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)) + (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)) ’ +Datatype: + list_t = + ListCons 't list_t + | ListNil +End + val [nth_def] = DefineDiv ‘ nth (ls : 't list_t) (i : u32) : 't result = case ls of |