37 NCons :: [bin,bool]=>bin |
37 NCons :: [bin,bool]=>bin |
38 bin_succ :: bin=>bin |
38 bin_succ :: bin=>bin |
39 bin_pred :: bin=>bin |
39 bin_pred :: bin=>bin |
40 bin_minus :: bin=>bin |
40 bin_minus :: bin=>bin |
41 bin_add,bin_mult :: [bin,bin]=>bin |
41 bin_add,bin_mult :: [bin,bin]=>bin |
42 h_bin :: [bin,bool,bin]=>bin |
42 adding :: [bin,bool,bin]=>bin |
43 |
43 |
44 (*NCons inserts a bit, suppressing leading 0s and 1s*) |
44 (*NCons inserts a bit, suppressing leading 0s and 1s*) |
45 primrec |
45 primrec |
46 NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" |
46 NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" |
47 NCons_Min "NCons Min b = (if b then Min else (Min BIT b))" |
47 NCons_Min "NCons Min b = (if b then Min else (Min BIT b))" |
52 integ_of_Min "integ_of Min = - ($# 1)" |
52 integ_of_Min "integ_of Min = - ($# 1)" |
53 integ_of_BIT "integ_of(w BIT x) = (if x then $# 1 else $# 0) + |
53 integ_of_BIT "integ_of(w BIT x) = (if x then $# 1 else $# 0) + |
54 (integ_of w) + (integ_of w)" |
54 (integ_of w) + (integ_of w)" |
55 |
55 |
56 primrec |
56 primrec |
57 succ_Pls "bin_succ Pls = Pls BIT True" |
57 bin_succ_Pls "bin_succ Pls = Pls BIT True" |
58 succ_Min "bin_succ Min = Pls" |
58 bin_succ_Min "bin_succ Min = Pls" |
59 succ_BIT "bin_succ(w BIT x) = |
59 bin_succ_BIT "bin_succ(w BIT x) = |
60 (if x then bin_succ w BIT False |
60 (if x then bin_succ w BIT False |
61 else NCons w True)" |
61 else NCons w True)" |
62 |
62 |
63 primrec |
63 primrec |
64 pred_Pls "bin_pred Pls = Min" |
64 bin_pred_Pls "bin_pred Pls = Min" |
65 pred_Min "bin_pred Min = Min BIT False" |
65 bin_pred_Min "bin_pred Min = Min BIT False" |
66 pred_BIT "bin_pred(w BIT x) = |
66 bin_pred_BIT "bin_pred(w BIT x) = |
67 (if x then NCons w False |
67 (if x then NCons w False |
68 else (bin_pred w) BIT True)" |
68 else (bin_pred w) BIT True)" |
69 |
69 |
70 primrec |
70 primrec |
71 minus_Pls "bin_minus Pls = Pls" |
71 bin_minus_Pls "bin_minus Pls = Pls" |
72 minus_Min "bin_minus Min = Pls BIT True" |
72 bin_minus_Min "bin_minus Min = Pls BIT True" |
73 minus_BIT "bin_minus(w BIT x) = |
73 bin_minus_BIT "bin_minus(w BIT x) = |
74 (if x then bin_pred (NCons (bin_minus w) False) |
74 (if x then bin_pred (NCons (bin_minus w) False) |
75 else bin_minus w BIT False)" |
75 else bin_minus w BIT False)" |
76 |
76 |
77 primrec |
77 primrec |
78 add_Pls "bin_add Pls w = w" |
78 bin_add_Pls "bin_add Pls w = w" |
79 add_Min "bin_add Min w = bin_pred w" |
79 bin_add_Min "bin_add Min w = bin_pred w" |
80 add_BIT "bin_add (v BIT x) w = h_bin v x w" |
80 bin_add_BIT "bin_add (v BIT x) w = adding v x w" |
81 |
81 |
82 primrec |
82 primrec |
83 "h_bin v x Pls = v BIT x" |
83 "adding v x Pls = v BIT x" |
84 "h_bin v x Min = bin_pred (v BIT x)" |
84 "adding v x Min = bin_pred (v BIT x)" |
85 "h_bin v x (w BIT y) = |
85 "adding v x (w BIT y) = |
86 NCons (bin_add v (if (x & y) then bin_succ w else w)) |
86 NCons (bin_add v (if (x & y) then bin_succ w else w)) |
87 (x~=y)" |
87 (x~=y)" |
88 |
88 |
89 primrec |
89 primrec |
90 mult_Pls "bin_mult Pls w = Pls" |
90 bin_mult_Pls "bin_mult Pls w = Pls" |
91 mult_Min "bin_mult Min w = bin_minus w" |
91 bin_mult_Min "bin_mult Min w = bin_minus w" |
92 mult_BIT "bin_mult (v BIT x) w = |
92 bin_mult_BIT "bin_mult (v BIT x) w = |
93 (if x then (bin_add (NCons (bin_mult v w) False) w) |
93 (if x then (bin_add (NCons (bin_mult v w) False) w) |
94 else (NCons (bin_mult v w) False))" |
94 else (NCons (bin_mult v w) False))" |
95 |
95 |
96 |
96 |
97 end |
97 end |
98 |
98 |
99 ML |
99 ML |